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 1836
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 33669 about the logical redundancy of ax-5 1836 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 2051, 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 1478 . 2 wff 𝑥𝜑
41, 3wi 4 1 wff (𝜑 → ∀𝑥𝜑)
Colors of variables: wff setvar class
This axiom is referenced by:  ax5d  1837  ax5e  1838  ax5ea  1839  alimdv  1842  eximdv  1843  albidv  1846  exbidv  1847  alrimiv  1852  alrimdv  1854  nexdv  1861  stdpc5v  1864  nfvOLD  1868  19.8v  1892  19.23v  1899  spimvw  1924  spw  1964  cbvalvw  1966  alcomiw  1968  hbn1w  1970  ax12wlem  2006  ax12v  2045  ax12vOLD  2047  ax12vOLDOLD  2048  axc16gOLD  2158  cleljustALT  2184  dvelim  2336  dvelimv  2337  axc16ALT  2365  eujustALT  2472  abeq2  2729  ralrimiv  2959  mpteq12  4696  bnj1096  30558  bnj1350  30601  bnj1351  30602  bnj1352  30603  bnj1468  30621  bnj1000  30716  bnj1311  30797  bnj1445  30817  bnj1523  30844  bj-ax12wlem  32256  bj-spimevw  32296  bj-cbvexivw  32299  bj-ax12v3  32314  bj-ax12v3ALT  32315  bj-sbfvv  32405  bj-abeq2  32413  bj-abv  32545  bj-ab0  32546  wl-hbnaev  32934  wl-nfalv  32941  mpt2bi123f  33600  mptbi12f  33604  ax5ALT  33669  dveeq2-o  33695  dveeq1-o  33697  ax12el  33704  ax12a2-o  33712  intimasn  37427  alrim3con13v  38222  ax6e2nd  38253  19.21a3con13vVD  38567  tratrbVD  38577  ssralv2VD  38582  ax6e2ndVD  38624  ax6e2ndALT  38646  stoweidlem35  39556  eu2ndop1stv  40503
  Copyright terms: Public domain W3C validator