Axiom ax-gen 955

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 958 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 950	1 wff A.xph

This axiom is referenced by:  gen2 959  mpg 962  hbth 977  stdpc6 1114  cbv3 1147  cbval 1148  ax11eq 1340  a12lem1 1353  euor2 1414  rgen2a 1675  r19.21v 1692  vtocl2 1818  elabgt 1867  mosub 1894  sbcth 1917  sbciegf 1931  sbcralg 1965  sbcrexg 1966  csbex 1980  csbiegf 2002  csbief 2003  csbnestglem 2006  csbnest1g 2008  csbco3g 2011  sbcco3g 2012  int0 2515  intab 2528  dtruALT 2716  ssopab2i 2785  ordom 3104  relssi 3210  eqrelriv 3213  dmcosseq 3316  funsn 3484  fconst 3597  fopabcos 3772  tfrlem7 3856  caoprmo 4010  pssnn 4465  unifi 4484  fiint 4486  fodomfi 4492  supmo 4502  inf0 4530  axinf2 4548  trcl 4569  brdom3 4725  axpowndlem2 4873  axpowndlem4 4875  axregndlem2 4878  axinfnd 4881  suppsr3 5147  fzshftralt 6405  fsumrev 6918  fsumshft 6920  fsum0diag2 7145  sn0top 7540  indistop 7541  distop 7542  fctop 7543  cctop 7545  htthlem12 8495

Copyright terms: Public domain