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 𝑥 = 𝑥, we can conclude ∀𝑥𝑥 = 𝑥 or even ∀𝑦𝑥 = 𝑥. 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	⊢ 𝜑

Assertion

Ref	Expression
ax-gen	⊢ ∀𝑥𝜑

Detailed syntax breakdown of Axiom ax-gen

Step	Hyp	Ref	Expression
1		wph	. 2 wff 𝜑
2		vx	. 2 setvar 𝑥
3	1, 2	wal 1393	1 wff ∀𝑥𝜑

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  3938  mpteq2ia  4171  mpteq2da  4174  ssopab2i  4368  relssi  4813  xpidtr  5123  iotaexab  5301  funcnvsn  5370  funinsn  5374  tfrlem7  6476  tfri1  6524  sucinc  6606  findcard  7068  findcard2  7069  findcard2s  7070  fiintim  7114  fisseneq  7117  frec2uzrand  10655  frec2uzf1od  10656  frecfzennn  10676  hashinfom  11028  zfz1iso  11092  fclim  11842  mopnset  14553  metuex  14556  distop  14796  ch2var  16273  strcollnf  16490