Axiom ax-gen 1314

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

This axiom is referenced by:  gen2  1315  mpg  1316  mpgbi  1317  mpgbir  1318  hbth  1328  19.23h  1364  equidqeOLD  1403  19.9ht  1510  stdpc6  1569  equveli  1620  cesare  1982  camestres  1983  calemes  1994  ceqsralv  2558  vtocl2  2582  euxfr2dc  2699  sbcth  2750  sbciegf  2767  csbiegf  2863  sbcnestg  2872  csbnestg  2873  csbnest1g  2874  int0  3599  mpteq2ia  3813  mpteq2da  3816  ssopab2i  3984  relssi  4354  xpidtr  4638  funcnvsn  4867  tfrlem7  5851  tfrlemi14  5865  sucinc  5936  ch2var  7206  strcollnf  7399