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 1826
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 33006 about the logical redundancy of ax-5 1826 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 2040, 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 1472 . 2 wff 𝑥𝜑
41, 3wi 4 1 wff (𝜑 → ∀𝑥𝜑)
Colors of variables: wff setvar class
This axiom is referenced by:  ax5d  1827  ax5e  1828  nfv  1829  alimdv  1831  eximdv  1832  albidv  1835  exbidv  1836  alrimiv  1841  alrimdv  1843  nexdv  1850  stdpc5v  1853  nfvOLD  1857  19.8v  1881  19.23v  1888  spimvw  1913  spw  1953  cbvalvw  1955  alcomiw  1957  hbn1w  1959  ax12wlem  1995  ax12v  2034  ax12vOLD  2036  ax12vOLDOLD  2037  axc16gOLD  2146  cleljustALT  2172  dvelim  2324  dvelimv  2325  axc16ALT  2353  eujustALT  2460  abeq2  2718  ralrimiv  2947  mpteq12  4658  bnj1096  29913  bnj1350  29956  bnj1351  29957  bnj1352  29958  bnj1468  29976  bnj1000  30071  bnj1311  30152  bnj1445  30172  bnj1523  30199  bj-ax5ea  31611  bj-ax12wlem  31613  bj-spimevw  31650  bj-cbvexivw  31653  bj-ax12v3  31668  bj-ax12v3ALT  31669  bj-sbfvv  31759  bj-abeq2  31767  bj-abv  31889  bj-ab0  31890  wl-hbnaev  32280  wl-nfalv  32287  mpt2bi123f  32937  mptbi12f  32941  ax5ALT  33006  dveeq2-o  33032  dveeq1-o  33034  ax12el  33041  ax12a2-o  33049  intimasn  36764  alrim3con13v  37560  ax6e2nd  37591  19.21a3con13vVD  37905  tratrbVD  37915  ssralv2VD  37920  ax6e2ndVD  37962  ax6e2ndALT  37984  stoweidlem35  38725  eu2ndop1stv  39648
  Copyright terms: Public domain W3C validator