Theorem ax6e 2383

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

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

Syntax hints:  ¬ wn 3   → wi 4  ∀wal 1537  ∃wex 1782

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1798  ax-4 1812  ax-5 1913  ax-6 1971  ax-7 2011  ax-12 2171  ax-13 2372

This theorem depends on definitions:  df-bi 206  df-an 397  df-ex 1783

This theorem is referenced by:  ax6  2384  spimt  2386  spim  2387  spimed  2388  spimvALT  2391  spei  2394  equs4  2416  equsal  2417  equsexALT  2419  equvini  2455  equvel  2456  2ax6elem  2470  axi9  2705  dtrucor2  5295  axextnd  10347  ax8dfeq  33774  bj-axc10  34965  bj-alequex  34966  ax6er  35016  exlimiieq1  35017  wl-exeq  35693  wl-equsald  35698  ax6e2nd  42178  ax6e2ndVD  42528  ax6e2ndALT  42550  spd  46384