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

Axiom ax-17 1605
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 2100 about the logical redundancy of ax-17 1605 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 1719, 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 1529 . 2  wff  A. x ph
41, 3wi 6 1  wff  ( ph  ->  A. x ph )
Colors of variables: wff set class
This axiom is referenced by:  a17d  1606  nfv  1607  alimdv  1609  eximdv  1610  albidv  1613  exbidv  1614  alrimiv  1619  alrimdv  1621  spimvw  1642  equid  1647  spnfwOLD  1661  spw  1663  19.3v  1665  alcomiw  1681  hbn1w  1683  ax11wlem  1697  sp  1719  dvelimfALT2  1739  ax12olem1  1872  ax12olem2  1873  ax12olem6  1877  ax10lem2  1881  dvelimv  1883  a16gALT  1889  ax11a2  1938  cleljust  1961  dvelim  1963  ax16ALT  2037  dvelimALT  2077  ax17o  2100  dveeq2-o  2127  dveeq1-o  2130  ax11el  2136  ax11a2-o  2144  eujustALT  2149  cleqh  2383  abeq2  2391  mpteq12  4102  gsumdixp  15388  stoweidlem35  27185  alrim3con13v  27569  a9e2nd  27597  ax172  27616  19.21a3con13vVD  27898  tratrbVD  27907  ssralv2VD  27912  a9e2ndVD  27954  a9e2ndALT  27977  bnj1096  28083  bnj1350  28127  bnj1351  28128  bnj1352  28129  bnj1468  28147  bnj1000  28242  bnj1311  28323  bnj1445  28343  bnj1523  28370  equvinv  28383  equveliv  28384  a12study4  28386  a12study5rev  28391  ax10lem17ALT  28392  dvelimfALT2OLD  28394  a12study2  28403  a12study10  28405  a12study10n  28406  ax9lem1  28409  ax9lem3  28411  ax9lem6  28414  ax9lem14  28422  ax9lem15  28423  ax9lem17  28425  ax9vax9  28427
  Copyright terms: Public domain W3C validator