MPE Home 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 2207 about the logical redundancy of ax-17 1623 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 1759, 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 1546 . 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  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  2046  cleljust  2064  dvelim  2066  ax16ALT  2096  ax11vALT  2146  dvelimALT  2183  ax17o  2207  dveeq2-o  2234  dveeq1-o  2237  ax11el  2244  ax11a2-o  2252  eujustALT  2257  cleqh  2501  abeq2  2509  mpteq12  4248  stoweidlem35  27651  eu2ndop1stv  27847  alrim3con13v  28328  a9e2nd  28356  ax172  28375  19.21a3con13vVD  28673  tratrbVD  28682  ssralv2VD  28687  a9e2ndVD  28729  a9e2ndALT  28752  bnj1096  28859  bnj1350  28903  bnj1351  28904  bnj1352  28905  bnj1468  28923  bnj1000  29018  bnj1311  29099  bnj1445  29119  bnj1523  29146  dvelimhwNEW7  29161  ax12olem2wAUX7  29162  ax12olem6NEW7  29165  dvelimvNEW7  29168  dvelimwAUX7  29173  ax11a2NEW7  29235  a16gNEW7  29250  cleljustNEW7  29328  ax16ALTNEW7  29336  dvelimALTNEW7  29337  ax12olem2OLD7  29390  dvelimOLD7  29423
  Copyright terms: Public domain W3C validator