Theorem ax6e 2390

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

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

Syntax hints:  ¬ wn 3   → wi 4  ∀wal 1536  ∃wex 1781

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1797  ax-4 1811  ax-5 1911  ax-6 1970  ax-7 2015  ax-12 2175  ax-13 2379

This theorem depends on definitions:  df-bi 210  df-an 400  df-ex 1782

This theorem is referenced by:  ax6  2391  spimt  2393  spim  2394  spimed  2395  spimvALT  2398  spei  2401  equs4  2427  equsal  2428  equsexALT  2430  equvini  2466  equviniOLD  2467  equvel  2468  2ax6elem  2482  axi9  2766  dtrucor2  5238  axextnd  10002  ax8dfeq  33156  bj-axc10  34220  bj-alequex  34221  ax6er  34271  exlimiieq1  34272  wl-exeq  34939  wl-equsald  34944  ax6e2nd  41264  ax6e2ndVD  41614  ax6e2ndALT  41636  spd  45208