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

Theorem ax6e 2141
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 1711 through ax-9 1946, all axioms other than ax-6 1836 are believed to be theorems of free logic, although the system without ax-6 1836 is not complete in free logic.

It is preferred to use ax6ev 1838 when it is sufficient. (Contributed by NM, 14-May-1993.) Shortened after ax13lem1 2139 became available. (Revised by Wolf Lammen, 8-Sep-2018.)

Assertion
Ref Expression
ax6e 𝑥 𝑥 = 𝑦

Proof of Theorem ax6e
Dummy variable 𝑤 is distinct from all other variables.
StepHypRef Expression
1 19.8a 1988 . 2 (𝑥 = 𝑦 → ∃𝑥 𝑥 = 𝑦)
2 ax13lem1 2139 . . . 4 𝑥 = 𝑦 → (𝑤 = 𝑦 → ∀𝑥 𝑤 = 𝑦))
3 ax6ev 1838 . . . . . 6 𝑥 𝑥 = 𝑤
4 equtr 1897 . . . . . 6 (𝑥 = 𝑤 → (𝑤 = 𝑦𝑥 = 𝑦))
53, 4eximii 1740 . . . . 5 𝑥(𝑤 = 𝑦𝑥 = 𝑦)
6519.35i 1772 . . . 4 (∀𝑥 𝑤 = 𝑦 → ∃𝑥 𝑥 = 𝑦)
72, 6syl6com 36 . . 3 (𝑤 = 𝑦 → (¬ 𝑥 = 𝑦 → ∃𝑥 𝑥 = 𝑦))
8 ax6ev 1838 . . 3 𝑤 𝑤 = 𝑦
97, 8exlimiiv 1808 . 2 𝑥 = 𝑦 → ∃𝑥 𝑥 = 𝑦)
101, 9pm2.61i 171 1 𝑥 𝑥 = 𝑦
Colors of variables: wff setvar class
Syntax hints:  ¬ wn 3  wi 4  wal 1466  wex 1692
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1698  ax-4 1711  ax-5 1789  ax-6 1836  ax-7 1883  ax-12 1983  ax-13 2137
This theorem depends on definitions:  df-bi 192  df-an 380  df-ex 1693
This theorem is referenced by:  ax6  2142  spimt  2144  spim  2145  spimed  2146  spimv  2148  spei  2152  equs4  2174  equsal  2175  equsexALT  2178  equvini  2229  equvel  2230  2ax6elem  2332  axi9  2481  dtrucor2  4675  axextnd  9101  ax8dfeq  30596  bj-axc10  31495  bj-alequex  31496  ax6er  31617  exlimiieq1  31618  wl-exeq  32098  wl-equsald  32103  ax6e2nd  37281  ax6e2ndVD  37653  ax6e2ndALT  37675
  Copyright terms: Public domain W3C validator