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

Theorem euex 2261
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 1626 . . 3  |-  F/ y
ph
21eu1 2259 . 2  |-  ( E! x ph  <->  E. x
( ph  /\  A. y
( [ y  /  x ] ph  ->  x  =  y ) ) )
3 exsimpl 1599 . 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 1546   E.wex 1547   [wsb 1655   E!weu 2238
This theorem is referenced by:  eu2  2263  exmoeu  2280  eupickbi  2304  2eu2ex  2312  2exeu  2315  euxfr  3063  eusvnf  4658  eusvnfb  4659  reusv2lem2  4665  reusv2lem3  4666  dffv3  5664  tz6.12c  5690  ndmfv  5695  dff3  5821  zfrep6  5907  fnoprabg  6110  eusvobj2  6518  dfac5lem5  7941  grpidval  14634  0g0  14636  txcn  17579  unnf  25871  unqsym1  25889  moxfr  26424  eu2ndop1stv  27648  afveu  27686  bnj605  28616  bnj607  28625  bnj906  28639  bnj908  28640
This theorem was proved from axioms:  ax-1 5  ax-2 6  ax-3 7  ax-mp 8  ax-gen 1552  ax-5 1563  ax-17 1623  ax-9 1661  ax-8 1682  ax-6 1736  ax-7 1741  ax-11 1753  ax-12 1939
This theorem depends on definitions:  df-bi 178  df-or 360  df-an 361  df-tru 1325  df-ex 1548  df-nf 1551  df-sb 1656  df-eu 2242
  Copyright terms: Public domain W3C validator