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

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.
StepHypRef 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 )
)
53, 4eximii 1709 . . . . 5  |-  E. x
( w  =  y  ->  x  =  y )
6519.35i 1741 . . . 4  |-  ( A. x  w  =  y  ->  E. x  x  =  y )
72, 6syl6com 36 . . 3  |-  ( w  =  y  ->  ( -.  x  =  y  ->  E. x  x  =  y ) )
8 ax6ev 1807 . . 3  |-  E. w  w  =  y
97, 8exlimiiv 1777 . 2  |-  ( -.  x  =  y  ->  E. x  x  =  y )
101, 9pm2.61i 168 1  |-  E. x  x  =  y
Colors of variables: wff setvar class
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
  Copyright terms: Public domain W3C validator