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

For an explanation of disjoint variable conditions, see https://us.metamath.org/mpeuni/mmset.html#distinct 2181. (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 1534 . 2 wff 𝑥𝜑
41, 3wi 4 1 wff (𝜑 → ∀𝑥𝜑)
Colors of variables: wff setvar class
This axiom is referenced by:  ax5d  1911  ax5e  1912  ax5ea  1913  alimdv  1916  eximdv  1917  albidv  1920  exbidv  1921  alrimiv  1927  alrimdv  1929  nexdv  1936  stdpc5v  1938  19.23v  1942  19.37imv  1947  spvw  1984  19.3v  1985  19.8v  1986  spimevw  2000  spimvw  2001  spw  2040  cbvalvw  2042  alcomiw  2049  alcomiwOLD  2050  hbn1w  2052  naev2  2065  sbv  2097  ax12wlem  2135  nf5dv  2151  ax12v  2177  cleljustALT  2381  cbvalvOLD  2419  dvelim  2472  dvelimv  2473  axc16ALT  2527  eujustALT  2656  abeq2  2948  ralrimiv  3184  mpteq12  5156  hashgt23el  13788  bnj1096  32058  bnj1350  32101  bnj1351  32102  bnj1352  32103  bnj1468  32122  bnj1000  32217  bnj1311  32300  bnj1445  32320  bnj1523  32347  umgr2cycllem  32391  umgr2cycl  32392  bj-ax12wlem  33981  bj-cbvalim  33982  bj-cbvexim  33983  bj-cbvexivw  34009  bj-ax12v3  34023  bj-ax12v3ALT  34024  bj-nnfv  34087  bj-abv  34227  bj-ab0  34228  copsex2b  34436  opelopabbv  34439  brabd  34444  fvineqsnf1  34695  wl-nfalv  34769  mpobi123f  35444  mptbi12f  35448  ax5ALT  36047  dveeq2-o  36073  dveeq1-o  36075  ax12el  36082  ax12a2-o  36090  intimasn  40008  alrim3con13v  40873  ax6e2nd  40898  19.21a3con13vVD  41192  tratrbVD  41201  ssralv2VD  41206  ax6e2ndVD  41248  ax6e2ndALT  41270  stoweidlem35  42327  eu2ndop1stv  43331
  Copyright terms: Public domain W3C validator