Axiom ax-gen 1449

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 1536 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  1450  mpg  1451  mpgbi  1452  mpgbir  1453  hbth  1463  19.23h  1498  19.9ht  1641  stdpc6  1703  equveli  1759  cesare  2130  camestres  2131  calemes  2142  ceqsralv  2768  vtocl2  2792  euxfr2dc  2922  sbcth  2976  sbciegf  2994  csbiegf  3100  sbcnestg  3110  csbnestg  3111  csbnest1g  3112  int0  3857  mpteq2ia  4087  mpteq2da  4090  ssopab2i  4275  relssi  4715  xpidtr  5016  funcnvsn  5258  funinsn  5262  tfrlem7  6313  tfri1  6361  sucinc  6441  findcard  6883  findcard2  6884  findcard2s  6885  fiintim  6923  fisseneq  6926  frec2uzrand  10398  frec2uzf1od  10399  frecfzennn  10419  hashinfom  10749  zfz1iso  10812  fclim  11293  distop  13367  ch2var  14290  strcollnf  14508