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

Axiom ax-5 1704
 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 2236 about the logical redundancy of ax-5 1704 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.x to with no further assumptions. By sp 1859, we can also remove the quantifier (unconditionally). (Contributed by NM, 10-Jan-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 1393 . 2
41, 3wi 4 1
 Colors of variables: wff setvar class This axiom is referenced by:  ax5d  1705  ax5e  1706  nfv  1707  alimdv  1709  eximdv  1710  albidv  1713  exbidv  1714  alrimiv  1719  alrimdv  1721  19.21v  1729  19.8v  1753  19.23v  1760  spimvw  1784  spw  1807  cbvalvw  1809  alcomiw  1811  hbn1w  1813  ax12wlem  1828  ax12v  1855  ax12vOLD  1856  19.8aOLD  1858  axc16g  1940  axc16gOLD  2061  dvelim  2079  dvelimv  2080  axc16ALT  2105  cleljust  2109  ax5ALT  2236  dveeq2-o  2263  dveeq1-o  2265  ax12el  2272  ax12a2-o  2280  eujustALT  2285  mo2vOLD  2290  mo2vOLDOLD  2291  cleqhOLD  2573  abeq2  2581  ralrimiv  2869  mpteq12  4531  wl-nfalv  29977  mpt2bi123f  30571  mptbi12f  30575  stoweidlem35  31817  eu2ndop1stv  32207  alrim3con13v  33304  ax6e2nd  33331  19.21a3con13vVD  33652  tratrbVD  33661  ssralv2VD  33666  ax6e2ndVD  33708  ax6e2ndALT  33730  bnj1096  33841  bnj1350  33884  bnj1351  33885  bnj1352  33886  bnj1468  33904  bnj1000  33999  bnj1311  34080  bnj1445  34100  bnj1523  34127  bj-nfv  34227  bj-ax12wlem  34228  bj-spimevw  34230  bj-cbvexivw  34233  bj-axc11nv  34316  bj-axc16g  34321  bj-axc15v  34330  bj-cleljust  34344  bj-cleqh  34358  bj-abeq2  34359  bj-abtru  34473  bj-abfal  34474  intimasn  37771
 Copyright terms: Public domain W3C validator