Theorem ax6e 2388

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

Usage of this theorem is discouraged because it depends on ax-13 2377. It is preferred to use ax6ev 1971 when it is sufficient. (Contributed by NM, 14-May-1993.) Shortened after ax13lem1 2379 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 2189	. 2 ⊢ (𝑥 = 𝑦 → ∃𝑥 𝑥 = 𝑦)
2		ax13lem1 2379	. . . 4 ⊢ (¬ 𝑥 = 𝑦 → (𝑤 = 𝑦 → ∀𝑥 𝑤 = 𝑦))
3		ax6ev 1971	. . . . . 6 ⊢ ∃𝑥 𝑥 = 𝑤
4		equtr 2023	. . . . . 6 ⊢ (𝑥 = 𝑤 → (𝑤 = 𝑦 → 𝑥 = 𝑦))
5	3, 4	eximii 1839	. . . . 5 ⊢ ∃𝑥(𝑤 = 𝑦 → 𝑥 = 𝑦)
6	5	19.35i 1880	. . . 4 ⊢ (∀𝑥 𝑤 = 𝑦 → ∃𝑥 𝑥 = 𝑦)
7	2, 6	syl6com 37	. . 3 ⊢ (𝑤 = 𝑦 → (¬ 𝑥 = 𝑦 → ∃𝑥 𝑥 = 𝑦))
8		ax6ev 1971	. . 3 ⊢ ∃𝑤 𝑤 = 𝑦
9	7, 8	exlimiiv 1933	. 2 ⊢ (¬ 𝑥 = 𝑦 → ∃𝑥 𝑥 = 𝑦)
10	1, 9	pm2.61i 182	1 ⊢ ∃𝑥 𝑥 = 𝑦

Syntax hints:  ¬ wn 3   → wi 4  ∀wal 1540  ∃wex 1781

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1797  ax-4 1811  ax-5 1912  ax-6 1969  ax-7 2010  ax-12 2185  ax-13 2377

This theorem depends on definitions:  df-bi 207  df-an 396  df-ex 1782

This theorem is referenced by:  ax6  2389  spimt  2391  spim  2392  spimed  2393  spimvALT  2396  spei  2399  equs4  2421  equsal  2422  equsexALT  2424  equvini  2460  equvel  2461  2ax6elem  2475  axi9  2705  dtrucor2  5319  axextnd  10514  ax8dfeq  36009  bj-axc10  37025  bj-alequex  37026  ax6er  37075  exlimiieq1  37076  wl-exeq  37783  wl-equsald  37788  ax6e2nd  44908  ax6e2ndVD  45257  ax6e2ndALT  45279  spd  50031