Theorem ax6e 2058

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

It is preferred to use ax6ev 1799 when it is sufficient. (Contributed by NM, 14-May-1993.) Shortened after axc9lem1 2057 became available. (Revised by Wolf Lammen, 8-Sep-2018.)

Assertion

Ref	Expression
ax6e	|- E. x x = y

Proof of Theorem ax6e

Dummy variable w is distinct from all other variables.

Step	Hyp	Ref	Expression
1		19.8a 1910	. 2 |- ( x = y -> E. x x = y )
2		ax6ev 1799	. . 3 |- E. w w = y
3		axc9lem1 2057	. . . . 5 |- ( -. x = y -> ( w = y -> A. x w = y ) )
4		ax6ev 1799	. . . . . . 7 |- E. x x = w
5		equtr 1848	. . . . . . 7 |- ( x = w -> ( w = y -> x = y ) )
6	4, 5	eximii 1705	. . . . . 6 |- E. x ( w = y -> x = y )
7	6	19.35i 1736	. . . . 5 |- ( A. x w = y -> E. x x = y )
8	3, 7	syl6com 36	. . . 4 |- ( w = y -> ( -. x = y -> E. x x = y ) )
9	8	exlimiv 1769	. . 3 |- ( E. w w = y -> ( -. x = y -> E. x x = y ) )
10	2, 9	ax-mp 5	. 2 |- ( -. x = y -> E. x x = y )
11	1, 10	pm2.61i 167	1 |- E. x x = y

Syntax hints:   -. wn 3   -> wi 4   A.wal 1435   E.wex 1659

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1665  ax-4 1678  ax-5 1751  ax-6 1797  ax-7 1841  ax-12 1907  ax-13 2055

This theorem depends on definitions:  df-bi 188  df-an 372  df-ex 1660

This theorem is referenced by:  ax6  2059  spimt  2061  spim  2062  spimed  2063  spei  2068  equs4  2090  equsal  2091  equsexALT  2094  equvini  2143  equveli  2144  2ax6elem  2245  axi9  2403  dtrucor2  4656  axextnd  9014  ax8dfeq  30240  bj-alequex  31056  ax6er  31194  exlimiieq1  31195  wl-exeq  31582  wl-equsald  31587  ax6e2nd  36577  ax6e2ndVD  36960  ax6e2ndALT  36982