Axiom ax-gen 1502

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 1589 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 1400	1 wff ∀𝑥𝜑

This axiom is referenced by:  gen2  1503  mpg  1504  mpgbi  1505  mpgbir  1506  hbth  1516  19.23h  1551  19.9ht  1694  stdpc6  1755  equveli  1812  cesare  2191  camestres  2192  calemes  2203  ceqsralv  2853  vtocl2  2878  euxfr2dc  3011  sbcth  3065  sbciegf  3083  csbiegf  3191  sbcnestg  3201  csbnestg  3202  csbnest1g  3203  int0  3982  mpteq2ia  4215  mpteq2da  4218  ssopab2i  4418  relssi  4864  xpidtr  5176  iotaexab  5354  funcnvsn  5424  funinsn  5428  tfrlem7  6581  tfri1  6629  sucinc  6711  findcard  7185  findcard2  7186  findcard2s  7187  fiintim  7231  fisseneq  7235  frec2uzrand  10823  frec2uzf1od  10824  frecfzennn  10844  hashinfom  11198  zfz1iso  11274  fclim  12041  mopnset  14864  metuex  14867  distop  15112  ch2var  16712  strcollnf  16928