Theorem ax6e 2415

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

Usage of this theorem is discouraged because it depends on ax-13 2404. It is preferred to use ax6ev 2004 when it is sufficient. (Contributed by NM, 14-May-1993.) Shortened after ax13lem1 2406 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 2221	. 2 ⊢ (𝑥 = 𝑦 → ∃𝑥 𝑥 = 𝑦)
2		ax13lem1 2406	. . . 4 ⊢ (¬ 𝑥 = 𝑦 → (𝑤 = 𝑦 → ∀𝑥 𝑤 = 𝑦))
3		ax6ev 2004	. . . . . 6 ⊢ ∃𝑥 𝑥 = 𝑤
4		equtr 2056	. . . . . 6 ⊢ (𝑥 = 𝑤 → (𝑤 = 𝑦 → 𝑥 = 𝑦))
5	3, 4	eximii 1870	. . . . 5 ⊢ ∃𝑥(𝑤 = 𝑦 → 𝑥 = 𝑦)
6	5	19.35i 1913	. . . 4 ⊢ (∀𝑥 𝑤 = 𝑦 → ∃𝑥 𝑥 = 𝑦)
7	2, 6	syl6com 38	. . 3 ⊢ (𝑤 = 𝑦 → (¬ 𝑥 = 𝑦 → ∃𝑥 𝑥 = 𝑦))
8		ax6ev 2004	. . 3 ⊢ ∃𝑤 𝑤 = 𝑦
9	7, 8	exlimiiv 1966	. 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 1945  ax-6 2002  ax-7 2043  ax-12 2216  ax-13 2404

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

This theorem is used by:  ax6  2416  spimt  2418  spim  2419  spimed  2420  spimvALT  2423  spei  2426  equs4  2448  equsal  2449  equsexALT  2451  equvini  2487  equvel  2488  2ax6elem  2502  axi9  2731  dtrucor2  5339  axextnd  10706  ax8dfeq  36751  bj-axc10  37886  bj-alequex  37887  ax6er  37936  exlimiieq1  37937  wl-exeq  38671  wl-equsald  38676  ax6e2nd  45743  ax6e2ndVD  46092  ax6e2ndALT  46114  spd  51076