Theorem ax6e 2417

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

Usage of this theorem is discouraged because it depends on ax-13 2406. It is preferred to use ax6ev 1992 when it is sufficient. (Contributed by NM, 14-May-1993.) Shortened after ax13lem1 2408 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 2219	. 2 ⊢ (𝑥 = 𝑦 → ∃𝑥 𝑥 = 𝑦)
2		ax13lem1 2408	. . . 4 ⊢ (¬ 𝑥 = 𝑦 → (𝑤 = 𝑦 → ∀𝑥 𝑤 = 𝑦))
3		ax6ev 1992	. . . . . 6 ⊢ ∃𝑥 𝑥 = 𝑤
4		equtr 2044	. . . . . 6 ⊢ (𝑥 = 𝑤 → (𝑤 = 𝑦 → 𝑥 = 𝑦))
5	3, 4	eximii 1860	. . . . 5 ⊢ ∃𝑥(𝑤 = 𝑦 → 𝑥 = 𝑦)
6	5	19.35i 1901	. . . 4 ⊢ (∀𝑥 𝑤 = 𝑦 → ∃𝑥 𝑥 = 𝑦)
7	2, 6	syl6com 38	. . 3 ⊢ (𝑤 = 𝑦 → (¬ 𝑥 = 𝑦 → ∃𝑥 𝑥 = 𝑦))
8		ax6ev 1992	. . 3 ⊢ ∃𝑤 𝑤 = 𝑦
9	7, 8	exlimiiv 1954	. 2 ⊢ (¬ 𝑥 = 𝑦 → ∃𝑥 𝑥 = 𝑦)
10	1, 9	pm2.61i 184	1 ⊢ ∃𝑥 𝑥 = 𝑦

Syntax hints:  ¬ wn 3   → wi 4  ∀wal 1561  ∃wex 1802

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1818  ax-4 1832  ax-5 1933  ax-6 1990  ax-7 2031  ax-12 2215  ax-13 2406

This theorem depends on definitions:  df-bi 210  df-an 401  df-ex 1803

This theorem is referenced by:  ax6  2418  spimt  2420  spim  2421  spimed  2422  spimvALT  2425  spei  2428  equs4  2450  equsal  2451  equsexALT  2453  equvini  2489  equvel  2490  2ax6elem  2504  axi9  2733  dtrucor2  5333  axextnd  10564  ax8dfeq  36154  bj-axc10  37275  bj-alequex  37276  ax6er  37325  exlimiieq1  37326  wl-exeq  38044  wl-equsald  38049  ax6e2nd  45126  ax6e2ndVD  45475  ax6e2ndALT  45497  spd  50308