Axiom ax-gen 963

Description: Rule of Generalization. The postulated inference rule of pure predicate calculus. See e.g. Rule 2 of [Hamilton] p. 74. This rule says that if something is unconditionally true, then it is true for all values of a variable. For example, if we have proved x = x, we can conclude A.xx = x or even A.yx = x. Theorem a4i 982 shows we can go the other way also: in other words we can add or remove universal quantifiers from the beginning of any theorem as required.

Hypothesis

Ref	Expression
ax-g.1	|- ph

Assertion

Ref	Expression
ax-gen	|- A.xph

Detailed syntax breakdown of Axiom ax-gen

Step	Hyp	Ref	Expression
1		wph	. 2 wff ph
2		vx	. 2 set x
3	1, 2	wal 954	1 wff A.xph

This axiom is referenced by:  ax4 972  ax5o 974  ax5 976  ax6 979  gen2 983  mpg 986  hbth 1001  stdpc6 1127  cbv3 1164  cbval 1165  ax11eq 1363  a12lem1 1376  euor2 1437  rgen2a 1699  r19.21v 1716  vtocl2 1843  elabgt 1895  mosub 1922  sbcth 1946  sbciegf 1960  sbcralg 1994  sbcrexg 1995  csbex 2009  csbiegf 2031  csbief 2032  csbnestglem 2035  csbnest1g 2037  csbco3g 2040  sbcco3g 2041  int0 2547  intab 2560  dtruALT 2748  ssopab2i 2823  ordom 3141  relssi 3248  eqrelriv 3251  dmcosseq 3365  funsn 3543  fconst 3658  fopabcos 3833  tfrlem7 3917  caoprmo 4070  pssnn 4534  unifiOLD 4557  fiint 4559  fiintOLD 4560  fodomfiOLD 4566  supmo 4576  inf0 4606  axinf2 4624  trcl 4645  brdom3 4801  axpowndlem2 4950  axpowndlem4 4952  axregndlem2 4955  axinfnd 4958  suppsr3 5224  fzshftralt 6522  fsumrev 7029  fsumshft 7031  fsum0diag2 7259  sn0top 7647  indistop 7648  distop 7649  fctopOLD 7650  cctop 7652  htthlem12 8631  spwval2 8653  faimpex 10438

Copyright terms: Public domain