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 1816 through ax-9 2124, all axioms other than ax-6 1975 are believed to be theorems of free logic, although the system without ax-6 1975 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 1977 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 2182 . 2 (𝑥 = 𝑦 → ∃𝑥 𝑥 = 𝑦)
2 ax13lem1 2374 . . . 4 𝑥 = 𝑦 → (𝑤 = 𝑦 → ∀𝑥 𝑤 = 𝑦))
3 ax6ev 1977 . . . . . 6 𝑥 𝑥 = 𝑤
4 equtr 2033 . . . . . 6 (𝑥 = 𝑤 → (𝑤 = 𝑦𝑥 = 𝑦))
53, 4eximii 1843 . . . . 5 𝑥(𝑤 = 𝑦𝑥 = 𝑦)
6519.35i 1885 . . . 4 (∀𝑥 𝑤 = 𝑦 → ∃𝑥 𝑥 = 𝑦)
72, 6syl6com 37 . . 3 (𝑤 = 𝑦 → (¬ 𝑥 = 𝑦 → ∃𝑥 𝑥 = 𝑦))
8 ax6ev 1977 . . 3 𝑤 𝑤 = 𝑦
97, 8exlimiiv 1938 . 2 𝑥 = 𝑦 → ∃𝑥 𝑥 = 𝑦)
101, 9pm2.61i 185 1 𝑥 𝑥 = 𝑦
Colors of variables: wff setvar class
Syntax hints:  ¬ wn 3  wi 4  wal 1540  wex 1786
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1802  ax-4 1816  ax-5 1917  ax-6 1975  ax-7 2020  ax-12 2179  ax-13 2372
This theorem depends on definitions:  df-bi 210  df-an 400  df-ex 1787
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  2706  dtrucor2  5239  axextnd  10091  ax8dfeq  33346  bj-axc10  34596  bj-alequex  34597  ax6er  34647  exlimiieq1  34648  wl-exeq  35316  wl-equsald  35321  ax6e2nd  41716  ax6e2ndVD  42066  ax6e2ndALT  42088  spd  45837
  Copyright terms: Public domain W3C validator