Theorem ax6e 2414

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

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

This proof depends on syntax axioms:  ¬ wn 3   → wi 4  ∀wal 1568  ∃wex 1812

This proof depends on axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1828  ax-4 1842  ax-5 1943  ax-6 2000  ax-7 2041  ax-12 2215  ax-13 2403

This proof depends on definitions:  df-bi 210  df-an 402  df-ex 1813

This theorem is used by:  ax6  2415  spimt  2417  spim  2418  spimed  2419  spimvALT  2422  spei  2425  equs4  2447  equsal  2448  equsexALT  2450  equvini  2486  equvel  2487  2ax6elem  2501  axi9  2730  dtrucor2  5341  axextnd  10604  ax8dfeq  36383  bj-axc10  37534  bj-alequex  37535  ax6er  37584  exlimiieq1  37585  wl-exeq  38305  wl-equsald  38310  ax6e2nd  45389  ax6e2ndVD  45738  ax6e2ndALT  45760  spd  50612