Axiom ax-gen 1498

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 1585 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 1396	1 wff ∀𝑥𝜑

This axiom is referenced by:  gen2  1499  mpg  1500  mpgbi  1501  mpgbir  1502  hbth  1512  19.23h  1547  19.9ht  1690  stdpc6  1751  equveli  1807  cesare  2184  camestres  2185  calemes  2196  ceqsralv  2835  vtocl2  2860  euxfr2dc  2992  sbcth  3046  sbciegf  3064  csbiegf  3172  sbcnestg  3182  csbnestg  3183  csbnest1g  3184  int0  3947  mpteq2ia  4180  mpteq2da  4183  ssopab2i  4378  relssi  4823  xpidtr  5134  iotaexab  5312  funcnvsn  5382  funinsn  5386  tfrlem7  6526  tfri1  6574  sucinc  6656  findcard  7120  findcard2  7121  findcard2s  7122  fiintim  7166  fisseneq  7170  frec2uzrand  10730  frec2uzf1od  10731  frecfzennn  10751  hashinfom  11103  zfz1iso  11168  fclim  11934  mopnset  14648  metuex  14651  distop  14896  ch2var  16485  strcollnf  16701