Axiom ax-gen 1473

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 1560 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 1371	1 wff ∀𝑥𝜑

This axiom is referenced by:  gen2  1474  mpg  1475  mpgbi  1476  mpgbir  1477  hbth  1487  19.23h  1522  19.9ht  1665  stdpc6  1727  equveli  1783  cesare  2159  camestres  2160  calemes  2171  ceqsralv  2804  vtocl2  2829  euxfr2dc  2959  sbcth  3013  sbciegf  3031  csbiegf  3138  sbcnestg  3148  csbnestg  3149  csbnest1g  3150  int0  3901  mpteq2ia  4134  mpteq2da  4137  ssopab2i  4328  relssi  4770  xpidtr  5078  iotaexab  5255  funcnvsn  5324  funinsn  5328  tfrlem7  6410  tfri1  6458  sucinc  6538  findcard  6992  findcard2  6993  findcard2s  6994  fiintim  7035  fisseneq  7038  frec2uzrand  10557  frec2uzf1od  10558  frecfzennn  10578  hashinfom  10930  zfz1iso  10993  fclim  11649  mopnset  14358  metuex  14361  distop  14601  ch2var  15777  strcollnf  15995