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

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.
StepHypRef 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 )
)
64, 5eximii 1637 . . . . . 6  |-  E. x
( w  =  y  ->  x  =  y )
7619.35i 1666 . . . . 5  |-  ( A. x  w  =  y  ->  E. x  x  =  y )
83, 7syl6com 35 . . . 4  |-  ( w  =  y  ->  ( -.  x  =  y  ->  E. x  x  =  y ) )
98exlimiv 1698 . . 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 164 1  |-  E. x  x  =  y
Colors of variables: wff setvar class
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
  Copyright terms: Public domain W3C validator