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

Axiom ax-5 1793
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 33085 about the logical redundancy of ax-5 1793 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 𝑥 to 𝜑 with no further assumptions. By sp 1990, 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 wff 𝜑
2 vx . . 3 setvar 𝑥
31, 2wal 1472 . 2 wff 𝑥𝜑
41, 3wi 4 1 wff (𝜑 → ∀𝑥𝜑)
Colors of variables: wff setvar class
This axiom is referenced by:  ax5d  1794  ax5e  1795  nfv  1796  alimdv  1798  eximdv  1799  albidv  1802  exbidv  1803  alrimiv  1808  alrimdv  1810  stdpc5v  1820  19.8v  1845  19.23v  1852  spimvw  1877  spw  1916  cbvalvw  1918  alcomiw  1920  hbn1w  1922  ax12wlem  1957  ax12v  1984  ax12vOLD  1986  ax12vOLDOLD  1987  axc16g  2071  cleljustALT  2134  dvelim  2229  dvelimv  2230  axc16ALT  2258  eujustALT  2365  abeq2  2623  ralrimiv  2852  mpteq12  4562  bnj1096  29953  bnj1350  29996  bnj1351  29997  bnj1352  29998  bnj1468  30016  bnj1000  30111  bnj1311  30192  bnj1445  30212  bnj1523  30239  bj-ax5ea  31640  bj-ax12wlem  31642  bj-spimevw  31679  bj-cbvexivw  31682  bj-ax12v3  31697  bj-ax12v3ALT  31698  bj-axc15v  31776  bj-sbfvv  31792  bj-abeq2  31803  bj-abv  31925  bj-ab0  31926  wl-nfv  32316  wl-hbnaev  32358  wl-nfalv  32365  mpt2bi123f  33016  mptbi12f  33020  ax5ALT  33085  dveeq2-o  33111  dveeq1-o  33113  ax12el  33120  ax12a2-o  33128  intimasn  36850  alrim3con13v  37646  ax6e2nd  37677  19.21a3con13vVD  37991  tratrbVD  38001  ssralv2VD  38006  ax6e2ndVD  38048  ax6e2ndALT  38070  stoweidlem35  38818  eu2ndop1stv  39745
  Copyright terms: Public domain W3C validator