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

Axiom ax-17 1626
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 2233 about the logical redundancy of ax-17 1626 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 1763, 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 1549 . 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  1627  ax17e  1628  nfv  1629  alimdv  1631  eximdv  1632  albidv  1635  exbidv  1636  alrimiv  1641  alrimdv  1643  19.9v  1676  spimvw  1681  equidOLD  1689  spnfwOLD  1704  spw  1706  spwOLD  1707  19.3vOLD  1709  cbvalvw  1715  alcomiw  1718  hbn1w  1721  ax11wlem  1735  19.8a  1762  spOLD  1764  dvelimhwOLD  1877  ax12olem1OLD  2011  ax12olem6OLD  2016  ax10lem2OLD  2026  dvelimvOLD  2028  a16g  2048  a16gOLD  2049  dvelim  2069  dvelimv  2070  ax11a2  2076  cleljust  2097  ax16ALT  2131  ax11vALT  2172  dvelimALT  2209  ax17o  2233  dveeq2-o  2260  dveeq1-o  2263  ax11el  2270  ax11a2-o  2278  eujustALT  2283  cleqh  2532  abeq2  2540  mpteq12  4280  stoweidlem35  27751  eu2ndop1stv  27947  alrim3con13v  28554  a9e2nd  28582  ax172  28603  19.21a3con13vVD  28901  tratrbVD  28910  ssralv2VD  28915  a9e2ndVD  28957  a9e2ndALT  28979  bnj1096  29090  bnj1350  29134  bnj1351  29135  bnj1352  29136  bnj1468  29154  bnj1000  29249  bnj1311  29330  bnj1445  29350  bnj1523  29377  dvelimhwNEW7  29392  ax12olem2wAUX7  29393  ax12olem6NEW7  29396  dvelimvNEW7  29399  dvelimwAUX7  29404  ax11a2NEW7  29468  a16gNEW7  29483  cleljustNEW7  29564  ax16ALTNEW7  29572  dvelimALTNEW7  29573  ax12olem2OLD7  29643  dvelimOLD7  29676
  Copyright terms: Public domain W3C validator