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

Theorem eu5 2194
Description: Uniqueness in terms of "at most one." (Contributed by NM, 23-Mar-1995.)
Assertion
Ref Expression
eu5  |-  ( E! x ph  <->  ( E. x ph  /\  E* x ph ) )

Proof of Theorem eu5
Dummy variable  y is distinct from all other variables.
StepHypRef Expression
1 nfv 1609 . . 3  |-  F/ y
ph
21eu3 2182 . 2  |-  ( E! x ph  <->  ( E. x ph  /\  E. y A. x ( ph  ->  x  =  y ) ) )
31mo2 2185 . . 3  |-  ( E* x ph  <->  E. y A. x ( ph  ->  x  =  y ) )
43anbi2i 675 . 2  |-  ( ( E. x ph  /\  E* x ph )  <->  ( E. x ph  /\  E. y A. x ( ph  ->  x  =  y ) ) )
52, 4bitr4i 243 1  |-  ( E! x ph  <->  ( E. x ph  /\  E* x ph ) )
Colors of variables: wff set class
Syntax hints:    -> wi 4    <-> wb 176    /\ wa 358   A.wal 1530   E.wex 1531    = wceq 1632   E!weu 2156   E*wmo 2157
This theorem is referenced by:  eu4  2195  eumo  2196  exmoeu2  2199  euim  2206  euan  2213  2euex  2228  2euswap  2232  2exeu  2233  2eu1  2236  reu5  2766  reuss2  3461  n0moeu  3480  reusv2lem1  4551  funcnv3  5327  fnres  5376  fnopabg  5383  brprcneu  5534  dff3  5689  finnisoeu  7756  dfac2  7773  recmulnq  8604  uptx  17335  hausflf2  17709  adjeu  22485  mptfnf  23241  bnj151  29225  bnj600  29267
This theorem was proved from axioms:  ax-1 5  ax-2 6  ax-3 7  ax-mp 8  ax-gen 1536  ax-5 1547  ax-17 1606  ax-9 1644  ax-8 1661  ax-6 1715  ax-7 1720  ax-11 1727  ax-12 1878
This theorem depends on definitions:  df-bi 177  df-or 359  df-an 360  df-tru 1310  df-ex 1532  df-nf 1535  df-sb 1639  df-eu 2160  df-mo 2161
  Copyright terms: Public domain W3C validator