Axiom ax-gen 1471

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 1558 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 1370	1 wff A. x ph

This axiom is referenced by:  gen2  1472  mpg  1473  mpgbi  1474  mpgbir  1475  hbth  1485  19.23h  1520  19.9ht  1663  stdpc6  1725  equveli  1781  cesare  2157  camestres  2158  calemes  2169  ceqsralv  2802  vtocl2  2827  euxfr2dc  2957  sbcth  3011  sbciegf  3029  csbiegf  3136  sbcnestg  3146  csbnestg  3147  csbnest1g  3148  int0  3898  mpteq2ia  4129  mpteq2da  4132  ssopab2i  4323  relssi  4765  xpidtr  5072  iotaexab  5249  funcnvsn  5318  funinsn  5322  tfrlem7  6402  tfri1  6450  sucinc  6530  findcard  6984  findcard2  6985  findcard2s  6986  fiintim  7027  fisseneq  7030  frec2uzrand  10548  frec2uzf1od  10549  frecfzennn  10569  hashinfom  10921  zfz1iso  10984  fclim  11547  mopnset  14256  metuex  14259  distop  14499  ch2var  15636  strcollnf  15854