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

Axiom ax-17 1628
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 2241 about the logical redundancy of ax-17 1628 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 A. to with no further assumptions. By sp 1766, 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 1550 . 2
41, 3wi 4 1
Colors of variables: wff set class
This axiom is referenced by:  a17d  1629  ax17e  1630  nfv  1631  alimdv  1633  eximdv  1634  albidv  1637  exbidv  1638  alrimiv  1643  alrimdv  1645  19.9v  1679  spimvw  1684  equidOLD  1692  spnfwOLD  1707  spw  1709  spwOLD  1710  19.3vOLD  1712  cbvalvw  1718  alcomiw  1721  hbn1w  1724  ax11wlem  1738  19.8a  1765  spOLD  1767  dvelimhwOLD  1880  ax12olem1OLD  2015  ax12olem6OLD  2020  ax10lem2OLD  2030  dvelimvOLD  2032  a16g  2052  a16gOLD  2053  dvelim  2077  dvelimv  2078  ax11a2  2084  cleljust  2108  ax16ALT  2161  ax11vALT  2180  dvelimALT  2217  ax17o  2241  dveeq2-o  2268  dveeq1-o  2271  ax11el  2278  ax11a2-o  2286  eujustALT  2291  cleqh  2540  abeq2  2548  mpteq12  4322  mpt2bi123f  26859  mptbi12f  26863  stoweidlem35  27938  eu2ndop1stv  28134  alrim3con13v  28856  a9e2nd  28884  ax172  28905  19.21a3con13vVD  29205  tratrbVD  29214  ssralv2VD  29219  a9e2ndVD  29261  a9e2ndALT  29283  bnj1096  29394  bnj1350  29438  bnj1351  29439  bnj1352  29440  bnj1468  29458  bnj1000  29553  bnj1311  29634  bnj1445  29654  bnj1523  29681  dvelimhwNEW7  29696  ax12olem2wAUX7  29697  ax12olem6NEW7  29700  dvelimvNEW7  29703  dvelimwAUX7  29708  ax11a2NEW7  29772  a16gNEW7  29787  cleljustNEW7  29868  ax16ALTNEW7  29876  dvelimALTNEW7  29877  ax12olem2OLD7  29947  dvelimOLD7  29980
  Copyright terms: Public domain W3C validator