Theorem ax6e 2413

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

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

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

This proof depends on axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1828  ax-4 1842  ax-5 1943  ax-6 2000  ax-7 2041  ax-12 2213  ax-13 2402

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

This theorem is used by:  ax6  2414  spimt  2416  spim  2417  spimed  2418  spimvALT  2421  spei  2424  equs4  2446  equsal  2447  equsexALT  2449  equvini  2485  equvel  2486  2ax6elem  2500  axi9  2729  dtrucor2  5334  axextnd  10657  ax8dfeq  36530  bj-axc10  37665  bj-alequex  37666  ax6er  37715  exlimiieq1  37716  wl-exeq  38434  wl-equsald  38439  ax6e2nd  45500  ax6e2ndVD  45849  ax6e2ndALT  45871  spd  50730