Axiom ax-gen 1335

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

This axiom is referenced by:  gen2  1336  mpg  1337  mpgbi  1338  mpgbir  1339  hbth  1349  19.23h  1384  19.9ht  1529  stdpc6  1588  equveli  1639  cesare  2001  camestres  2002  calemes  2013  ceqsralv  2579  vtocl2  2603  euxfr2dc  2720  sbcth  2771  sbciegf  2788  csbiegf  2884  sbcnestg  2893  csbnestg  2894  csbnest1g  2895  int0  3620  mpteq2ia  3834  mpteq2da  3837  ssopab2i  4005  relssi  4374  xpidtr  4658  funcnvsn  4888  tfrlem7  5874  tfri1  5892  sucinc  5964  frec2uzzd  8867  frec2uzsucd  8868  frec2uzrand  8872  frec2uzf1od  8873  frecfzennn  8884  ch2var  9242  strcollnf  9445