Axiom ax-gen 1437

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 1524 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 1341	1 wff ∀𝑥𝜑

This axiom is referenced by:  gen2  1438  mpg  1439  mpgbi  1440  mpgbir  1441  hbth  1451  19.23h  1486  19.9ht  1629  stdpc6  1691  equveli  1747  cesare  2118  camestres  2119  calemes  2130  ceqsralv  2756  vtocl2  2780  euxfr2dc  2910  sbcth  2963  sbciegf  2981  csbiegf  3087  sbcnestg  3097  csbnestg  3098  csbnest1g  3099  int0  3837  mpteq2ia  4067  mpteq2da  4070  ssopab2i  4254  relssi  4694  xpidtr  4993  funcnvsn  5232  funinsn  5236  tfrlem7  6281  tfri1  6329  sucinc  6409  findcard  6850  findcard2  6851  findcard2s  6852  fiintim  6890  fisseneq  6893  frec2uzrand  10336  frec2uzf1od  10337  frecfzennn  10357  hashinfom  10687  zfz1iso  10750  fclim  11231  distop  12685  ch2var  13608  strcollnf  13827