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

Theorem euex 2300
Description: Existential uniqueness implies existence. For a shorter proof using more axioms, see euexALT 2317. (Contributed by NM, 15-Sep-1993.) (Proof shortened by Andrew Salmon, 9-Jul-2011.) (Proof shortened by Wolf Lammen, 4-Dec-2018.)
Assertion
Ref Expression
euex  |-  ( E! x ph  ->  E. x ph )

Proof of Theorem euex
Dummy variable  y is distinct from all other variables.
StepHypRef Expression
1 df-eu 2280 . 2  |-  ( E! x ph  <->  E. y A. x ( ph  <->  x  =  y ) )
2 ax6ev 1800 . . . . 5  |-  E. x  x  =  y
3 biimpr 201 . . . . . 6  |-  ( (
ph 
<->  x  =  y )  ->  ( x  =  y  ->  ph ) )
43com12 32 . . . . 5  |-  ( x  =  y  ->  (
( ph  <->  x  =  y
)  ->  ph ) )
52, 4eximii 1703 . . . 4  |-  E. x
( ( ph  <->  x  =  y )  ->  ph )
6519.35i 1735 . . 3  |-  ( A. x ( ph  <->  x  =  y )  ->  E. x ph )
76exlimiv 1770 . 2  |-  ( E. y A. x (
ph 
<->  x  =  y )  ->  E. x ph )
81, 7sylbi 198 1  |-  ( E! x ph  ->  E. x ph )
Colors of variables: wff setvar class
Syntax hints:    -> wi 4    <-> wb 187   A.wal 1435   E.wex 1657   E!weu 2276
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1663  ax-4 1676  ax-5 1752  ax-6 1798
This theorem depends on definitions:  df-bi 188  df-ex 1658  df-eu 2280
This theorem is referenced by:  eu5  2302  exmoeu  2308  euan  2336  eupickbi  2345  2eu2ex  2352  2exeu  2355  euxfr  3199  eusvnf  4562  eusvnfb  4563  reusv2lem2  4569  reusv2lem3  4570  csbiota  5537  dffv3  5821  tz6.12c  5844  ndmfv  5849  dff3  5994  csbriota  6223  eusvobj2  6242  fnoprabg  6355  zfrep6  6719  dfac5lem5  8509  initoeu1  15849  initoeu1w  15850  initoeu2  15854  termoeu1  15856  termoeu1w  15857  grpidval  16446  0g0  16449  txcn  20583  bnj605  29670  bnj607  29679  bnj906  29693  bnj908  29694  unnf  31016  unqsym1  31034  moxfr  35446  eu2ndop1stv  38437  afveu  38468  zrninitoringc  39664
  Copyright terms: Public domain W3C validator