Axiom ax-gen 1463

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 1550 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 1362	1 wff A. x ph

This axiom is referenced by:  gen2  1464  mpg  1465  mpgbi  1466  mpgbir  1467  hbth  1477  19.23h  1512  19.9ht  1655  stdpc6  1717  equveli  1773  cesare  2149  camestres  2150  calemes  2161  ceqsralv  2794  vtocl2  2819  euxfr2dc  2949  sbcth  3003  sbciegf  3021  csbiegf  3128  sbcnestg  3138  csbnestg  3139  csbnest1g  3140  int0  3888  mpteq2ia  4119  mpteq2da  4122  ssopab2i  4312  relssi  4754  xpidtr  5060  iotaexab  5237  funcnvsn  5303  funinsn  5307  tfrlem7  6375  tfri1  6423  sucinc  6503  findcard  6949  findcard2  6950  findcard2s  6951  fiintim  6992  fisseneq  6995  frec2uzrand  10497  frec2uzf1od  10498  frecfzennn  10518  hashinfom  10870  zfz1iso  10933  fclim  11459  mopnset  14108  metuex  14111  distop  14321  ch2var  15413  strcollnf  15631