Axiom ax-gen 965

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 984 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 956	1 wff A.xph

This axiom is referenced by:  ax4 974  ax5o 976  ax5 978  ax6 981  gen2 985  mpg 988  hbth 1003  stdpc6 1129  cbv3 1166  cbval 1167  ax11eq 1365  a12lem1 1378  euor2 1440  rgen2a 1702  r19.21v 1719  vtocl2 1846  elabgt 1898  mosub 1925  sbcth 1949  sbciegf 1963  sbcralg 1997  sbcrexg 1998  csbex 2012  csbiegf 2034  csbief 2035  csbnestglem 2038  csbnest1g 2040  csbco3g 2043  sbcco3g 2044  int0 2551  intab 2564  dtruALT 2754  ssopab2i 2829  ordom 3147  relssi 3254  eqrelriv 3257  dmcosseq 3371  funsn 3549  fconst 3664  fopabcos 3839  tfrlem7 3923  caoprmo 4076  pssnn 4544  unifiOLD 4570  fiint 4572  fiintOLD 4573  fodomfi 4575  fodomfiOLD 4576  supmo 4585  inf0 4615  axinf2 4633  trcl 4655  brdom3 4811  axpowndlem2 4962  axpowndlem4 4964  axregndlem2 4967  axinfnd 4970  suppsr3 5236  fzshftralt 6523  fsumrev 7029  fsumshft 7031  fsum0diag2 7259  sn0top 7644  indistop 7645  distop 7646  fctopOLD 7647  cctop 7649  htthlem12 8627  spwval2 8649  faimpex 10433

Copyright terms: Public domain