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

Theorem reu5 3051
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 2294 . 2  |-  ( E! x ( x  e.  A  /\  ph )  <->  ( E. x ( x  e.  A  /\  ph )  /\  E* x ( x  e.  A  /\  ph ) ) )
2 df-reu 2789 . 2  |-  ( E! x  e.  A  ph  <->  E! x ( x  e.  A  /\  ph )
)
3 df-rex 2788 . . 3  |-  ( E. x  e.  A  ph  <->  E. x ( x  e.  A  /\  ph )
)
4 df-rmo 2790 . . 3  |-  ( E* x  e.  A  ph  <->  E* x ( x  e.  A  /\  ph )
)
53, 4anbi12i 701 . 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 280 1  |-  ( E! x  e.  A  ph  <->  ( E. x  e.  A  ph 
/\  E* x  e.  A  ph ) )
Colors of variables: wff setvar class
Syntax hints:    <-> wb 187    /\ wa 370   E.wex 1659    e. wcel 1870   E!weu 2266   E*wmo 2267   E.wrex 2783   E!wreu 2784   E*wrmo 2785
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1665  ax-4 1678  ax-5 1751  ax-6 1797
This theorem depends on definitions:  df-bi 188  df-an 372  df-ex 1660  df-eu 2270  df-mo 2271  df-rex 2788  df-reu 2789  df-rmo 2790
This theorem is referenced by:  reurex  3052  reurmo  3053  reu4  3271  reueq  3275  reusv1  4625  wereu  4850  wereu2  4851  fncnv  5665  moriotass  6295  supeu  7974  resqreu  13295  sqrtneg  13310  sqreu  13402  catideu  15532  poslubd  16345  ismgmid  16458  mndideu  16501  evlseu  18674  frlmup4  19290  ply1divalg  22963  tglinethrueu  24543  foot  24621  mideu  24637  pjhtheu  26882  pjpreeq  26886  cnlnadjeui  27565  cvmliftlem14  29808  cvmlift2lem13  29826  cvmlift3  29839  linethrueu  30708  phpreu  31636  poimirlem18  31665  poimirlem21  31668  2reu5a  38001  reuan  38004  2reurex  38005  2rexreu  38009  2reu1  38010
  Copyright terms: Public domain W3C validator