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 1902
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 35925 about the logical redundancy of ax-5 1902 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 2172, we can also remove the quantifier (unconditionally).

For an explanation of disjoint variable conditions, see https://us.metamath.org/mpeuni/mmset.html#distinct 2172. (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 1526 . 2 wff 𝑥𝜑
41, 3wi 4 1 wff (𝜑 → ∀𝑥𝜑)
Colors of variables: wff setvar class
This axiom is referenced by:  ax5d  1903  ax5e  1904  ax5ea  1905  alimdv  1908  eximdv  1909  albidv  1912  exbidv  1913  alrimiv  1919  alrimdv  1921  nexdv  1928  stdpc5v  1930  19.23v  1934  19.37imv  1939  spvw  1976  19.3v  1977  19.8v  1978  spimevw  1992  spimvw  1993  spw  2032  cbvalvw  2034  alcomiw  2041  alcomiwOLD  2042  hbn1w  2044  naev2  2057  sbv  2089  ax12wlem  2127  nf5dv  2143  ax12v  2168  cleljustALT  2375  cbvalvOLD  2414  dvelim  2468  dvelimv  2469  axc16ALT  2524  eujustALT  2653  abeq2  2945  ralrimiv  3181  mpteq12  5145  hashgt23el  13775  bnj1096  31954  bnj1350  31997  bnj1351  31998  bnj1352  31999  bnj1468  32018  bnj1000  32113  bnj1311  32194  bnj1445  32214  bnj1523  32241  umgr2cycllem  32285  umgr2cycl  32286  bj-ax12wlem  33875  bj-cbvalim  33876  bj-cbvexim  33877  bj-cbvexivw  33903  bj-ax12v3  33917  bj-ax12v3ALT  33918  bj-nnfv  33981  bj-abv  34121  bj-ab0  34122  copsex2b  34325  opelopabbv  34328  brabd  34333  fvineqsnf1  34574  wl-nfalv  34648  mpobi123f  35323  mptbi12f  35327  ax5ALT  35925  dveeq2-o  35951  dveeq1-o  35953  ax12el  35960  ax12a2-o  35968  intimasn  39882  alrim3con13v  40747  ax6e2nd  40772  19.21a3con13vVD  41066  tratrbVD  41075  ssralv2VD  41080  ax6e2ndVD  41122  ax6e2ndALT  41144  stoweidlem35  42201  eu2ndop1stv  43205
  Copyright terms: Public domain W3C validator