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 used 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  3984  mpteq2ia  4219  mpteq2da  4222  ssopab2i  4422  relssi  4868  xpidtr  5181  iotaexab  5359  funcnvsn  5429  funinsn  5433  tfrlem7  6593  tfri1  6641  sucinc  6723  findcard  7198  findcard2  7199  findcard2s  7200  fiintim  7244  fisseneq  7248  frec2uzrand  10862  frec2uzf1od  10863  frecfzennn  10883  hashinfom  11238  zfz1iso  11314  fclim  12084  mopnset  14997  metuex  15000  distop  15328  ch2var  17017  strcollnf  17233