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 2117, all axioms other than ax-6 1972 are believed to be theorems of free logic, although the system without ax-6 1972 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 1974 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.

Step	Hyp	Ref	Expression
1		19.8a 2175	. 2 ⊢ (𝑥 = 𝑦 → ∃𝑥 𝑥 = 𝑦)
2		ax13lem1 2374	. . . 4 ⊢ (¬ 𝑥 = 𝑦 → (𝑤 = 𝑦 → ∀𝑥 𝑤 = 𝑦))
3		ax6ev 1974	. . . . . 6 ⊢ ∃𝑥 𝑥 = 𝑤
4		equtr 2025	. . . . . 6 ⊢ (𝑥 = 𝑤 → (𝑤 = 𝑦 → 𝑥 = 𝑦))
5	3, 4	eximii 1840	. . . . 5 ⊢ ∃𝑥(𝑤 = 𝑦 → 𝑥 = 𝑦)
6	5	19.35i 1882	. . . 4 ⊢ (∀𝑥 𝑤 = 𝑦 → ∃𝑥 𝑥 = 𝑦)
7	2, 6	syl6com 37	. . 3 ⊢ (𝑤 = 𝑦 → (¬ 𝑥 = 𝑦 → ∃𝑥 𝑥 = 𝑦))
8		ax6ev 1974	. . 3 ⊢ ∃𝑤 𝑤 = 𝑦
9	7, 8	exlimiiv 1935	. 2 ⊢ (¬ 𝑥 = 𝑦 → ∃𝑥 𝑥 = 𝑦)
10	1, 9	pm2.61i 182	1 ⊢ ∃𝑥 𝑥 = 𝑦

Syntax hints:  ¬ wn 3   → wi 4  ∀wal 1540  ∃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 1914  ax-6 1972  ax-7 2012  ax-12 2172  ax-13 2372

This theorem depends on definitions:  df-bi 206  df-an 398  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  2700  dtrucor2  5366  axextnd  10573  ax8dfeq  34701  bj-axc10  35566  bj-alequex  35567  ax6er  35616  exlimiieq1  35617  wl-exeq  36308  wl-equsald  36313  ax6e2nd  43190  ax6e2ndVD  43540  ax6e2ndALT  43562  spd  47563