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

Theorem euex 2166
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 1605 . . 3  |-  F/ y
ph
21eu1 2164 . 2  |-  ( E! x ph  <->  E. x
( ph  /\  A. y
( [ y  /  x ] ph  ->  x  =  y ) ) )
3 exsimpl 1579 . 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 1527   E.wex 1528    = wceq 1623   [wsb 1629   E!weu 2143
This theorem is referenced by:  eu2  2168  exmoeu  2185  eupickbi  2209  2eu2ex  2217  2exeu  2220  euxfr  2951  eusvnf  4529  eusvnfb  4530  reusv2lem2  4536  reusv2lem3  4537  dffv3  5521  tz6.12c  5547  ndmfv  5552  dff3  5673  zfrep6  5748  fnoprabg  5945  eusvobj2  6337  dfac5lem5  7754  grpidval  14384  0g0  14386  txcn  17320  unnf  24846  unqsym1  24864  moxfr  26752  bnj605  28939  bnj607  28948  bnj906  28962  bnj908  28963
This theorem was proved from axioms:  ax-1 5  ax-2 6  ax-3 7  ax-mp 8  ax-gen 1533  ax-5 1544  ax-17 1603  ax-9 1635  ax-8 1643  ax-6 1703  ax-7 1708  ax-11 1715  ax-12 1866
This theorem depends on definitions:  df-bi 177  df-or 359  df-an 360  df-tru 1310  df-ex 1529  df-nf 1532  df-sb 1630  df-eu 2147
  Copyright terms: Public domain W3C validator