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. For a shorter proof using more axioms, see euexALT 2328. (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 2279 . 2  |-  ( E! x ph  <->  E. y A. x ( ph  <->  x  =  y ) )
2 ax6ev 1721 . . . . 5  |-  E. x  x  =  y
3 bi2 198 . . . . . 6  |-  ( (
ph 
<->  x  =  y )  ->  ( x  =  y  ->  ph ) )
43com12 31 . . . . 5  |-  ( x  =  y  ->  (
( ph  <->  x  =  y
)  ->  ph ) )
52, 4eximii 1637 . . . 4  |-  E. x
( ( ph  <->  x  =  y )  ->  ph )
6519.35i 1666 . . 3  |-  ( A. x ( ph  <->  x  =  y )  ->  E. x ph )
76exlimiv 1698 . 2  |-  ( E. y A. x (
ph 
<->  x  =  y )  ->  E. x ph )
81, 7sylbi 195 1  |-  ( E! x ph  ->  E. x ph )
Colors of variables: wff setvar class
Syntax hints:    -> wi 4    <-> wb 184   A.wal 1377   E.wex 1596   E!weu 2275
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1601  ax-4 1612  ax-5 1680  ax-6 1719
This theorem depends on definitions:  df-bi 185  df-ex 1597  df-eu 2279
This theorem is referenced by:  eu5  2305  exmoeu  2311  exmoeuOLD  2312  eu2OLD  2329  euan  2353  eupickbi  2368  eupickbiOLD  2369  2eu2ex  2377  2exeu  2380  euxfr  3289  eusvnf  4642  eusvnfb  4643  reusv2lem2  4649  reusv2lem3  4650  csbiota  5580  dffv3  5862  tz6.12c  5885  ndmfv  5890  dff3  6034  csbriota  6257  eusvobj2  6277  fnoprabg  6387  zfrep6  6752  dfac5lem5  8508  grpidval  15749  0g0  15751  txcn  19890  unnf  29477  unqsym1  29495  moxfr  30256  eu2ndop1stv  31702  afveu  31733  bnj605  33062  bnj607  33071  bnj906  33085  bnj908  33086
  Copyright terms: Public domain W3C validator