Theorem ax6e 2413

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

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

Syntax hints:  ¬ wn 3   → wi 4  ∀wal 1557  ∃wex 1798

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1814  ax-4 1828  ax-5 1929  ax-6 1986  ax-7 2027  ax-12 2211  ax-13 2402

This theorem depends on definitions:  df-bi 209  df-an 400  df-ex 1799

This theorem is referenced by:  ax6  2414  spimt  2416  spim  2417  spimed  2418  spimvALT  2421  spei  2424  equs4  2446  equsal  2447  equsexALT  2449  equvini  2485  equvel  2486  2ax6elem  2500  axi9  2729  dtrucor2  5328  axextnd  10546  ax8dfeq  36110  bj-axc10  37232  bj-alequex  37233  ax6er  37282  exlimiieq1  37283  wl-exeq  38001  wl-equsald  38006  ax6e2nd  45098  ax6e2ndVD  45447  ax6e2ndALT  45469  spd  50263