Axiom ax-gen 1390

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 1481 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 1294	1 wff ∀𝑥𝜑

This axiom is referenced by:  gen2  1391  mpg  1392  mpgbi  1393  mpgbir  1394  hbth  1404  19.23h  1439  19.9ht  1584  stdpc6  1643  equveli  1696  cesare  2059  camestres  2060  calemes  2071  ceqsralv  2664  vtocl2  2688  euxfr2dc  2814  sbcth  2867  sbciegf  2884  csbiegf  2985  sbcnestg  2995  csbnestg  2996  csbnest1g  2997  int0  3724  mpteq2ia  3946  mpteq2da  3949  ssopab2i  4128  relssi  4558  xpidtr  4855  funcnvsn  5093  funinsn  5097  tfrlem7  6120  tfri1  6168  sucinc  6246  findcard  6684  findcard2  6685  findcard2s  6686  fiintim  6719  fisseneq  6722  frec2uzrand  9961  frec2uzf1od  9962  frecfzennn  9982  hashinfom  10301  zfz1iso  10361  fclim  10837  distop  11937  ch2var  12376  strcollnf  12588