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

Theorem ax6e 2383
Description: At least one individual exists. This is not a theorem of free logic, which is sound in empty domains. For such a logic, we would add this theorem as an axiom of set theory (Axiom 0 of [Kunen] p. 10). In the system consisting of ax-4 1812 through ax-9 2117, all axioms other than ax-6 1972 are believed to be theorems of free logic, although the system without ax-6 1972 is not complete in free logic.

Usage of this theorem is discouraged because it depends on ax-13 2372. It is preferred to use ax6ev 1974 when it is sufficient. (Contributed by NM, 14-May-1993.) Shortened after ax13lem1 2374 became available. (Revised by Wolf Lammen, 8-Sep-2018.) (New usage is discouraged.)

Assertion
Ref Expression
ax6e 𝑥 𝑥 = 𝑦

Proof of Theorem ax6e
Dummy variable 𝑤 is distinct from all other variables.
StepHypRef Expression
1 19.8a 2175 . 2 (𝑥 = 𝑦 → ∃𝑥 𝑥 = 𝑦)
2 ax13lem1 2374 . . . 4 𝑥 = 𝑦 → (𝑤 = 𝑦 → ∀𝑥 𝑤 = 𝑦))
3 ax6ev 1974 . . . . . 6 𝑥 𝑥 = 𝑤
4 equtr 2025 . . . . . 6 (𝑥 = 𝑤 → (𝑤 = 𝑦𝑥 = 𝑦))
53, 4eximii 1840 . . . . 5 𝑥(𝑤 = 𝑦𝑥 = 𝑦)
6519.35i 1882 . . . 4 (∀𝑥 𝑤 = 𝑦 → ∃𝑥 𝑥 = 𝑦)
72, 6syl6com 37 . . 3 (𝑤 = 𝑦 → (¬ 𝑥 = 𝑦 → ∃𝑥 𝑥 = 𝑦))
8 ax6ev 1974 . . 3 𝑤 𝑤 = 𝑦
97, 8exlimiiv 1935 . 2 𝑥 = 𝑦 → ∃𝑥 𝑥 = 𝑦)
101, 9pm2.61i 182 1 𝑥 𝑥 = 𝑦
Colors of variables: wff setvar class
Syntax hints:  ¬ wn 3  wi 4  wal 1540  wex 1782
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1798  ax-4 1812  ax-5 1914  ax-6 1972  ax-7 2012  ax-12 2172  ax-13 2372
This theorem depends on definitions:  df-bi 206  df-an 398  df-ex 1783
This theorem is referenced by:  ax6  2384  spimt  2386  spim  2387  spimed  2388  spimvALT  2391  spei  2394  equs4  2416  equsal  2417  equsexALT  2419  equvini  2455  equvel  2456  2ax6elem  2470  axi9  2700  dtrucor2  5371  axextnd  10586  ax8dfeq  34770  bj-axc10  35661  bj-alequex  35662  ax6er  35711  exlimiieq1  35712  wl-exeq  36403  wl-equsald  36408  ax6e2nd  43319  ax6e2ndVD  43669  ax6e2ndALT  43691  spd  47723
  Copyright terms: Public domain W3C validator