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

Theorem euex 2179
Description: Existential uniqueness implies existence. (Contributed by NM, 15-Sep-1993.) (Proof shortened by Andrew Salmon, 9-Jul-2011.)
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 nfv 1609 . . 3  |-  F/ y
ph
21eu1 2177 . 2  |-  ( E! x ph  <->  E. x
( ph  /\  A. y
( [ y  /  x ] ph  ->  x  =  y ) ) )
3 exsimpl 1582 . 2  |-  ( E. x ( ph  /\  A. y ( [ y  /  x ] ph  ->  x  =  y ) )  ->  E. x ph )
42, 3sylbi 187 1  |-  ( E! x ph  ->  E. x ph )
Colors of variables: wff set class
Syntax hints:    -> wi 4    /\ wa 358   A.wal 1530   E.wex 1531    = wceq 1632   [wsb 1638   E!weu 2156
This theorem is referenced by:  eu2  2181  exmoeu  2198  eupickbi  2222  2eu2ex  2230  2exeu  2233  euxfr  2964  eusvnf  4545  eusvnfb  4546  reusv2lem2  4552  reusv2lem3  4553  dffv3  5537  tz6.12c  5563  ndmfv  5568  dff3  5689  zfrep6  5764  fnoprabg  5961  eusvobj2  6353  dfac5lem5  7770  grpidval  14400  0g0  14402  txcn  17336  unnf  24918  unqsym1  24936  moxfr  26855  eu2ndop1stv  28083  afveu  28121  bnj605  29255  bnj607  29264  bnj906  29278  bnj908  29279
This theorem was proved from axioms:  ax-1 5  ax-2 6  ax-3 7  ax-mp 8  ax-gen 1536  ax-5 1547  ax-17 1606  ax-9 1644  ax-8 1661  ax-6 1715  ax-7 1720  ax-11 1727  ax-12 1878
This theorem depends on definitions:  df-bi 177  df-or 359  df-an 360  df-tru 1310  df-ex 1532  df-nf 1535  df-sb 1639  df-eu 2160
  Copyright terms: Public domain W3C validator