Axiom ax-gen 1449

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 x = x, we can conclude A. x x = x or even A. y x = x. Theorem spi 1536 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	|- ph

Assertion

Ref	Expression
ax-gen	|- A. x ph

Detailed syntax breakdown of Axiom ax-gen

Step	Hyp	Ref	Expression
1		wph	. 2 wff ph
2		vx	. 2 setvar x
3	1, 2	wal 1351	1 wff A. x ph

This axiom is referenced by:  gen2  1450  mpg  1451  mpgbi  1452  mpgbir  1453  hbth  1463  19.23h  1498  19.9ht  1641  stdpc6  1703  equveli  1759  cesare  2130  camestres  2131  calemes  2142  ceqsralv  2769  vtocl2  2793  euxfr2dc  2923  sbcth  2977  sbciegf  2995  csbiegf  3101  sbcnestg  3111  csbnestg  3112  csbnest1g  3113  int0  3859  mpteq2ia  4090  mpteq2da  4093  ssopab2i  4278  relssi  4718  xpidtr  5020  funcnvsn  5262  funinsn  5266  tfrlem7  6318  tfri1  6366  sucinc  6446  findcard  6888  findcard2  6889  findcard2s  6890  fiintim  6928  fisseneq  6931  frec2uzrand  10405  frec2uzf1od  10406  frecfzennn  10426  hashinfom  10758  zfz1iso  10821  fclim  11302  distop  13588  ch2var  14522  strcollnf  14740