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  1808  cesare  2187  camestres  2188  calemes  2199  ceqsralv  2847  vtocl2  2872  euxfr2dc  3005  sbcth  3059  sbciegf  3077  csbiegf  3185  sbcnestg  3195  csbnestg  3196  csbnest1g  3197  int0  3968  mpteq2ia  4201  mpteq2da  4204  ssopab2i  4401  relssi  4846  xpidtr  5158  iotaexab  5336  funcnvsn  5406  funinsn  5410  tfrlem7  6561  tfri1  6609  sucinc  6691  findcard  7158  findcard2  7159  findcard2s  7160  fiintim  7204  fisseneq  7208  frec2uzrand  10791  frec2uzf1od  10792  frecfzennn  10812  hashinfom  11166  zfz1iso  11238  fclim  12004  mopnset  14826  metuex  14829  distop  15076  ch2var  16665  strcollnf  16881