Axiom ax-gen 1495

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 1582 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 1393	1 wff A. x ph

This axiom is referenced by:  gen2  1496  mpg  1497  mpgbi  1498  mpgbir  1499  hbth  1509  19.23h  1544  19.9ht  1687  stdpc6  1749  equveli  1805  cesare  2182  camestres  2183  calemes  2194  ceqsralv  2831  vtocl2  2856  euxfr2dc  2988  sbcth  3042  sbciegf  3060  csbiegf  3168  sbcnestg  3178  csbnestg  3179  csbnest1g  3180  int0  3937  mpteq2ia  4170  mpteq2da  4173  ssopab2i  4366  relssi  4810  xpidtr  5119  iotaexab  5297  funcnvsn  5366  funinsn  5370  tfrlem7  6469  tfri1  6517  sucinc  6599  findcard  7058  findcard2  7059  findcard2s  7060  fiintim  7104  fisseneq  7107  frec2uzrand  10639  frec2uzf1od  10640  frecfzennn  10660  hashinfom  11012  zfz1iso  11076  fclim  11820  mopnset  14531  metuex  14534  distop  14774  ch2var  16186  strcollnf  16403