Theorem ax6e 2412

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

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

Syntax hints:  ¬ wn 3   → wi 4  ∀wal 1629  ∃wex 1852

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1870  ax-4 1885  ax-5 1991  ax-6 2057  ax-7 2093  ax-12 2203  ax-13 2408

This theorem depends on definitions:  df-bi 197  df-an 383  df-ex 1853

This theorem is referenced by:  ax6  2413  spimt  2415  spim  2416  spimed  2417  spimvALT  2420  spei  2423  equs4  2445  equsal  2446  equsexALT  2448  equvini  2492  equvel  2493  2ax6elem  2597  axi9  2747  dtrucor2  5029  axextnd  9613  ax8dfeq  32033  bj-axc10  33037  bj-alequex  33038  ax6er  33148  exlimiieq1  33149  wl-exeq  33649  wl-equsald  33653  ax6e2nd  39292  ax6e2ndVD  39659  ax6e2ndALT  39681  spd  42946