Axiom ax-gen 1502

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 1589 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 1400	1 wff ∀𝑥𝜑

This axiom is used by:  gen2  1503  mpg  1504  mpgbi  1505  mpgbir  1506  hbth  1516  19.23h  1551  19.9ht  1694  stdpc6  1755  equveli  1812  cesare  2191  camestres  2192  calemes  2203  ceqsralv  2853  vtocl2  2878  euxfr2dc  3011  sbcth  3065  sbciegf  3083  csbiegf  3191  sbcnestg  3201  csbnestg  3202  csbnest1g  3203  int0  3984  mpteq2ia  4217  mpteq2da  4220  ssopab2i  4420  relssi  4866  xpidtr  5178  iotaexab  5356  funcnvsn  5426  funinsn  5430  tfrlem7  6588  tfri1  6636  sucinc  6718  findcard  7192  findcard2  7193  findcard2s  7194  fiintim  7238  fisseneq  7242  frec2uzrand  10857  frec2uzf1od  10858  frecfzennn  10878  hashinfom  11233  zfz1iso  11309  fclim  12079  mopnset  14973  metuex  14976  distop  15277  ch2var  16961  strcollnf  17177