Axiom ax-gen 1495

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 1582 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 1393	1 wff A. x ph

This axiom is referenced by:  gen2  1496  mpg  1497  mpgbi  1498  mpgbir  1499  hbth  1509  19.23h  1544  19.9ht  1687  stdpc6  1749  equveli  1805  cesare  2182  camestres  2183  calemes  2194  ceqsralv  2832  vtocl2  2857  euxfr2dc  2989  sbcth  3043  sbciegf  3061  csbiegf  3169  sbcnestg  3179  csbnestg  3180  csbnest1g  3181  int0  3940  mpteq2ia  4173  mpteq2da  4176  ssopab2i  4370  relssi  4815  xpidtr  5125  iotaexab  5303  funcnvsn  5372  funinsn  5376  tfrlem7  6478  tfri1  6526  sucinc  6608  findcard  7070  findcard2  7071  findcard2s  7072  fiintim  7116  fisseneq  7119  frec2uzrand  10657  frec2uzf1od  10658  frecfzennn  10678  hashinfom  11030  zfz1iso  11095  fclim  11845  mopnset  14556  metuex  14559  distop  14799  ch2var  16299  strcollnf  16516