Theorem ax6e 2382

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

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

Syntax hints:  ¬ wn 3   → wi 4  ∀wal 1539  ∃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 1913  ax-6 1971  ax-7 2011  ax-12 2171  ax-13 2371

This theorem depends on definitions:  df-bi 206  df-an 397  df-ex 1782

This theorem is referenced by:  ax6  2383  spimt  2385  spim  2386  spimed  2387  spimvALT  2390  spei  2393  equs4  2415  equsal  2416  equsexALT  2418  equvini  2454  equvel  2455  2ax6elem  2469  axi9  2699  dtrucor2  5369  axextnd  10582  ax8dfeq  34758  bj-axc10  35649  bj-alequex  35650  ax6er  35699  exlimiieq1  35700  wl-exeq  36391  wl-equsald  36396  ax6e2nd  43304  ax6e2ndVD  43654  ax6e2ndALT  43676  spd  47676