Axiom ax-gen 1442

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 1529 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 1346	1 wff ∀𝑥𝜑

This axiom is referenced by:  gen2  1443  mpg  1444  mpgbi  1445  mpgbir  1446  hbth  1456  19.23h  1491  19.9ht  1634  stdpc6  1696  equveli  1752  cesare  2123  camestres  2124  calemes  2135  ceqsralv  2761  vtocl2  2785  euxfr2dc  2915  sbcth  2968  sbciegf  2986  csbiegf  3092  sbcnestg  3102  csbnestg  3103  csbnest1g  3104  int0  3845  mpteq2ia  4075  mpteq2da  4078  ssopab2i  4262  relssi  4702  xpidtr  5001  funcnvsn  5243  funinsn  5247  tfrlem7  6296  tfri1  6344  sucinc  6424  findcard  6866  findcard2  6867  findcard2s  6868  fiintim  6906  fisseneq  6909  frec2uzrand  10361  frec2uzf1od  10362  frecfzennn  10382  hashinfom  10712  zfz1iso  10776  fclim  11257  distop  12879  ch2var  13802  strcollnf  14020