Axiom ax-gen 1426

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 1517 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 1330	1 wff A. x ph

This axiom is referenced by:  gen2  1427  mpg  1428  mpgbi  1429  mpgbir  1430  hbth  1440  19.23h  1475  19.9ht  1621  stdpc6  1680  equveli  1733  cesare  2104  camestres  2105  calemes  2116  ceqsralv  2720  vtocl2  2744  euxfr2dc  2873  sbcth  2926  sbciegf  2944  csbiegf  3048  sbcnestg  3058  csbnestg  3059  csbnest1g  3060  int0  3793  mpteq2ia  4022  mpteq2da  4025  ssopab2i  4207  relssi  4638  xpidtr  4937  funcnvsn  5176  funinsn  5180  tfrlem7  6222  tfri1  6270  sucinc  6349  findcard  6790  findcard2  6791  findcard2s  6792  fiintim  6825  fisseneq  6828  frec2uzrand  10209  frec2uzf1od  10210  frecfzennn  10230  hashinfom  10556  zfz1iso  10616  fclim  11095  distop  12293  ch2var  13145  strcollnf  13354