Axiom ax-gen 1475

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 1562 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 1373	1 wff ∀𝑥𝜑

This axiom is referenced by:  gen2  1476  mpg  1477  mpgbi  1478  mpgbir  1479  hbth  1489  19.23h  1524  19.9ht  1667  stdpc6  1729  equveli  1785  cesare  2162  camestres  2163  calemes  2174  ceqsralv  2811  vtocl2  2836  euxfr2dc  2968  sbcth  3022  sbciegf  3040  csbiegf  3148  sbcnestg  3158  csbnestg  3159  csbnest1g  3160  int0  3916  mpteq2ia  4149  mpteq2da  4152  ssopab2i  4345  relssi  4787  xpidtr  5095  iotaexab  5273  funcnvsn  5342  funinsn  5346  tfrlem7  6433  tfri1  6481  sucinc  6561  findcard  7018  findcard2  7019  findcard2s  7020  fiintim  7061  fisseneq  7064  frec2uzrand  10594  frec2uzf1od  10595  frecfzennn  10615  hashinfom  10967  zfz1iso  11030  fclim  11771  mopnset  14481  metuex  14484  distop  14724  ch2var  16041  strcollnf  16258