Axiom ax-gen 1460

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 1547 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 1362	1 wff ∀𝑥𝜑

This axiom is referenced by:  gen2  1461  mpg  1462  mpgbi  1463  mpgbir  1464  hbth  1474  19.23h  1509  19.9ht  1652  stdpc6  1714  equveli  1770  cesare  2146  camestres  2147  calemes  2158  ceqsralv  2791  vtocl2  2816  euxfr2dc  2946  sbcth  3000  sbciegf  3018  csbiegf  3125  sbcnestg  3135  csbnestg  3136  csbnest1g  3137  int0  3885  mpteq2ia  4116  mpteq2da  4119  ssopab2i  4309  relssi  4751  xpidtr  5057  iotaexab  5234  funcnvsn  5300  funinsn  5304  tfrlem7  6372  tfri1  6420  sucinc  6500  findcard  6946  findcard2  6947  findcard2s  6948  fiintim  6987  fisseneq  6990  frec2uzrand  10479  frec2uzf1od  10480  frecfzennn  10500  hashinfom  10852  zfz1iso  10915  fclim  11440  mopnset  14051  metuex  14054  distop  14264  ch2var  15329  strcollnf  15547