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 1837
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 34011 about the logical redundancy of ax-5 1837 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 1479 . 2 wff 𝑥𝜑
41, 3wi 4 1 wff (𝜑 → ∀𝑥𝜑)
Colors of variables: wff setvar class
This axiom is referenced by:  ax5d  1838  ax5e  1839  ax5ea  1840  alimdv  1843  eximdv  1844  albidv  1847  exbidv  1848  alrimiv  1853  alrimdv  1855  nexdv  1862  stdpc5v  1865  nfvOLD  1869  19.8v  1893  19.23v  1900  spimvw  1925  spw  1965  cbvalvw  1967  alcomiw  1969  hbn1w  1971  ax12wlem  2007  ax12v  2046  ax12vOLD  2048  ax12vOLDOLD  2049  axc16gOLD  2159  cleljustALT  2183  cbvalv  2271  dvelim  2335  dvelimv  2336  axc16ALT  2364  eujustALT  2471  abeq2  2730  ralrimiv  2962  mpteq12  4727  bnj1096  30827  bnj1350  30870  bnj1351  30871  bnj1352  30872  bnj1468  30890  bnj1000  30985  bnj1311  31066  bnj1445  31086  bnj1523  31113  bj-ax12wlem  32592  bj-spimevw  32632  bj-cbvexivw  32635  bj-ax12v3  32650  bj-ax12v3ALT  32651  bj-sbfvv  32740  bj-abeq2  32748  bj-abv  32876  bj-ab0  32877  wl-hbnaev  33276  wl-nfalv  33283  mpt2bi123f  33942  mptbi12f  33946  ax5ALT  34011  dveeq2-o  34037  dveeq1-o  34039  ax12el  34046  ax12a2-o  34054  intimasn  37768  alrim3con13v  38563  ax6e2nd  38594  19.21a3con13vVD  38907  tratrbVD  38917  ssralv2VD  38922  ax6e2ndVD  38964  ax6e2ndALT  38986  stoweidlem35  40015  eu2ndop1stv  40965
  Copyright terms: Public domain W3C validator