Axiom ax-gen 1338

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 1429 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 1241	1 wff A. x ph

This axiom is referenced by:  gen2  1339  mpg  1340  mpgbi  1341  mpgbir  1342  hbth  1352  19.23h  1387  19.9ht  1532  stdpc6  1591  equveli  1642  cesare  2004  camestres  2005  calemes  2016  ceqsralv  2585  vtocl2  2609  euxfr2dc  2726  sbcth  2777  sbciegf  2794  csbiegf  2890  sbcnestg  2899  csbnestg  2900  csbnest1g  2901  int0  3629  mpteq2ia  3843  mpteq2da  3846  ssopab2i  4014  relssi  4431  xpidtr  4715  funcnvsn  4945  tfrlem7  5933  tfri1  5951  sucinc  6025  findcard  6345  findcard2  6346  findcard2s  6347  frec2uzzd  9186  frec2uzsucd  9187  frec2uzrand  9191  frec2uzf1od  9192  frecfzennn  9203  fclim  9815  ch2var  9907  strcollnf  10110