MPE Home Metamath Proof Explorer < Previous   Next >
Nearby theorems
Mirrors  >  Home  >  MPE Home  >  Th. List  >  ax6e Structured version   Unicode version

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.
StepHypRef 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 )
)
64, 5eximii 1705 . . . . . 6  |-  E. x
( w  =  y  ->  x  =  y )
7619.35i 1736 . . . . 5  |-  ( A. x  w  =  y  ->  E. x  x  =  y )
83, 7syl6com 36 . . . 4  |-  ( w  =  y  ->  ( -.  x  =  y  ->  E. x  x  =  y ) )
98exlimiv 1769 . . 3  |-  ( E. w  w  =  y  ->  ( -.  x  =  y  ->  E. x  x  =  y )
)
102, 9ax-mp 5 . 2  |-  ( -.  x  =  y  ->  E. x  x  =  y )
111, 10pm2.61i 167 1  |-  E. x  x  =  y
Colors of variables: wff setvar class
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
  Copyright terms: Public domain W3C validator