Theorem ax6e 2387

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

Usage of this theorem is discouraged because it depends on ax-13 2376. It is preferred to use ax6ev 1970 when it is sufficient. (Contributed by NM, 14-May-1993.) Shortened after ax13lem1 2378 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 2188	. 2 ⊢ (𝑥 = 𝑦 → ∃𝑥 𝑥 = 𝑦)
2		ax13lem1 2378	. . . 4 ⊢ (¬ 𝑥 = 𝑦 → (𝑤 = 𝑦 → ∀𝑥 𝑤 = 𝑦))
3		ax6ev 1970	. . . . . 6 ⊢ ∃𝑥 𝑥 = 𝑤
4		equtr 2022	. . . . . 6 ⊢ (𝑥 = 𝑤 → (𝑤 = 𝑦 → 𝑥 = 𝑦))
5	3, 4	eximii 1838	. . . . 5 ⊢ ∃𝑥(𝑤 = 𝑦 → 𝑥 = 𝑦)
6	5	19.35i 1879	. . . 4 ⊢ (∀𝑥 𝑤 = 𝑦 → ∃𝑥 𝑥 = 𝑦)
7	2, 6	syl6com 37	. . 3 ⊢ (𝑤 = 𝑦 → (¬ 𝑥 = 𝑦 → ∃𝑥 𝑥 = 𝑦))
8		ax6ev 1970	. . 3 ⊢ ∃𝑤 𝑤 = 𝑦
9	7, 8	exlimiiv 1932	. 2 ⊢ (¬ 𝑥 = 𝑦 → ∃𝑥 𝑥 = 𝑦)
10	1, 9	pm2.61i 182	1 ⊢ ∃𝑥 𝑥 = 𝑦

Syntax hints:  ¬ wn 3   → wi 4  ∀wal 1539  ∃wex 1780

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1796  ax-4 1810  ax-5 1911  ax-6 1968  ax-7 2009  ax-12 2184  ax-13 2376

This theorem depends on definitions:  df-bi 207  df-an 396  df-ex 1781

This theorem is referenced by:  ax6  2388  spimt  2390  spim  2391  spimed  2392  spimvALT  2395  spei  2398  equs4  2420  equsal  2421  equsexALT  2423  equvini  2459  equvel  2460  2ax6elem  2474  axi9  2704  dtrucor2  5317  axextnd  10502  ax8dfeq  35990  bj-axc10  36984  bj-alequex  36985  ax6er  37034  exlimiieq1  37035  wl-exeq  37735  wl-equsald  37740  ax6e2nd  44795  ax6e2ndVD  45144  ax6e2ndALT  45166  spd  49919