Axiom ax-gen 1495

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 1582 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 1393	1 wff A. x ph

This axiom is referenced by:  gen2  1496  mpg  1497  mpgbi  1498  mpgbir  1499  hbth  1509  19.23h  1544  19.9ht  1687  stdpc6  1749  equveli  1805  cesare  2182  camestres  2183  calemes  2194  ceqsralv  2831  vtocl2  2856  euxfr2dc  2988  sbcth  3042  sbciegf  3060  csbiegf  3168  sbcnestg  3178  csbnestg  3179  csbnest1g  3180  int0  3936  mpteq2ia  4169  mpteq2da  4172  ssopab2i  4365  relssi  4809  xpidtr  5118  iotaexab  5296  funcnvsn  5365  funinsn  5369  tfrlem7  6461  tfri1  6509  sucinc  6589  findcard  7046  findcard2  7047  findcard2s  7048  fiintim  7089  fisseneq  7092  frec2uzrand  10622  frec2uzf1od  10623  frecfzennn  10643  hashinfom  10995  zfz1iso  11058  fclim  11800  mopnset  14510  metuex  14513  distop  14753  ch2var  16089  strcollnf  16306