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

Theorem a9e 1952
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-5 1566 through ax-14 1729 and ax-17 1626, all axioms other than ax-9 1666 are believed to be theorems of free logic, although the system without ax-9 1666 is probably not complete in free logic. (Contributed by NM, 5-Aug-1993.) (Revised by Wolf Lammen, 25-Feb-2018.)
Assertion
Ref Expression
a9e  |-  E. x  x  =  y

Proof of Theorem a9e
Dummy variable  v is distinct from all other variables.
StepHypRef Expression
1 19.8a 1762 . 2  |-  ( x  =  y  ->  E. x  x  =  y )
2 a9ev 1668 . . 3  |-  E. v 
v  =  y
3 ax12v 1951 . . . . . 6  |-  ( -.  x  =  y  -> 
( y  =  v  ->  A. x  y  =  v ) )
4 a9ev 1668 . . . . . . . 8  |-  E. x  x  =  v
5 equequ2 1698 . . . . . . . . 9  |-  ( y  =  v  ->  (
x  =  y  <->  x  =  v ) )
65biimprcd 217 . . . . . . . 8  |-  ( x  =  v  ->  (
y  =  v  ->  x  =  y )
)
74, 6eximii 1587 . . . . . . 7  |-  E. x
( y  =  v  ->  x  =  y )
8719.35i 1611 . . . . . 6  |-  ( A. x  y  =  v  ->  E. x  x  =  y )
93, 8syl6com 33 . . . . 5  |-  ( y  =  v  ->  ( -.  x  =  y  ->  E. x  x  =  y ) )
109equcoms 1693 . . . 4  |-  ( v  =  y  ->  ( -.  x  =  y  ->  E. x  x  =  y ) )
1110exlimiv 1644 . . 3  |-  ( E. v  v  =  y  ->  ( -.  x  =  y  ->  E. x  x  =  y )
)
122, 11ax-mp 8 . 2  |-  ( -.  x  =  y  ->  E. x  x  =  y )
131, 12pm2.61i 158 1  |-  E. x  x  =  y
Colors of variables: wff set class
Syntax hints:   -. wn 3    -> wi 4   A.wal 1549   E.wex 1550
This theorem is referenced by:  ax9  1953  spimt  1955  spim  1957  spimed  1960  spei  1966  equs4  1997  equs4OLD  1998  equsal  1999  equvini  2083  equviniOLD  2084  equveli  2085  ax11vALT  2173  axi9  2413  dtrucor2  4398  axextnd  8466  ax13dfeq  25426  wl-exeq  26234  a9e2nd  28645  a9e2ndVD  29020  a9e2ndALT  29042
This theorem was proved from axioms:  ax-1 5  ax-2 6  ax-3 7  ax-mp 8  ax-gen 1555  ax-5 1566  ax-17 1626  ax-9 1666  ax-8 1687  ax-11 1761  ax-12 1950
This theorem depends on definitions:  df-bi 178  df-an 361  df-ex 1551
  Copyright terms: Public domain W3C validator