Theorem ax6e 2094

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

It is preferred to use ax6ev 1807 when it is sufficient. (Contributed by NM, 14-May-1993.) Shortened after axc9lem1 2093 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 1935	. 2 |- ( x = y -> E. x x = y )
2		axc9lem1 2093	. . . 4 |- ( -. x = y -> ( w = y -> A. x w = y ) )
3		ax6ev 1807	. . . . . 6 |- E. x x = w
4		equtr 1865	. . . . . 6 |- ( x = w -> ( w = y -> x = y ) )
5	3, 4	eximii 1709	. . . . 5 |- E. x ( w = y -> x = y )
6	5	19.35i 1741	. . . 4 |- ( A. x w = y -> E. x x = y )
7	2, 6	syl6com 36	. . 3 |- ( w = y -> ( -. x = y -> E. x x = y ) )
8		ax6ev 1807	. . 3 |- E. w w = y
9	7, 8	exlimiiv 1777	. 2 |- ( -. x = y -> E. x x = y )
10	1, 9	pm2.61i 168	1 |- E. x x = y

Syntax hints:   -. wn 3   -> wi 4   A.wal 1442   E.wex 1663

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1669  ax-4 1682  ax-5 1758  ax-6 1805  ax-7 1851  ax-12 1933  ax-13 2091

This theorem depends on definitions:  df-bi 189  df-an 373  df-ex 1664

This theorem is referenced by:  ax6  2095  spimt  2097  spim  2098  spimed  2099  spimv  2101  spei  2105  equs4  2127  equsal  2128  equsexALT  2131  equvini  2179  equveli  2180  2ax6elem  2278  axi9  2427  dtrucor2  4634  axextnd  9016  ax8dfeq  30445  bj-alequex  31309  ax6er  31435  exlimiieq1  31436  wl-exeq  31867  wl-equsald  31872  ax6e2nd  36925  ax6e2ndVD  37305  ax6e2ndALT  37327