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

Axiom ax-17 1606
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 2109 about the logical redundancy of ax-17 1606 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 1728, 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 1530 . 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  1607  ax17e  1608  nfv  1609  alimdv  1611  eximdv  1612  albidv  1615  exbidv  1616  alrimiv  1621  alrimdv  1623  19.9v  1653  spimvw  1657  equid  1662  spnfwOLD  1677  spw  1679  19.3vOLD  1681  alcomiw  1690  hbn1w  1692  ax11wlem  1706  sp  1728  dvelimhw  1747  ax12olem1  1880  ax12olem2  1881  ax12olem6  1885  ax10lem2  1890  dvelimv  1892  a16g  1898  ax11a2  1946  cleljust  1967  dvelim  1969  ax16ALT  2000  dvelimALT  2085  ax17o  2109  dveeq2-o  2136  dveeq1-o  2139  ax11el  2146  ax11a2-o  2154  eujustALT  2159  cleqh  2393  abeq2  2401  mpteq12  4115  gsumdixp  15408  disjorf  23371  stoweidlem35  27887  eu2ndop1stv  28083  alrim3con13v  28595  a9e2nd  28623  ax172  28642  19.21a3con13vVD  28944  tratrbVD  28953  ssralv2VD  28958  a9e2ndVD  29000  a9e2ndALT  29023  bnj1096  29130  bnj1350  29174  bnj1351  29175  bnj1352  29176  bnj1468  29194  bnj1000  29289  bnj1311  29370  bnj1445  29390  bnj1523  29417  dvelimhwNEW7  29432  ax12olem2wAUX7  29433  ax12olem6NEW7  29436  dvelimvNEW7  29439  dvelimwAUX7  29444  ax11a2NEW7  29506  a16gNEW7  29521  cleljustNEW7  29599  ax16ALTNEW7  29607  ax12olem2OLD7  29660  dvelimOLD7  29693  equvinv  29736  equveliv  29737  a12study4  29739  a12study5rev  29744  ax10lem17ALT  29745  dvelimfALT2OLD  29747  a12study2  29756  a12study10  29758  a12study10n  29759  ax9lem1  29762  ax9lem3  29764  ax9lem6  29767  ax9lem14  29775  ax9lem15  29776  ax9lem17  29778  ax9vax9  29780
  Copyright terms: Public domain W3C validator