Theorem ax6e 2404

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

It is preferred to use ax6ev 2079 when it is sufficient. (Contributed by NM, 14-May-1993.) Shortened after ax13lem1 2393 became available. (Revised by Wolf Lammen, 8-Sep-2018.)

Assertion

Ref	Expression
ax6e	⊢ ∃𝑥 𝑥 = 𝑦

Proof of Theorem ax6e

Dummy variable 𝑤 is distinct from all other variables.

Step	Hyp	Ref	Expression
1		19.8a 2225	. 2 ⊢ (𝑥 = 𝑦 → ∃𝑥 𝑥 = 𝑦)
2		ax13lem1 2393	. . . 4 ⊢ (¬ 𝑥 = 𝑦 → (𝑤 = 𝑦 → ∀𝑥 𝑤 = 𝑦))
3		ax6ev 2079	. . . . . 6 ⊢ ∃𝑥 𝑥 = 𝑤
4		equtr 2127	. . . . . 6 ⊢ (𝑥 = 𝑤 → (𝑤 = 𝑦 → 𝑥 = 𝑦))
5	3, 4	eximii 1937	. . . . 5 ⊢ ∃𝑥(𝑤 = 𝑦 → 𝑥 = 𝑦)
6	5	19.35i 1983	. . . 4 ⊢ (∀𝑥 𝑤 = 𝑦 → ∃𝑥 𝑥 = 𝑦)
7	2, 6	syl6com 37	. . 3 ⊢ (𝑤 = 𝑦 → (¬ 𝑥 = 𝑦 → ∃𝑥 𝑥 = 𝑦))
8		ax6ev 2079	. . 3 ⊢ ∃𝑤 𝑤 = 𝑦
9	7, 8	exlimiiv 2032	. 2 ⊢ (¬ 𝑥 = 𝑦 → ∃𝑥 𝑥 = 𝑦)
10	1, 9	pm2.61i 177	1 ⊢ ∃𝑥 𝑥 = 𝑦

Syntax hints:  ¬ wn 3   → wi 4  ∀wal 1656  ∃wex 1880

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1896  ax-4 1910  ax-5 2011  ax-6 2077  ax-7 2114  ax-12 2222  ax-13 2391

This theorem depends on definitions:  df-bi 199  df-an 387  df-ex 1881

This theorem is referenced by:  ax6  2405  spimt  2407  spimtOLD  2408  spim  2409  spimed  2410  spimvALT  2413  spei  2416  equs4  2438  equsal  2439  equsexALT  2441  equvini  2477  equvel  2478  2ax6elem  2584  axi9  2800  dtrucor2  5073  axextnd  9729  ax8dfeq  32243  bj-axc10  33242  bj-alequex  33243  ax6er  33345  exlimiieq1  33346  wl-exeq  33866  wl-equsald  33870  wl-dv-sb  33875  ax6e2nd  39603  ax6e2ndVD  39963  ax6e2ndALT  39985  spd  43321