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

Theorem reu5 2766
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 2194 . 2  |-  ( E! x ( x  e.  A  /\  ph )  <->  ( E. x ( x  e.  A  /\  ph )  /\  E* x ( x  e.  A  /\  ph ) ) )
2 df-reu 2563 . 2  |-  ( E! x  e.  A  ph  <->  E! x ( x  e.  A  /\  ph )
)
3 df-rex 2562 . . 3  |-  ( E. x  e.  A  ph  <->  E. x ( x  e.  A  /\  ph )
)
4 df-rmo 2564 . . 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 1531    e. wcel 1696   E!weu 2156   E*wmo 2157   E.wrex 2557   E!wreu 2558   E*wrmo 2559
This theorem is referenced by:  reurex  2767  reurmo  2768  reu4  2972  reueq  2975  wereu  4405  wereu2  4406  reusv1  4550  fncnv  5330  moriotass  6350  supeu  7221  enqeq  8574  resqreu  11754  sqrneg  11769  sqreu  11860  eqsqrd  11867  catideu  13593  poslubd  14267  spweu  14352  mndideu  14391  ismgmid  14403  efgred2  15078  frgpnabllem2  15178  frgpcyg  16543  qtophmeo  17524  evlseu  19416  ply1divalg  19539  pjhtheu  21989  pjpreeq  21993  cnlnadjeui  22673  cvmliftlem14  23843  cvmlift2lem13  23861  cvmlift3  23874  linethrueu  24851  frlmup4  27356  2reu5a  28058  reuan  28061  2reurex  28062  2rexreu  28066  2reu1  28067  frgra2v  28423
This theorem was proved from axioms:  ax-1 5  ax-2 6  ax-3 7  ax-mp 8  ax-gen 1536  ax-5 1547  ax-17 1606  ax-9 1644  ax-8 1661  ax-6 1715  ax-7 1720  ax-11 1727  ax-12 1878
This theorem depends on definitions:  df-bi 177  df-or 359  df-an 360  df-tru 1310  df-ex 1532  df-nf 1535  df-sb 1639  df-eu 2160  df-mo 2161  df-rex 2562  df-reu 2563  df-rmo 2564
  Copyright terms: Public domain W3C validator