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

Theorem eu5 2247
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 1619 . . 3  |-  F/ y
ph
21eu3 2235 . 2  |-  ( E! x ph  <->  ( E. x ph  /\  E. y A. x ( ph  ->  x  =  y ) ) )
31mo2 2238 . . 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 1540   E.wex 1541    = wceq 1642   E!weu 2209   E*wmo 2210
This theorem is referenced by:  eu4  2248  eumo  2249  exmoeu2  2252  euim  2259  euan  2266  2euex  2281  2euswap  2285  2exeu  2286  2eu1  2289  reu5  2829  reuss2  3524  n0moeu  3543  reusv2lem1  4614  funcnv3  5390  fnres  5439  fnopabg  5446  brprcneu  5598  dff3  5753  finnisoeu  7827  dfac2  7844  recmulnq  8675  uptx  17419  hausflf2  17789  adjeu  22577  mptfnf  23274  bnj151  28654  bnj600  28696
This theorem was proved from axioms:  ax-1 5  ax-2 6  ax-3 7  ax-mp 8  ax-gen 1546  ax-5 1557  ax-17 1616  ax-9 1654  ax-8 1675  ax-6 1729  ax-7 1734  ax-11 1746  ax-12 1930
This theorem depends on definitions:  df-bi 177  df-or 359  df-an 360  df-tru 1319  df-ex 1542  df-nf 1545  df-sb 1649  df-eu 2213  df-mo 2214
  Copyright terms: Public domain W3C validator