Axiom ax-gen 1546

Description: Rule of Generalization. The postulated inference rule of pure 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 ∀xx = x or even ∀yx = x. Theorem allt in set.mm shows the special case ∀x ⊤. Theorem spi 1753 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	⊢ φ

Assertion

Ref	Expression
ax-gen	⊢ ∀xφ

Detailed syntax breakdown of Axiom ax-gen

Step	Hyp	Ref	Expression
1		wph	. 2 wff φ
2		vx	. 2 setvar x
3	1, 2	wal 1540	1 wff ∀xφ

This axiom is referenced by:  gen2  1547  mpg  1548  mpgbi  1549  mpgbir  1550  hbth  1552  stdpc6  1687  ax12dgen3  1727  spim  1975  cbv3  1982  equveli  1988  sbft  2025  ax11eq  2193  cesare  2307  camestres  2308  calemes  2319  axi12  2333  ceqsralv  2887  vtocl2  2911  mosub  3015  sbcth  3061  sbciegf  3078  csbiegf  3177  sbcnestg  3186  csbnestg  3187  csbnest1g  3189  int0  3941  dfuni12  4292  nnadjoin  4521  sfintfin  4533  tfinnn  4535  vfinspnn  4542  ssopab2i  4715  relssi  4849  eqrelriv  4851  ssdmrn  5100  funmo  5126  caovmo  5646  mpteq2ia  5660  mpteq2da  5667  clos10  5888  xpassen  6058  frecxp  6315