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

Theorem eu5 2181
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 1605 . . 3  |-  F/ y
ph
21eu3 2169 . 2  |-  ( E! x ph  <->  ( E. x ph  /\  E. y A. x ( ph  ->  x  =  y ) ) )
31mo2 2172 . . 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 1527   E.wex 1528    = wceq 1623   E!weu 2143   E*wmo 2144
This theorem is referenced by:  eu4  2182  eumo  2183  exmoeu2  2186  euim  2193  euan  2200  2euex  2215  2euswap  2219  2exeu  2220  2eu1  2223  reu5  2753  reuss2  3448  n0moeu  3467  reusv2lem1  4535  funcnv3  5311  fnres  5360  fnopabg  5367  brprcneu  5518  dff3  5673  finnisoeu  7740  dfac2  7757  recmulnq  8588  uptx  17319  hausflf2  17693  adjeu  22469  bnj151  28282  bnj600  28324
This theorem was proved from axioms:  ax-1 5  ax-2 6  ax-3 7  ax-mp 8  ax-gen 1533  ax-5 1544  ax-17 1603  ax-9 1635  ax-8 1643  ax-6 1703  ax-7 1708  ax-11 1715  ax-12 1866
This theorem depends on definitions:  df-bi 177  df-or 359  df-an 360  df-tru 1310  df-ex 1529  df-nf 1532  df-sb 1630  df-eu 2147  df-mo 2148
  Copyright terms: Public domain W3C validator