Axiom ax-gen 1463

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 1550 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 1362	1 wff ∀𝑥𝜑

This axiom is referenced by:  gen2  1464  mpg  1465  mpgbi  1466  mpgbir  1467  hbth  1477  19.23h  1512  19.9ht  1655  stdpc6  1717  equveli  1773  cesare  2149  camestres  2150  calemes  2161  ceqsralv  2794  vtocl2  2819  euxfr2dc  2949  sbcth  3003  sbciegf  3021  csbiegf  3128  sbcnestg  3138  csbnestg  3139  csbnest1g  3140  int0  3889  mpteq2ia  4120  mpteq2da  4123  ssopab2i  4313  relssi  4755  xpidtr  5061  iotaexab  5238  funcnvsn  5304  funinsn  5308  tfrlem7  6384  tfri1  6432  sucinc  6512  findcard  6958  findcard2  6959  findcard2s  6960  fiintim  7001  fisseneq  7004  frec2uzrand  10514  frec2uzf1od  10515  frecfzennn  10535  hashinfom  10887  zfz1iso  10950  fclim  11476  mopnset  14184  metuex  14187  distop  14405  ch2var  15497  strcollnf  15715