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

Theorem reu5 2753
Description: Restricted uniqueness in terms of "at most one." (Contributed by NM, 23-May-1999.) (Revised by NM, 16-Jun-2017.)
Assertion
Ref Expression
reu5  |-  ( E! x  e.  A  ph  <->  ( E. x  e.  A  ph 
/\  E* x  e.  A ph ) )

Proof of Theorem reu5
StepHypRef Expression
1 eu5 2181 . 2  |-  ( E! x ( x  e.  A  /\  ph )  <->  ( E. x ( x  e.  A  /\  ph )  /\  E* x ( x  e.  A  /\  ph ) ) )
2 df-reu 2550 . 2  |-  ( E! x  e.  A  ph  <->  E! x ( x  e.  A  /\  ph )
)
3 df-rex 2549 . . 3  |-  ( E. x  e.  A  ph  <->  E. x ( x  e.  A  /\  ph )
)
4 df-rmo 2551 . . 3  |-  ( E* x  e.  A ph  <->  E* x ( x  e.  A  /\  ph )
)
53, 4anbi12i 678 . 2  |-  ( ( E. x  e.  A  ph 
/\  E* x  e.  A ph )  <->  ( E. x
( x  e.  A  /\  ph )  /\  E* x ( x  e.  A  /\  ph )
) )
61, 2, 53bitr4i 268 1  |-  ( E! x  e.  A  ph  <->  ( E. x  e.  A  ph 
/\  E* x  e.  A ph ) )
Colors of variables: wff set class
Syntax hints:    <-> wb 176    /\ wa 358   E.wex 1528    e. wcel 1684   E!weu 2143   E*wmo 2144   E.wrex 2544   E!wreu 2545   E*wrmo 2546
This theorem is referenced by:  reurex  2754  reurmo  2755  reu4  2959  reueq  2962  wereu  4389  wereu2  4390  reusv1  4534  fncnv  5314  moriotass  6334  supeu  7205  enqeq  8558  resqreu  11738  sqrneg  11753  sqreu  11844  eqsqrd  11851  catideu  13577  poslubd  14251  spweu  14336  mndideu  14375  ismgmid  14387  efgred2  15062  frgpnabllem2  15162  frgpcyg  16527  qtophmeo  17508  evlseu  19400  ply1divalg  19523  pjhtheu  21973  pjpreeq  21977  cnlnadjeui  22657  cvmliftlem14  23828  cvmlift2lem13  23846  cvmlift3  23859  linethrueu  24779  frlmup4  27253  2reu5a  27955  reuan  27958  2reurex  27959  2rexreu  27963  2reu1  27964  frgra2v  28177
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  df-rex 2549  df-reu 2550  df-rmo 2551
  Copyright terms: Public domain W3C validator