Axiom ax-gen 1502

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 1589 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 1400	1 wff A. x ph

This axiom is used by:  gen2  1503  mpg  1504  mpgbi  1505  mpgbir  1506  hbth  1516  19.23h  1551  19.9ht  1694  stdpc6  1755  equveli  1812  cesare  2191  camestres  2192  calemes  2203  ceqsralv  2853  vtocl2  2878  euxfr2dc  3011  sbcth  3065  sbciegf  3083  csbiegf  3191  sbcnestg  3201  csbnestg  3202  csbnest1g  3203  int0  3984  mpteq2ia  4217  mpteq2da  4220  ssopab2i  4420  relssi  4866  xpidtr  5178  iotaexab  5356  funcnvsn  5426  funinsn  5430  tfrlem7  6588  tfri1  6636  sucinc  6718  findcard  7192  findcard2  7193  findcard2s  7194  fiintim  7238  fisseneq  7242  frec2uzrand  10842  frec2uzf1od  10843  frecfzennn  10863  hashinfom  11217  zfz1iso  11293  fclim  12060  mopnset  14889  metuex  14892  distop  15186  ch2var  16795  strcollnf  17011