Axiom ax-gen 1378

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 1469 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 1282	1 wff A. x ph

This axiom is referenced by:  gen2  1379  mpg  1380  mpgbi  1381  mpgbir  1382  hbth  1392  19.23h  1427  19.9ht  1572  stdpc6  1631  equveli  1682  cesare  2045  camestres  2046  calemes  2057  ceqsralv  2630  vtocl2  2654  euxfr2dc  2777  sbcth  2828  sbciegf  2845  csbiegf  2946  sbcnestg  2955  csbnestg  2956  csbnest1g  2957  int0  3650  mpteq2ia  3864  mpteq2da  3867  ssopab2i  4032  relssi  4449  xpidtr  4735  funcnvsn  4965  tfrlem7  5956  tfri1  5974  sucinc  6048  findcard  6372  findcard2  6373  findcard2s  6374  frec2uzzd  9402  frec2uzsucd  9403  frec2uzrand  9407  frec2uzf1od  9408  frecfzennn  9419  fclim  10133  ch2var  10578  strcollnf  10780