Axiom ax-gen 1495

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 1582 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 1393	1 wff ∀𝑥𝜑

This axiom is referenced by:  gen2  1496  mpg  1497  mpgbi  1498  mpgbir  1499  hbth  1509  19.23h  1544  19.9ht  1687  stdpc6  1749  equveli  1805  cesare  2182  camestres  2183  calemes  2194  ceqsralv  2831  vtocl2  2856  euxfr2dc  2988  sbcth  3042  sbciegf  3060  csbiegf  3168  sbcnestg  3178  csbnestg  3179  csbnest1g  3180  int0  3937  mpteq2ia  4170  mpteq2da  4173  ssopab2i  4366  relssi  4810  xpidtr  5119  iotaexab  5297  funcnvsn  5366  funinsn  5370  tfrlem7  6463  tfri1  6511  sucinc  6591  findcard  7050  findcard2  7051  findcard2s  7052  fiintim  7093  fisseneq  7096  frec2uzrand  10627  frec2uzf1od  10628  frecfzennn  10648  hashinfom  11000  zfz1iso  11063  fclim  11805  mopnset  14516  metuex  14519  distop  14759  ch2var  16131  strcollnf  16348