Axiom ax-gen 1459

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 1546 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 1361	1 wff A. x ph

This axiom is referenced by:  gen2  1460  mpg  1461  mpgbi  1462  mpgbir  1463  hbth  1473  19.23h  1508  19.9ht  1651  stdpc6  1713  equveli  1769  cesare  2140  camestres  2141  calemes  2152  ceqsralv  2780  vtocl2  2804  euxfr2dc  2934  sbcth  2988  sbciegf  3006  csbiegf  3112  sbcnestg  3122  csbnestg  3123  csbnest1g  3124  int0  3870  mpteq2ia  4101  mpteq2da  4104  ssopab2i  4289  relssi  4729  xpidtr  5031  funcnvsn  5273  funinsn  5277  tfrlem7  6332  tfri1  6380  sucinc  6460  findcard  6902  findcard2  6903  findcard2s  6904  fiintim  6942  fisseneq  6945  frec2uzrand  10419  frec2uzf1od  10420  frecfzennn  10440  hashinfom  10772  zfz1iso  10835  fclim  11316  distop  13881  ch2var  14815  strcollnf  15033