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

Theorem euex 2281
Description: Existential uniqueness implies existence. For a shorter proof using more axioms, see euexALT 2306. (Contributed by NM, 15-Sep-1993.) (Proof shortened by Andrew Salmon, 9-Jul-2011.) (Revised 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 2257 . 2  |-  ( E! x ph  <->  E. y A. x ( ph  <->  x  =  y ) )
2 ax6ev 1710 . . . . 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 1627 . . . 4  |-  E. x
( ( ph  <->  x  =  y )  ->  ph )
6519.35i 1656 . . 3  |-  ( A. x ( ph  <->  x  =  y )  ->  E. x ph )
76exlimiv 1688 . 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 1367   E.wex 1586   E!weu 2253
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1591  ax-4 1602  ax-5 1670  ax-6 1708
This theorem depends on definitions:  df-bi 185  df-ex 1587  df-eu 2257
This theorem is referenced by:  eu5  2283  exmoeu  2289  exmoeuOLD  2290  eu2OLD  2307  euan  2331  eupickbi  2346  eupickbiOLD  2347  2eu2ex  2355  2exeu  2358  euxfr  3144  eusvnf  4486  eusvnfb  4487  reusv2lem2  4493  reusv2lem3  4494  csbiota  5409  dffv3  5686  tz6.12c  5708  ndmfv  5713  dff3  5855  csbriota  6063  eusvobj2  6083  fnoprabg  6190  zfrep6  6544  dfac5lem5  8296  grpidval  15431  0g0  15433  txcn  19198  unnf  28252  unqsym1  28270  moxfr  29026  eu2ndop1stv  30024  afveu  30057  bnj605  31898  bnj607  31907  bnj906  31921  bnj908  31922
  Copyright terms: Public domain W3C validator