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  3004  sbcth  3058  sbciegf  3076  csbiegf  3184  sbcnestg  3194  csbnestg  3195  csbnest1g  3196  int0  3965  mpteq2ia  4198  mpteq2da  4201  ssopab2i  4398  relssi  4843  xpidtr  5155  iotaexab  5333  funcnvsn  5403  funinsn  5407  tfrlem7  6550  tfri1  6598  sucinc  6680  findcard  7147  findcard2  7148  findcard2s  7149  fiintim  7193  fisseneq  7197  frec2uzrand  10771  frec2uzf1od  10772  frecfzennn  10792  hashinfom  11145  zfz1iso  11217  fclim  11983  mopnset  14717  metuex  14720  distop  14967  ch2var  16556  strcollnf  16772