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 1809 through ax-9 2119, all axioms other than ax-6 1967 are believed to be theorems of free logic, although the system without ax-6 1967 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 1969 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 2182	. 2 ⊢ (𝑥 = 𝑦 → ∃𝑥 𝑥 = 𝑦)
2		ax13lem1 2373	. . . 4 ⊢ (¬ 𝑥 = 𝑦 → (𝑤 = 𝑦 → ∀𝑥 𝑤 = 𝑦))
3		ax6ev 1969	. . . . . 6 ⊢ ∃𝑥 𝑥 = 𝑤
4		equtr 2021	. . . . . 6 ⊢ (𝑥 = 𝑤 → (𝑤 = 𝑦 → 𝑥 = 𝑦))
5	3, 4	eximii 1837	. . . . 5 ⊢ ∃𝑥(𝑤 = 𝑦 → 𝑥 = 𝑦)
6	5	19.35i 1878	. . . 4 ⊢ (∀𝑥 𝑤 = 𝑦 → ∃𝑥 𝑥 = 𝑦)
7	2, 6	syl6com 37	. . 3 ⊢ (𝑤 = 𝑦 → (¬ 𝑥 = 𝑦 → ∃𝑥 𝑥 = 𝑦))
8		ax6ev 1969	. . 3 ⊢ ∃𝑤 𝑤 = 𝑦
9	7, 8	exlimiiv 1931	. 2 ⊢ (¬ 𝑥 = 𝑦 → ∃𝑥 𝑥 = 𝑦)
10	1, 9	pm2.61i 182	1 ⊢ ∃𝑥 𝑥 = 𝑦

Syntax hints:  ¬ wn 3   → wi 4  ∀wal 1538  ∃wex 1779

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1795  ax-4 1809  ax-5 1910  ax-6 1967  ax-7 2008  ax-12 2178  ax-13 2371

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

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  2698  dtrucor2  5330  axextnd  10551  ax8dfeq  35793  bj-axc10  36778  bj-alequex  36779  ax6er  36828  exlimiieq1  36829  wl-exeq  37529  wl-equsald  37534  ax6e2nd  44555  ax6e2ndVD  44904  ax6e2ndALT  44926  spd  49671