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

Theorem reu5 2913
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 2318 . 2  |-  ( E! x ( x  e.  A  /\  ph )  <->  ( E. x ( x  e.  A  /\  ph )  /\  E* x ( x  e.  A  /\  ph ) ) )
2 df-reu 2704 . 2  |-  ( E! x  e.  A  ph  <->  E! x ( x  e.  A  /\  ph )
)
3 df-rex 2703 . . 3  |-  ( E. x  e.  A  ph  <->  E. x ( x  e.  A  /\  ph )
)
4 df-rmo 2705 . . 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 1550    e. wcel 1725   E!weu 2280   E*wmo 2281   E.wrex 2698   E!wreu 2699   E*wrmo 2700
This theorem is referenced by:  reurex  2914  reurmo  2915  reu4  3120  reueq  3123  wereu  4570  wereu2  4571  reusv1  4715  fncnv  5507  moriotass  6571  supeu  7451  resqreu  12050  sqrneg  12065  sqreu  12156  catideu  13892  poslubd  14566  spweu  14651  mndideu  14690  ismgmid  14702  evlseu  19929  ply1divalg  20052  pjhtheu  22888  pjpreeq  22892  cnlnadjeui  23572  cvmliftlem14  24976  cvmlift2lem13  24994  cvmlift3  25007  linethrueu  26082  frlmup4  27221  2reu5a  27922  reuan  27925  2reurex  27926  2rexreu  27930  2reu1  27931  frgra2v  28326
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  df-rex 2703  df-reu 2704  df-rmo 2705
  Copyright terms: Public domain W3C validator