Axiom ax-gen 1473

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 1560 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 1371	1 wff A. x ph

This axiom is referenced by:  gen2  1474  mpg  1475  mpgbi  1476  mpgbir  1477  hbth  1487  19.23h  1522  19.9ht  1665  stdpc6  1727  equveli  1783  cesare  2160  camestres  2161  calemes  2172  ceqsralv  2808  vtocl2  2833  euxfr2dc  2965  sbcth  3019  sbciegf  3037  csbiegf  3145  sbcnestg  3155  csbnestg  3156  csbnest1g  3157  int0  3913  mpteq2ia  4146  mpteq2da  4149  ssopab2i  4342  relssi  4784  xpidtr  5092  iotaexab  5269  funcnvsn  5338  funinsn  5342  tfrlem7  6426  tfri1  6474  sucinc  6554  findcard  7011  findcard2  7012  findcard2s  7013  fiintim  7054  fisseneq  7057  frec2uzrand  10587  frec2uzf1od  10588  frecfzennn  10608  hashinfom  10960  zfz1iso  11023  fclim  11720  mopnset  14429  metuex  14432  distop  14672  ch2var  15903  strcollnf  16120