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

Axiom ax-17 1627
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 2236 about the logical redundancy of ax-17 1627 in the presence of our obsolete axioms.)

This axiom essentially says that if  x does not occur in  ph, i.e.  ph does not depend on  x in any way, then we can add the quantifier  A. x to  ph with no further assumptions. By sp 1764, we can also remove the quantifier (unconditionally). (Contributed by NM, 5-Aug-1993.)

Assertion
Ref Expression
ax-17  |-  ( ph  ->  A. x ph )
Distinct variable group:    ph, x

Detailed syntax breakdown of Axiom ax-17
StepHypRef Expression
1 wph . 2  wff  ph
2 vx . . 3  set  x
31, 2wal 1550 . 2  wff  A. x ph
41, 3wi 4 1  wff  ( ph  ->  A. x ph )
Colors of variables: wff set class
This axiom is referenced by:  a17d  1628  ax17e  1629  nfv  1630  alimdv  1632  eximdv  1633  albidv  1636  exbidv  1637  alrimiv  1642  alrimdv  1644  19.9v  1677  spimvw  1682  equidOLD  1690  spnfwOLD  1705  spw  1707  spwOLD  1708  19.3vOLD  1710  cbvalvw  1716  alcomiw  1719  hbn1w  1722  ax11wlem  1736  19.8a  1763  spOLD  1765  dvelimhwOLD  1878  ax12olem1OLD  2012  ax12olem6OLD  2017  ax10lem2OLD  2027  dvelimvOLD  2029  a16g  2049  a16gOLD  2050  dvelim  2074  dvelimv  2075  ax11a2  2081  cleljust  2105  ax16ALT  2156  ax11vALT  2175  dvelimALT  2212  ax17o  2236  dveeq2-o  2263  dveeq1-o  2266  ax11el  2273  ax11a2-o  2281  eujustALT  2286  cleqh  2535  abeq2  2543  mpteq12  4291  stoweidlem35  27774  eu2ndop1stv  27970  alrim3con13v  28691  a9e2nd  28719  ax172  28740  19.21a3con13vVD  29038  tratrbVD  29047  ssralv2VD  29052  a9e2ndVD  29094  a9e2ndALT  29116  bnj1096  29227  bnj1350  29271  bnj1351  29272  bnj1352  29273  bnj1468  29291  bnj1000  29386  bnj1311  29467  bnj1445  29487  bnj1523  29514  dvelimhwNEW7  29529  ax12olem2wAUX7  29530  ax12olem6NEW7  29533  dvelimvNEW7  29536  dvelimwAUX7  29541  ax11a2NEW7  29605  a16gNEW7  29620  cleljustNEW7  29701  ax16ALTNEW7  29709  dvelimALTNEW7  29710  ax12olem2OLD7  29780  dvelimOLD7  29813
  Copyright terms: Public domain W3C validator