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

Theorem reu5 2864
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 2276 . 2  |-  ( E! x ( x  e.  A  /\  ph )  <->  ( E. x ( x  e.  A  /\  ph )  /\  E* x ( x  e.  A  /\  ph ) ) )
2 df-reu 2656 . 2  |-  ( E! x  e.  A  ph  <->  E! x ( x  e.  A  /\  ph )
)
3 df-rex 2655 . . 3  |-  ( E. x  e.  A  ph  <->  E. x ( x  e.  A  /\  ph )
)
4 df-rmo 2657 . . 3  |-  ( E* x  e.  A ph  <->  E* x ( x  e.  A  /\  ph )
)
53, 4anbi12i 679 . 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 269 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 177    /\ wa 359   E.wex 1547    e. wcel 1717   E!weu 2238   E*wmo 2239   E.wrex 2650   E!wreu 2651   E*wrmo 2652
This theorem is referenced by:  reurex  2865  reurmo  2866  reu4  3071  reueq  3074  wereu  4519  wereu2  4520  reusv1  4663  fncnv  5455  moriotass  6515  supeu  7392  resqreu  11985  sqrneg  12000  sqreu  12091  catideu  13827  poslubd  14501  spweu  14586  mndideu  14625  ismgmid  14637  evlseu  19804  ply1divalg  19927  pjhtheu  22744  pjpreeq  22748  cnlnadjeui  23428  cvmliftlem14  24763  cvmlift2lem13  24781  cvmlift3  24794  linethrueu  25804  frlmup4  26922  2reu5a  27623  reuan  27626  2reurex  27627  2rexreu  27631  2reu1  27632  frgra2v  27752
This theorem was proved from axioms:  ax-1 5  ax-2 6  ax-3 7  ax-mp 8  ax-gen 1552  ax-5 1563  ax-17 1623  ax-9 1661  ax-8 1682  ax-6 1736  ax-7 1741  ax-11 1753  ax-12 1939
This theorem depends on definitions:  df-bi 178  df-or 360  df-an 361  df-tru 1325  df-ex 1548  df-nf 1551  df-sb 1656  df-eu 2242  df-mo 2243  df-rex 2655  df-reu 2656  df-rmo 2657
  Copyright terms: Public domain W3C validator