Axiom ax-gen 1447

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 1534 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 1351	1 wff ∀𝑥𝜑

This axiom is referenced by:  gen2  1448  mpg  1449  mpgbi  1450  mpgbir  1451  hbth  1461  19.23h  1496  19.9ht  1639  stdpc6  1701  equveli  1757  cesare  2128  camestres  2129  calemes  2140  ceqsralv  2766  vtocl2  2790  euxfr2dc  2920  sbcth  2974  sbciegf  2992  csbiegf  3098  sbcnestg  3108  csbnestg  3109  csbnest1g  3110  int0  3854  mpteq2ia  4084  mpteq2da  4087  ssopab2i  4271  relssi  4711  xpidtr  5011  funcnvsn  5253  funinsn  5257  tfrlem7  6308  tfri1  6356  sucinc  6436  findcard  6878  findcard2  6879  findcard2s  6880  fiintim  6918  fisseneq  6921  frec2uzrand  10373  frec2uzf1od  10374  frecfzennn  10394  hashinfom  10724  zfz1iso  10787  fclim  11268  distop  13154  ch2var  14077  strcollnf  14295