Theorem ax6e 2412

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

Usage of this theorem is discouraged because it depends on ax-13 2401. It is preferred to use ax6ev 2001 when it is sufficient. (Contributed by NM, 14-May-1993.) Shortened after ax13lem1 2403 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 2217	. 2 ⊢ (𝑥 = 𝑦 → ∃𝑥 𝑥 = 𝑦)
2		ax13lem1 2403	. . . 4 ⊢ (¬ 𝑥 = 𝑦 → (𝑤 = 𝑦 → ∀𝑥 𝑤 = 𝑦))
3		ax6ev 2001	. . . . . 6 ⊢ ∃𝑥 𝑥 = 𝑤
4		equtr 2053	. . . . . 6 ⊢ (𝑥 = 𝑤 → (𝑤 = 𝑦 → 𝑥 = 𝑦))
5	3, 4	eximii 1869	. . . . 5 ⊢ ∃𝑥(𝑤 = 𝑦 → 𝑥 = 𝑦)
6	5	19.35i 1910	. . . 4 ⊢ (∀𝑥 𝑤 = 𝑦 → ∃𝑥 𝑥 = 𝑦)
7	2, 6	syl6com 38	. . 3 ⊢ (𝑤 = 𝑦 → (¬ 𝑥 = 𝑦 → ∃𝑥 𝑥 = 𝑦))
8		ax6ev 2001	. . 3 ⊢ ∃𝑤 𝑤 = 𝑦
9	7, 8	exlimiiv 1963	. 2 ⊢ (¬ 𝑥 = 𝑦 → ∃𝑥 𝑥 = 𝑦)
10	1, 9	pm2.61i 184	1 ⊢ ∃𝑥 𝑥 = 𝑦

This proof depends on syntax axioms:  ¬ wn 3   → wi 4  ∀wal 1567  ∃wex 1811

This proof depends on axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1827  ax-4 1841  ax-5 1942  ax-6 1999  ax-7 2040  ax-12 2212  ax-13 2401

This proof depends on definitions:  df-bi 210  df-an 402  df-ex 1812

This theorem is used by:  ax6  2413  spimt  2415  spim  2416  spimed  2417  spimvALT  2420  spei  2423  equs4  2445  equsal  2446  equsexALT  2448  equvini  2484  equvel  2485  2ax6elem  2499  axi9  2728  dtrucor2  5333  axextnd  10680  ax8dfeq  36653  bj-axc10  37788  bj-alequex  37789  ax6er  37838  exlimiieq1  37839  wl-exeq  38560  wl-equsald  38565  ax6e2nd  45635  ax6e2ndVD  45984  ax6e2ndALT  46006  spd  50955