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

Axiom ax-5 1644
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 ax5ALT 2267 about the logical redundancy of ax-5 1644 in the presence of our obsolete axioms.)

This axiom essentially says that if does not occur in , i.e. does not depend on in any way, then we can add the quantifier A. to with no further assumptions. By sp 1770, we can also remove the quantifier (unconditionally). (Contributed by NM, 5-Aug-1993.)

Assertion
Ref Expression
ax-5
Distinct variable group:   ,

Detailed syntax breakdown of Axiom ax-5
StepHypRef Expression
1 wph . 2
2 vx . . 3
31, 2wal 1564 . 2
41, 3wi 4 1
Colors of variables: wff set class
This axiom is referenced by:  a5d  1645  ax5e  1646  nfv  1647  alimdv  1649  eximdv  1650  albidv  1653  exbidv  1654  alrimiv  1659  alrimdv  1661  19.9v  1694  spimvw  1699  spw  1719  spwOLD  1720  cbvalvw  1722  alcomiw  1725  hbn1w  1728  ax12wlem  1742  19.8a  1769  dvelimhwOLD  1880  axc9lem1OLD  2017  axc9lem6OLD  2022  axc11nlem2OLD  2031  dvelimvOLD  2033  axc16g  2052  a16gOLD  2055  dvelim  2081  dvelimv  2082  ax12a2  2088  cleljust  2113  axc16ALT  2164  ax12vALT  2190  dvelimALT  2242  ax5ALT  2267  dveeq2-o  2294  dveeq1-o  2296  ax12el  2303  ax12a2-o  2311  eujustALT  2316  cleqh  2586  abeq2  2594  mpteq12  4397  mpt2bi123f  28118  mptbi12f  28122  stoweidlem35  29009  eu2ndop1stv  29205  alrim3con13v  30085  a6e2nd  30113  ax52  30134  19.21a3con13vVD  30434  tratrbVD  30443  ssralv2VD  30448  a6e2ndVD  30490  a6e2ndALT  30512  bnj1096  30623  bnj1350  30667  bnj1351  30668  bnj1352  30669  bnj1468  30687  bnj1000  30782  bnj1311  30863  bnj1445  30883  bnj1523  30910  dvelimhwNEW11  31007  axc9lem2wAUX11  31008  axc9lem6NEW11  31011  dvelimvNEW11  31014  dvelimwAUX11  31019  ax12a2NEW11  31083  a16gNEW11  31098  cleljustNEW11  31178  axc16ALTNEW11  31186  dvelimALTNEW11  31187  axc9lem2OLD11  31257  dvelimOLD11  31290
  Copyright terms: Public domain W3C validator