Axiom ax-gen 1425

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 1516 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 1329	1 wff ∀𝑥𝜑

This axiom is referenced by:  gen2  1426  mpg  1427  mpgbi  1428  mpgbir  1429  hbth  1439  19.23h  1474  19.9ht  1620  stdpc6  1679  equveli  1732  cesare  2103  camestres  2104  calemes  2115  ceqsralv  2717  vtocl2  2741  euxfr2dc  2869  sbcth  2922  sbciegf  2940  csbiegf  3043  sbcnestg  3053  csbnestg  3054  csbnest1g  3055  int0  3785  mpteq2ia  4014  mpteq2da  4017  ssopab2i  4199  relssi  4630  xpidtr  4929  funcnvsn  5168  funinsn  5172  tfrlem7  6214  tfri1  6262  sucinc  6341  findcard  6782  findcard2  6783  findcard2s  6784  fiintim  6817  fisseneq  6820  frec2uzrand  10178  frec2uzf1od  10179  frecfzennn  10199  hashinfom  10524  zfz1iso  10584  fclim  11063  distop  12254  ch2var  12974  strcollnf  13183