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

Theorem eu5 2318
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 1629 . . 3  |-  F/ y
ph
21eu3 2306 . 2  |-  ( E! x ph  <->  ( E. x ph  /\  E. y A. x ( ph  ->  x  =  y ) ) )
31mo2 2309 . . 3  |-  ( E* x ph  <->  E. y A. x ( ph  ->  x  =  y ) )
43anbi2i 676 . 2  |-  ( ( E. x ph  /\  E* x ph )  <->  ( E. x ph  /\  E. y A. x ( ph  ->  x  =  y ) ) )
52, 4bitr4i 244 1  |-  ( E! x ph  <->  ( E. x ph  /\  E* x ph ) )
Colors of variables: wff set class
Syntax hints:    -> wi 4    <-> wb 177    /\ wa 359   A.wal 1549   E.wex 1550   E!weu 2280   E*wmo 2281
This theorem is referenced by:  eu4  2319  eumo  2320  exmoeu2  2323  euim  2330  euan  2337  2euex  2352  2euswap  2356  2exeu  2357  2eu1  2360  reu5  2913  reuss2  3613  n0moeu  3632  reusv2lem1  4716  funcnv3  5504  fnres  5553  fnopabg  5560  brprcneu  5713  dff3  5874  finnisoeu  7986  dfac2  8003  recmulnq  8833  uptx  17649  hausflf2  18022  adjeu  23384  mptfnf  24065  bnj151  29185  bnj600  29227
This theorem was proved from axioms:  ax-1 5  ax-2 6  ax-3 7  ax-mp 8  ax-gen 1555  ax-5 1566  ax-17 1626  ax-9 1666  ax-8 1687  ax-6 1744  ax-7 1749  ax-11 1761  ax-12 1950
This theorem depends on definitions:  df-bi 178  df-or 360  df-an 361  df-tru 1328  df-ex 1551  df-nf 1554  df-sb 1659  df-eu 2284  df-mo 2285
  Copyright terms: Public domain W3C validator