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

Theorem ax6e 2237
 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 1727 through ax-9 1985, all axioms other than ax-6 1874 are believed to be theorems of free logic, although the system without ax-6 1874 is not complete in free logic. It is preferred to use ax6ev 1876 when it is sufficient. (Contributed by NM, 14-May-1993.) Shortened after ax13lem1 2235 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 2038 . 2 (𝑥 = 𝑦 → ∃𝑥 𝑥 = 𝑦)
2 ax13lem1 2235 . . . 4 𝑥 = 𝑦 → (𝑤 = 𝑦 → ∀𝑥 𝑤 = 𝑦))
3 ax6ev 1876 . . . . . 6 𝑥 𝑥 = 𝑤
4 equtr 1934 . . . . . 6 (𝑥 = 𝑤 → (𝑤 = 𝑦𝑥 = 𝑦))
53, 4eximii 1753 . . . . 5 𝑥(𝑤 = 𝑦𝑥 = 𝑦)
6519.35i 1794 . . . 4 (∀𝑥 𝑤 = 𝑦 → ∃𝑥 𝑥 = 𝑦)
72, 6syl6com 36 . . 3 (𝑤 = 𝑦 → (¬ 𝑥 = 𝑦 → ∃𝑥 𝑥 = 𝑦))
8 ax6ev 1876 . . 3 𝑤 𝑤 = 𝑦
97, 8exlimiiv 1845 . 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 1712  ax-4 1727  ax-5 1826  ax-6 1874  ax-7 1921  ax-12 2033  ax-13 2233 This theorem depends on definitions:  df-bi 195  df-an 384  df-ex 1695 This theorem is referenced by:  ax6  2238  spimt  2240  spim  2241  spimed  2242  spimv  2244  spei  2248  equs4  2277  equsal  2278  equsexALT  2281  equvini  2333  equvel  2334  2ax6elem  2436  axi9  2585  dtrucor2  4823  axextnd  9269  ax8dfeq  30754  bj-axc10  31700  bj-alequex  31701  ax6er  31814  exlimiieq1  31815  wl-exeq  32296  wl-equsald  32300  ax6e2nd  37591  ax6e2ndVD  37962  ax6e2ndALT  37984
 Copyright terms: Public domain W3C validator