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

Theorem euex 2334
Description: Existential uniqueness implies existence. For a shorter proof using more axioms, see euexALT 2351. (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 2314 . 2  |-  ( E! x ph  <->  E. y A. x ( ph  <->  x  =  y ) )
2 ax6ev 1818 . . . . 5  |-  E. x  x  =  y
3 biimpr 203 . . . . . 6  |-  ( (
ph 
<->  x  =  y )  ->  ( x  =  y  ->  ph ) )
43com12 32 . . . . 5  |-  ( x  =  y  ->  (
( ph  <->  x  =  y
)  ->  ph ) )
52, 4eximii 1720 . . . 4  |-  E. x
( ( ph  <->  x  =  y )  ->  ph )
6519.35i 1752 . . 3  |-  ( A. x ( ph  <->  x  =  y )  ->  E. x ph )
76exlimiv 1787 . 2  |-  ( E. y A. x (
ph 
<->  x  =  y )  ->  E. x ph )
81, 7sylbi 200 1  |-  ( E! x ph  ->  E. x ph )
Colors of variables: wff setvar class
Syntax hints:    -> wi 4    <-> wb 189   A.wal 1453   E.wex 1674   E!weu 2310
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1680  ax-4 1693  ax-5 1769  ax-6 1816
This theorem depends on definitions:  df-bi 190  df-ex 1675  df-eu 2314
This theorem is referenced by:  eu5  2336  exmoeu  2342  euan  2370  eupickbi  2379  2eu2ex  2386  2exeu  2389  euxfr  3236  eusvnf  4612  eusvnfb  4613  reusv2lem2  4619  reusv2lem3  4620  csbiota  5594  dffv3  5884  tz6.12c  5907  ndmfv  5912  dff3  6058  csbriota  6289  eusvobj2  6308  fnoprabg  6424  zfrep6  6788  dfac5lem5  8584  initoeu1  15955  initoeu1w  15956  initoeu2  15960  termoeu1  15962  termoeu1w  15963  grpidval  16552  0g0  16555  txcn  20690  bnj605  29767  bnj607  29776  bnj906  29790  bnj908  29791  unnf  31116  unqsym1  31134  moxfr  35579  eu2ndop1stv  38661  afveu  38693  zrninitoringc  40346
  Copyright terms: Public domain W3C validator