Axiom ax-gen 1460

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 1547 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 1362	1 wff A. x ph

This axiom is referenced by:  gen2  1461  mpg  1462  mpgbi  1463  mpgbir  1464  hbth  1474  19.23h  1509  19.9ht  1652  stdpc6  1714  equveli  1770  cesare  2146  camestres  2147  calemes  2158  ceqsralv  2791  vtocl2  2815  euxfr2dc  2945  sbcth  2999  sbciegf  3017  csbiegf  3124  sbcnestg  3134  csbnestg  3135  csbnest1g  3136  int0  3884  mpteq2ia  4115  mpteq2da  4118  ssopab2i  4308  relssi  4750  xpidtr  5056  iotaexab  5233  funcnvsn  5299  funinsn  5303  tfrlem7  6370  tfri1  6418  sucinc  6498  findcard  6944  findcard2  6945  findcard2s  6946  fiintim  6985  fisseneq  6988  frec2uzrand  10476  frec2uzf1od  10477  frecfzennn  10497  hashinfom  10849  zfz1iso  10912  fclim  11437  distop  14253  ch2var  15259  strcollnf  15477