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 1976
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 34665 about the logical redundancy of ax-5 1976 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 2188, 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 1618 . 2 wff 𝑥𝜑
41, 3wi 4 1 wff (𝜑 → ∀𝑥𝜑)
Colors of variables: wff setvar class
This axiom is referenced by:  ax5d  1977  ax5e  1978  ax5ea  1979  alimdv  1982  eximdv  1983  albidv  1986  exbidv  1987  alrimiv  1992  alrimdv  1994  nexdv  2001  stdpc5v  2004  19.23v  2008  19.37imv  2012  nfvOLD  2025  19.8v  2049  19.23vOLD  2056  spimvw  2070  spw  2106  cbvalvw  2108  alcomiw  2110  hbn1w  2112  ax12wlem  2146  ax12v  2185  axc16gOLD  2295  cleljustALT  2318  cbvalv  2406  dvelim  2465  dvelimv  2466  axc16ALT  2491  eujustALT  2598  abeq2  2858  ralrimiv  3091  mpteq12  4876  bnj1096  31131  bnj1350  31174  bnj1351  31175  bnj1352  31176  bnj1468  31194  bnj1000  31289  bnj1311  31370  bnj1445  31390  bnj1523  31417  bj-ax12wlem  32894  bj-spimevw  32934  bj-cbvexivw  32937  bj-ax12v3  32952  bj-ax12v3ALT  32953  bj-sbfvv  33042  bj-abeq2  33050  bj-abv  33178  bj-ab0  33179  wl-hbnaev  33587  wl-nfalv  33594  mpt2bi123f  34253  mptbi12f  34257  ax5ALT  34665  dveeq2-o  34691  dveeq1-o  34693  ax12el  34700  ax12a2-o  34708  intimasn  38420  alrim3con13v  39214  ax6e2nd  39245  19.21a3con13vVD  39555  tratrbVD  39565  ssralv2VD  39570  ax6e2ndVD  39612  ax6e2ndALT  39634  stoweidlem35  40724  eu2ndop1stv  41677
  Copyright terms: Public domain W3C validator