MPE Home Metamath Proof Explorer < Previous   Next >
Nearby theorems
Mirrors  >  Home  >  MPE Home  >  Th. List  >  ax-5 Structured version   Visualization version   GIF version

Axiom ax-5 1789
Description: Axiom of Distinctness. This axiom quantifies a variable over a formula in which it does not occur. Axiom C5 in [Megill] p. 444 (p. 11 of the preprint). Also appears as Axiom B6 (p. 75) of system S2 of [Tarski] p. 77 and Axiom C5-1 of [Monk2] p. 113.

(See comments in ax5ALT 32710 about the logical redundancy of ax-5 1789 in the presence of our obsolete axioms.)

This axiom essentially says that if 𝑥 does not occur in 𝜑, i.e. 𝜑 does not depend on 𝑥 in any way, then we can add the quantifier 𝑥 to 𝜑 with no further assumptions. By sp 1990, we can also remove the quantifier (unconditionally). (Contributed by NM, 10-Jan-1993.)

Assertion
Ref Expression
ax-5 (𝜑 → ∀𝑥𝜑)
Distinct variable group:   𝜑,𝑥

Detailed syntax breakdown of Axiom ax-5
StepHypRef Expression
1 wph . 2 wff 𝜑
2 vx . . 3 setvar 𝑥
31, 2wal 1466 . 2 wff 𝑥𝜑
41, 3wi 4 1 wff (𝜑 → ∀𝑥𝜑)
Colors of variables: wff setvar class
This axiom is referenced by:  ax5d  1790  ax5e  1791  nfv  1792  alimdv  1794  eximdv  1795  albidv  1798  exbidv  1799  alrimiv  1804  alrimdv  1806  stdpc5v  1816  19.21vOLDOLD  1818  19.8v  1843  19.23v  1850  spimvw  1875  spw  1915  cbvalvw  1917  alcomiw  1919  hbn1w  1921  ax12wlem  1956  ax12v  1984  ax12vOLD  1986  ax12vOLDOLD  1987  axc16g  2075  cleljustALT  2135  dvelim  2220  dvelimv  2221  axc16ALT  2249  eujustALT  2356  abeq2  2614  ralrimiv  2843  mpteq12  4514  bnj1096  29746  bnj1350  29789  bnj1351  29790  bnj1352  29791  bnj1468  29809  bnj1000  29904  bnj1311  29985  bnj1445  30005  bnj1523  30032  bj-ax5ea  31411  bj-ax12wlem  31413  bj-spimevw  31450  bj-cbvexivw  31453  bj-axc11nv  31535  bj-axc15v  31543  bj-sbfvv  31559  bj-abeq2  31570  bj-abtru  31692  bj-abfal  31693  wl-hbnaev  32082  wl-nfalv  32089  mpt2bi123f  32642  mptbi12f  32646  ax5ALT  32710  dveeq2-o  32737  dveeq1-o  32739  ax12el  32746  ax12a2-o  32754  intimasn  36488  alrim3con13v  37250  ax6e2nd  37281  19.21a3con13vVD  37596  tratrbVD  37606  ssralv2VD  37611  ax6e2ndVD  37653  ax6e2ndALT  37675  stoweidlem35  38332  eu2ndop1stv  39143
  Copyright terms: Public domain W3C validator