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 1713 through ax-9 1947, all axioms other than ax-6 1838 are believed to be theorems of free logic, although the system without ax-6 1838 is not complete in free logic.

It is preferred to use ax6ev 1840 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 1840 . . . . . 6 𝑥 𝑥 = 𝑤
4 equtr 1898 . . . . . 6 (𝑥 = 𝑤 → (𝑤 = 𝑦𝑥 = 𝑦))
53, 4eximii 1742 . . . . 5 𝑥(𝑤 = 𝑦𝑥 = 𝑦)
6519.35i 1776 . . . 4 (∀𝑥 𝑤 = 𝑦 → ∃𝑥 𝑥 = 𝑦)
72, 6syl6com 36 . . 3 (𝑤 = 𝑦 → (¬ 𝑥 = 𝑦 → ∃𝑥 𝑥 = 𝑦))
8 ax6ev 1840 . . 3 𝑤 𝑤 = 𝑦
97, 8exlimiiv 1812 . 2 𝑥 = 𝑦 → ∃𝑥 𝑥 = 𝑦)
101, 9pm2.61i 174 1 𝑥 𝑥 = 𝑦
Colors of variables: wff setvar class
Syntax hints:  ¬ wn 3  wi 4  wal 1472  wex 1694
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1700  ax-4 1713  ax-5 1793  ax-6 1838  ax-7 1885  ax-12 1983  ax-13 2137
This theorem depends on definitions:  df-bi 195  df-an 384  df-ex 1695
This theorem is referenced by:  ax6  2142  spimt  2144  spim  2145  spimed  2146  spimv  2148  spei  2152  equs4  2181  equsal  2182  equsexALT  2185  equvini  2238  equvel  2239  2ax6elem  2341  axi9  2490  dtrucor2  4727  axextnd  9167  ax8dfeq  30791  bj-axc10  31729  bj-alequex  31730  ax6er  31850  exlimiieq1  31851  wl-exeq  32374  wl-equsald  32379  ax6e2nd  37677  ax6e2ndVD  38048  ax6e2ndALT  38070
  Copyright terms: Public domain W3C validator