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  2886  vtocl2  2910  mosub  3014  sbcth  3060  sbciegf  3077  csbiegf  3176  sbcnestg  3185  csbnestg  3186  csbnest1g  3188  int0  3940  dfuni12  4291  nnadjoin  4520  sfintfin  4532  tfinnn  4534  vfinspnn  4541  ssopab2i  4714  relssi  4848  eqrelriv  4850  ssdmrn  5099  funmo  5125  caovmo  5645  mpteq2ia  5659  mpteq2da  5666  clos10  5887  xpassen  6057  frecxp  6314