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

Axiom ax-5 1636
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 2259 about the logical redundancy of ax-5 1636 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 1762, 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 1556 . 2
41, 3wi 4 1
Colors of variables: wff set class
This axiom is referenced by:  a5d  1637  ax5e  1638  nfv  1639  alimdv  1641  eximdv  1642  albidv  1645  exbidv  1646  alrimiv  1651  alrimdv  1653  19.9v  1686  spimvw  1691  spw  1711  spwOLD  1712  cbvalvw  1714  alcomiw  1717  hbn1w  1720  ax12wlem  1734  19.8a  1761  dvelimhwOLD  1872  axc9lem1OLD  2009  axc9lem6OLD  2014  axc11nlem2OLD  2023  dvelimvOLD  2025  axc16g  2044  a16gOLD  2047  dvelim  2073  dvelimv  2074  ax12a2  2080  cleljust  2105  axc16ALT  2156  ax12vALT  2182  dvelimALT  2234  ax5ALT  2259  dveeq2-o  2286  dveeq1-o  2288  ax12el  2295  ax12a2-o  2303  eujustALT  2308  cleqh  2578  abeq2  2586  mpteq12  4381  mpt2bi123f  27609  mptbi12f  27613  stoweidlem35  28684  eu2ndop1stv  28880  alrim3con13v  29808  a6e2nd  29836  ax52  29857  19.21a3con13vVD  30157  tratrbVD  30166  ssralv2VD  30171  a6e2ndVD  30213  a6e2ndALT  30235  bnj1096  30346  bnj1350  30390  bnj1351  30391  bnj1352  30392  bnj1468  30410  bnj1000  30505  bnj1311  30586  bnj1445  30606  bnj1523  30633  dvelimhwNEW11  30730  axc9lem2wAUX11  30731  axc9lem6NEW11  30734  dvelimvNEW11  30737  dvelimwAUX11  30742  ax12a2NEW11  30806  a16gNEW11  30821  cleljustNEW11  30901  axc16ALTNEW11  30909  dvelimALTNEW11  30910  axc9lem2OLD11  30980  dvelimOLD11  31013
  Copyright terms: Public domain W3C validator