Theorem ax6e 2250

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

It is preferred to use ax6ev 1890 when it is sufficient. (Contributed by NM, 14-May-1993.) Shortened after ax13lem1 2248 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 2052	. 2 ⊢ (𝑥 = 𝑦 → ∃𝑥 𝑥 = 𝑦)
2		ax13lem1 2248	. . . 4 ⊢ (¬ 𝑥 = 𝑦 → (𝑤 = 𝑦 → ∀𝑥 𝑤 = 𝑦))
3		ax6ev 1890	. . . . . 6 ⊢ ∃𝑥 𝑥 = 𝑤
4		equtr 1948	. . . . . 6 ⊢ (𝑥 = 𝑤 → (𝑤 = 𝑦 → 𝑥 = 𝑦))
5	3, 4	eximii 1764	. . . . 5 ⊢ ∃𝑥(𝑤 = 𝑦 → 𝑥 = 𝑦)
6	5	19.35i 1806	. . . 4 ⊢ (∀𝑥 𝑤 = 𝑦 → ∃𝑥 𝑥 = 𝑦)
7	2, 6	syl6com 37	. . 3 ⊢ (𝑤 = 𝑦 → (¬ 𝑥 = 𝑦 → ∃𝑥 𝑥 = 𝑦))
8		ax6ev 1890	. . 3 ⊢ ∃𝑤 𝑤 = 𝑦
9	7, 8	exlimiiv 1859	. 2 ⊢ (¬ 𝑥 = 𝑦 → ∃𝑥 𝑥 = 𝑦)
10	1, 9	pm2.61i 176	1 ⊢ ∃𝑥 𝑥 = 𝑦

Syntax hints:  ¬ wn 3   → wi 4  ∀wal 1481  ∃wex 1704

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1722  ax-4 1737  ax-5 1839  ax-6 1888  ax-7 1935  ax-12 2047  ax-13 2246

This theorem depends on definitions:  df-bi 197  df-an 386  df-ex 1705

This theorem is referenced by:  ax6  2251  spimt  2253  spim  2254  spimed  2255  spimv  2257  spei  2261  equs4  2290  equsal  2291  equsexALT  2293  equvini  2346  equvel  2347  2ax6elem  2449  axi9  2598  dtrucor2  4901  axextnd  9413  ax8dfeq  31704  bj-axc10  32707  bj-alequex  32708  ax6er  32820  exlimiieq1  32821  wl-exeq  33321  wl-equsald  33325  ax6e2nd  38774  ax6e2ndVD  39144  ax6e2ndALT  39166  spd  42425