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

Axiom ax-17 1603
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 2096 about the logical redundancy of ax-17 1603 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 1716, 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 1527 . 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  1604  nfv  1605  alimdv  1607  eximdv  1608  albidv  1611  exbidv  1612  alrimiv  1617  alrimdv  1619  spimvw  1639  equid  1644  spnfwOLD  1658  spw  1660  19.3v  1662  alcomiw  1678  hbn1w  1680  ax11wlem  1694  sp  1716  dvelimhw  1735  ax12olem1  1868  ax12olem2  1869  ax12olem6  1873  ax10lem2  1877  dvelimv  1879  a16g  1885  ax11a2  1933  cleljust  1954  dvelim  1956  ax16ALT  1987  dvelimALT  2072  ax17o  2096  dveeq2-o  2123  dveeq1-o  2126  ax11el  2133  ax11a2-o  2141  eujustALT  2146  cleqh  2380  abeq2  2388  mpteq12  4099  gsumdixp  15392  disjorf  23356  stoweidlem35  27784  alrim3con13v  28296  a9e2nd  28324  ax172  28343  19.21a3con13vVD  28628  tratrbVD  28637  ssralv2VD  28642  a9e2ndVD  28684  a9e2ndALT  28707  bnj1096  28814  bnj1350  28858  bnj1351  28859  bnj1352  28860  bnj1468  28878  bnj1000  28973  bnj1311  29054  bnj1445  29074  bnj1523  29101  equvinv  29114  equveliv  29115  a12study4  29117  a12study5rev  29122  ax10lem17ALT  29123  dvelimfALT2OLD  29125  a12study2  29134  a12study10  29136  a12study10n  29137  ax9lem1  29140  ax9lem3  29142  ax9lem6  29145  ax9lem14  29153  ax9lem15  29154  ax9lem17  29156  ax9vax9  29158
  Copyright terms: Public domain W3C validator