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 1839 through ax-9 2153, all axioms other than ax-6 1997 are believed to be theorems of free logic, although the system without ax-6 1997 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 1999 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 2217	. 2 ⊢ (𝑥 = 𝑦 → ∃𝑥 𝑥 = 𝑦)
2		ax13lem1 2406	. . . 4 ⊢ (¬ 𝑥 = 𝑦 → (𝑤 = 𝑦 → ∀𝑥 𝑤 = 𝑦))
3		ax6ev 1999	. . . . . 6 ⊢ ∃𝑥 𝑥 = 𝑤
4		equtr 2051	. . . . . 6 ⊢ (𝑥 = 𝑤 → (𝑤 = 𝑦 → 𝑥 = 𝑦))
5	3, 4	eximii 1867	. . . . 5 ⊢ ∃𝑥(𝑤 = 𝑦 → 𝑥 = 𝑦)
6	5	19.35i 1908	. . . 4 ⊢ (∀𝑥 𝑤 = 𝑦 → ∃𝑥 𝑥 = 𝑦)
7	2, 6	syl6com 38	. . 3 ⊢ (𝑤 = 𝑦 → (¬ 𝑥 = 𝑦 → ∃𝑥 𝑥 = 𝑦))
8		ax6ev 1999	. . 3 ⊢ ∃𝑤 𝑤 = 𝑦
9	7, 8	exlimiiv 1961	. 2 ⊢ (¬ 𝑥 = 𝑦 → ∃𝑥 𝑥 = 𝑦)
10	1, 9	pm2.61i 184	1 ⊢ ∃𝑥 𝑥 = 𝑦

Syntax hints:  ¬ wn 3   → wi 4  ∀wal 1568  ∃wex 1809

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1825  ax-4 1839  ax-5 1940  ax-6 1997  ax-7 2038  ax-12 2213  ax-13 2404

This theorem depends on definitions:  df-bi 210  df-an 401  df-ex 1810

This theorem is referenced 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  5345  axextnd  10577  ax8dfeq  36269  bj-axc10  37399  bj-alequex  37400  ax6er  37449  exlimiieq1  37450  wl-exeq  38170  wl-equsald  38175  ax6e2nd  45250  ax6e2ndVD  45599  ax6e2ndALT  45621  spd  50439