Axiom ax-gen 1311

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.xx = x or even A.yx = x. Theorem spi 1402 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.xph

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 1221	1 wff A.xph

This axiom is referenced by:  gen2  1312  mpg  1313  mpgbi  1314  mpgbir  1315  hbth  1325  19.23h  1360  19.9ht  1505  stdpc6  1564  equveli  1615  cesare  1977  camestres  1978  calemes  1989  ceqsralv  2553  vtocl2  2577  euxfr2dc  2694  sbcth  2745  sbciegf  2762  csbiegf  2858  sbcnestg  2867  csbnestg  2868  csbnest1g  2869  int0  3592  mpteq2ia  3806  mpteq2da  3809  ssopab2i  3977  relssi  4346  xpidtr  4630  funcnvsn  4859  tfrlem7  5843  tfrlemi14  5857  sucinc  5928  ch2var  8172  strcollnf  8365