New Foundations Explorer < Previous   Next > Nearby theorems Mirrors  >  Home  >  NFE Home  >  Th. List  >  ax-gen GIF version

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
StepHypRef Expression
1 wph . 2 wff φ
2 vx . 2 setvar x
31, 2wal 1540 1 wff xφ
 Colors of variables: wff setvar class 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
 Copyright terms: Public domain W3C validator