Theorem ax6e 2418

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 2156, 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 2407. It is preferred to use ax6ev 2002 when it is sufficient. (Contributed by NM, 14-May-1993.) Shortened after ax13lem1 2409 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 2220	. 2 ⊢ (𝑥 = 𝑦 → ∃𝑥 𝑥 = 𝑦)
2		ax13lem1 2409	. . . 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 2216  ax-13 2407

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

This theorem is used by:  ax6  2419  spimt  2421  spim  2422  spimed  2423  spimvALT  2426  spei  2429  equs4  2451  equsal  2452  equsexALT  2454  equvini  2490  equvel  2491  2ax6elem  2505  axi9  2734  dtrucor2  5348  axextnd  10594  ax8dfeq  36309  bj-axc10  37459  bj-alequex  37460  ax6er  37509  exlimiieq1  37510  wl-exeq  38230  wl-equsald  38235  ax6e2nd  45308  ax6e2ndVD  45657  ax6e2ndALT  45679  spd  50497