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  2768  vtocl2  2792  euxfr2dc  2922  sbcth  2976  sbciegf  2994  csbiegf  3100  sbcnestg  3110  csbnestg  3111  csbnest1g  3112  int0  3858  mpteq2ia  4089  mpteq2da  4092  ssopab2i  4277  relssi  4717  xpidtr  5019  funcnvsn  5261  funinsn  5265  tfrlem7  6317  tfri1  6365  sucinc  6445  findcard  6887  findcard2  6888  findcard2s  6889  fiintim  6927  fisseneq  6930  frec2uzrand  10404  frec2uzf1od  10405  frecfzennn  10425  hashinfom  10757  zfz1iso  10820  fclim  11301  distop  13555  ch2var  14489  strcollnf  14707