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

Theorem euex 2303
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 1629 . . 3  |-  F/ y
ph
21eu1 2301 . 2  |-  ( E! x ph  <->  E. x
( ph  /\  A. y
( [ y  /  x ] ph  ->  x  =  y ) ) )
3 exsimpl 1602 . 2  |-  ( E. x ( ph  /\  A. y ( [ y  /  x ] ph  ->  x  =  y ) )  ->  E. x ph )
42, 3sylbi 188 1  |-  ( E! x ph  ->  E. x ph )
Colors of variables: wff set class
Syntax hints:    -> wi 4    /\ wa 359   A.wal 1549   E.wex 1550   [wsb 1658   E!weu 2280
This theorem is referenced by:  eu2  2305  exmoeu  2322  eupickbi  2346  2eu2ex  2354  2exeu  2357  euxfr  3112  eusvnf  4710  eusvnfb  4711  reusv2lem2  4717  reusv2lem3  4718  dffv3  5716  tz6.12c  5742  ndmfv  5747  dff3  5874  zfrep6  5960  fnoprabg  6163  eusvobj2  6574  dfac5lem5  8000  grpidval  14699  0g0  14701  txcn  17650  unnf  26149  unqsym1  26167  moxfr  26714  eu2ndop1stv  27937  afveu  27974  bnj605  29205  bnj607  29214  bnj906  29228  bnj908  29229
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-6 1744  ax-7 1749  ax-11 1761  ax-12 1950
This theorem depends on definitions:  df-bi 178  df-or 360  df-an 361  df-tru 1328  df-ex 1551  df-nf 1554  df-sb 1659  df-eu 2284
  Copyright terms: Public domain W3C validator