Axiom ax-gen 1429

Description: Rule of Generalization. The postulated inference rule of 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. x x = x or even A. y x = x. Theorem spi 1516 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. (Contributed by NM, 5-Aug-1993.)

Hypothesis

Ref	Expression
ax-g.1	|- ph

Assertion

Ref	Expression
ax-gen	|- A. x ph

Detailed syntax breakdown of Axiom ax-gen

Step	Hyp	Ref	Expression
1		wph	. 2 wff ph
2		vx	. 2 setvar x
3	1, 2	wal 1333	1 wff A. x ph

This axiom is referenced by:  gen2  1430  mpg  1431  mpgbi  1432  mpgbir  1433  hbth  1443  19.23h  1478  19.9ht  1621  stdpc6  1683  equveli  1739  cesare  2110  camestres  2111  calemes  2122  ceqsralv  2743  vtocl2  2767  euxfr2dc  2897  sbcth  2950  sbciegf  2968  csbiegf  3074  sbcnestg  3084  csbnestg  3085  csbnest1g  3086  int0  3823  mpteq2ia  4052  mpteq2da  4055  ssopab2i  4239  relssi  4679  xpidtr  4978  funcnvsn  5217  funinsn  5221  tfrlem7  6266  tfri1  6314  sucinc  6394  findcard  6835  findcard2  6836  findcard2s  6837  fiintim  6875  fisseneq  6878  frec2uzrand  10313  frec2uzf1od  10314  frecfzennn  10334  hashinfom  10663  zfz1iso  10723  fclim  11202  distop  12555  ch2var  13412  strcollnf  13631