Theorem ax6e 1971

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

It is preferred to use ax6ev 1721 when it is sufficient. (Contributed by NM, 14-May-1993.) Shortened after axc9lem1 1970 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 1806	. 2 |- ( x = y -> E. x x = y )
2		ax6ev 1721	. . 3 |- E. w w = y
3		axc9lem1 1970	. . . . 5 |- ( -. x = y -> ( w = y -> A. x w = y ) )
4		ax6ev 1721	. . . . . . 7 |- E. x x = w
5		equtr 1745	. . . . . . 7 |- ( x = w -> ( w = y -> x = y ) )
6	4, 5	eximii 1637	. . . . . 6 |- E. x ( w = y -> x = y )
7	6	19.35i 1666	. . . . 5 |- ( A. x w = y -> E. x x = y )
8	3, 7	syl6com 35	. . . 4 |- ( w = y -> ( -. x = y -> E. x x = y ) )
9	8	exlimiv 1698	. . 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 164	1 |- E. x x = y

Syntax hints:   -. wn 3   -> wi 4   A.wal 1377   E.wex 1596

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1601  ax-4 1612  ax-5 1680  ax-6 1719  ax-7 1739  ax-12 1803  ax-13 1968

This theorem depends on definitions:  df-bi 185  df-an 371  df-ex 1597

This theorem is referenced by:  ax6  1972  spimt  1974  spim  1975  spimed  1976  spei  1981  equs4  2008  equsal  2009  equvini  2060  equveli  2061  equveliOLD  2062  2ax6elem  2179  axi9  2441  dtrucor2  4687  axextnd  8978  ax8dfeq  29158  wl-exeq  29914  wl-equsald  29919  ax6e2nd  32812  ax6e2ndVD  33189  ax6e2ndALT  33211  bj-alequex  33751  ax6er  33888  exlimiieq1  33889