Axiom ax-gen 1497

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 1584 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 1395	1 wff ∀𝑥𝜑

This axiom is referenced by:  gen2  1498  mpg  1499  mpgbi  1500  mpgbir  1501  hbth  1511  19.23h  1546  19.9ht  1689  stdpc6  1751  equveli  1807  cesare  2184  camestres  2185  calemes  2196  ceqsralv  2834  vtocl2  2859  euxfr2dc  2991  sbcth  3045  sbciegf  3063  csbiegf  3171  sbcnestg  3181  csbnestg  3182  csbnest1g  3183  int0  3942  mpteq2ia  4175  mpteq2da  4178  ssopab2i  4372  relssi  4817  xpidtr  5127  iotaexab  5305  funcnvsn  5375  funinsn  5379  tfrlem7  6482  tfri1  6530  sucinc  6612  findcard  7076  findcard2  7077  findcard2s  7078  fiintim  7122  fisseneq  7126  frec2uzrand  10666  frec2uzf1od  10667  frecfzennn  10687  hashinfom  11039  zfz1iso  11104  fclim  11854  mopnset  14565  metuex  14568  distop  14808  ch2var  16363  strcollnf  16580