Axiom ax-gen 1354

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 1445 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 1257	1 wff A. x ph

This axiom is referenced by:  gen2  1355  mpg  1356  mpgbi  1357  mpgbir  1358  hbth  1368  19.23h  1403  19.9ht  1548  stdpc6  1607  equveli  1658  cesare  2020  camestres  2021  calemes  2032  ceqsralv  2602  vtocl2  2626  euxfr2dc  2748  sbcth  2799  sbciegf  2816  csbiegf  2917  sbcnestg  2926  csbnestg  2927  csbnest1g  2928  int0  3656  mpteq2ia  3870  mpteq2da  3873  ssopab2i  4041  relssi  4458  xpidtr  4742  funcnvsn  4972  tfrlem7  5963  tfri1  5981  sucinc  6055  findcard  6375  findcard2  6376  findcard2s  6377  frec2uzzd  9349  frec2uzsucd  9350  frec2uzrand  9354  frec2uzf1od  9355  frecfzennn  9366  fclim  10045  ch2var  10273  strcollnf  10476