Metamath Proof Explorer < Previous   Next > Nearby theorems Mirrors  >  Home  >  MPE Home  >  Th. List  >  ax-17 Unicode version

Axiom ax-17 1623
 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 ax17o 2205 about the logical redundancy of ax-17 1623 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 1759, we can also remove the quantifier (unconditionally). (Contributed by NM, 5-Aug-1993.)
Assertion
Ref Expression
ax-17
Distinct variable group:   ,

Detailed syntax breakdown of Axiom ax-17
StepHypRef Expression
1 wph . 2
2 vx . . 3
31, 2wal 1546 . 2
41, 3wi 4 1
 Colors of variables: wff set class This axiom is referenced by:  a17d  1624  ax17e  1625  nfv  1626  alimdv  1628  eximdv  1629  albidv  1632  exbidv  1633  alrimiv  1638  alrimdv  1640  19.9v  1672  spimvw  1677  equidOLD  1685  spnfwOLD  1700  spw  1702  spwOLD  1703  19.3vOLD  1705  cbvalvw  1711  alcomiw  1714  hbn1w  1717  ax11wlem  1731  19.8a  1758  spOLD  1760  dvelimhwOLD  1873  ax12olem1OLD  1977  ax12olem6OLD  1982  ax10lem2OLD  1992  dvelimvOLD  1994  a16g  2012  a16gOLD  2013  dvelimv  2017  ax11a2  2044  cleljust  2062  dvelim  2064  ax16ALT  2094  ax11vALT  2144  dvelimALT  2181  ax17o  2205  dveeq2-o  2232  dveeq1-o  2235  ax11el  2242  ax11a2-o  2250  eujustALT  2255  cleqh  2498  abeq2  2506  mpteq12  4243  stoweidlem35  27613  eu2ndop1stv  27809  alrim3con13v  28268  a9e2nd  28296  ax172  28315  19.21a3con13vVD  28613  tratrbVD  28622  ssralv2VD  28627  a9e2ndVD  28669  a9e2ndALT  28692  bnj1096  28799  bnj1350  28843  bnj1351  28844  bnj1352  28845  bnj1468  28863  bnj1000  28958  bnj1311  29039  bnj1445  29059  bnj1523  29086  dvelimhwNEW7  29101  ax12olem2wAUX7  29102  ax12olem6NEW7  29105  dvelimvNEW7  29108  dvelimwAUX7  29113  ax11a2NEW7  29175  a16gNEW7  29190  cleljustNEW7  29268  ax16ALTNEW7  29276  dvelimALTNEW7  29277  ax12olem2OLD7  29330  dvelimOLD7  29363
 Copyright terms: Public domain W3C validator