Axiom ax-gen 1497

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 1584 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 1395	1 wff A. x ph

This axiom is referenced by:  gen2  1498  mpg  1499  mpgbi  1500  mpgbir  1501  hbth  1511  19.23h  1546  19.9ht  1689  stdpc6  1751  equveli  1807  cesare  2184  camestres  2185  calemes  2196  ceqsralv  2834  vtocl2  2859  euxfr2dc  2991  sbcth  3045  sbciegf  3063  csbiegf  3171  sbcnestg  3181  csbnestg  3182  csbnest1g  3183  int0  3942  mpteq2ia  4175  mpteq2da  4178  ssopab2i  4372  relssi  4817  xpidtr  5127  iotaexab  5305  funcnvsn  5375  funinsn  5379  tfrlem7  6486  tfri1  6534  sucinc  6616  findcard  7080  findcard2  7081  findcard2s  7082  fiintim  7126  fisseneq  7130  frec2uzrand  10671  frec2uzf1od  10672  frecfzennn  10692  hashinfom  11044  zfz1iso  11109  fclim  11875  mopnset  14588  metuex  14591  distop  14836  ch2var  16422  strcollnf  16639