Axiom ax-gen 1379

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 1470 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 1283	1 wff A. x ph

This axiom is referenced by:  gen2  1380  mpg  1381  mpgbi  1382  mpgbir  1383  hbth  1393  19.23h  1428  19.9ht  1573  stdpc6  1632  equveli  1684  cesare  2047  camestres  2048  calemes  2059  ceqsralv  2639  vtocl2  2663  euxfr2dc  2786  sbcth  2837  sbciegf  2854  csbiegf  2955  sbcnestg  2964  csbnestg  2965  csbnest1g  2966  int0  3670  mpteq2ia  3884  mpteq2da  3887  ssopab2i  4060  relssi  4477  xpidtr  4765  funcnvsn  4995  funinsn  4999  tfrlem7  5986  tfri1  6034  sucinc  6109  findcard  6444  findcard2  6445  findcard2s  6446  fisseneq  6474  frec2uzrand  9539  frec2uzf1od  9540  frecfzennn  9560  hashinfom  9854  fclim  10334  ch2var  10838  strcollnf  11047