Theorem ax6e 2391

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

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

Syntax hints:  ¬ wn 3   → wi 4  ∀wal 1545  ∃wex 1786

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1802  ax-4 1816  ax-5 1917  ax-6 1974  ax-7 2015  ax-12 2189  ax-13 2380

This theorem depends on definitions:  df-bi 208  df-an 397  df-ex 1787

This theorem is referenced by:  ax6  2392  spimt  2394  spim  2395  spimed  2396  spimvALT  2399  spei  2402  equs4  2424  equsal  2425  equsexALT  2427  equvini  2463  equvel  2464  2ax6elem  2478  axi9  2708  dtrucor2  5308  axextnd  10512  ax8dfeq  36031  bj-axc10  37143  bj-alequex  37144  ax6er  37193  exlimiieq1  37194  wl-exeq  37912  wl-equsald  37917  ax6e2nd  45009  ax6e2ndVD  45358  ax6e2ndALT  45380  spd  50175