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  6592  tfri1  6640  sucinc  6722  findcard  7196  findcard2  7197  findcard2s  7198  fiintim  7242  fisseneq  7246  frec2uzrand  10863  frec2uzf1od  10864  frecfzennn  10884  hashinfom  11239  zfz1iso  11315  fclim  12085  mopnset  14998  metuex  15001  distop  15311  ch2var  17000  strcollnf  17216