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 2116, all axioms other than ax-6 1971 are believed to be theorems of free logic, although the system without ax-6 1971 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 1973 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 2174 . 2 (𝑥 = 𝑦 → ∃𝑥 𝑥 = 𝑦)
2 ax13lem1 2374 . . . 4 𝑥 = 𝑦 → (𝑤 = 𝑦 → ∀𝑥 𝑤 = 𝑦))
3 ax6ev 1973 . . . . . 6 𝑥 𝑥 = 𝑤
4 equtr 2024 . . . . . 6 (𝑥 = 𝑤 → (𝑤 = 𝑦𝑥 = 𝑦))
53, 4eximii 1839 . . . . 5 𝑥(𝑤 = 𝑦𝑥 = 𝑦)
6519.35i 1881 . . . 4 (∀𝑥 𝑤 = 𝑦 → ∃𝑥 𝑥 = 𝑦)
72, 6syl6com 37 . . 3 (𝑤 = 𝑦 → (¬ 𝑥 = 𝑦 → ∃𝑥 𝑥 = 𝑦))
8 ax6ev 1973 . . 3 𝑤 𝑤 = 𝑦
97, 8exlimiiv 1934 . 2 𝑥 = 𝑦 → ∃𝑥 𝑥 = 𝑦)
101, 9pm2.61i 182 1 𝑥 𝑥 = 𝑦
Colors of variables: wff setvar class
Syntax hints:  ¬ wn 3  wi 4  wal 1537  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 1913  ax-6 1971  ax-7 2011  ax-12 2171  ax-13 2372
This theorem depends on definitions:  df-bi 206  df-an 397  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  2705  dtrucor2  5295  axextnd  10347  ax8dfeq  33774  bj-axc10  34965  bj-alequex  34966  ax6er  35016  exlimiieq1  35017  wl-exeq  35693  wl-equsald  35698  ax6e2nd  42178  ax6e2ndVD  42528  ax6e2ndALT  42550  spd  46384
  Copyright terms: Public domain W3C validator