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

Theorem reu5 3082
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 2305 . 2  |-  ( E! x ( x  e.  A  /\  ph )  <->  ( E. x ( x  e.  A  /\  ph )  /\  E* x ( x  e.  A  /\  ph ) ) )
2 df-reu 2824 . 2  |-  ( E! x  e.  A  ph  <->  E! x ( x  e.  A  /\  ph )
)
3 df-rex 2823 . . 3  |-  ( E. x  e.  A  ph  <->  E. x ( x  e.  A  /\  ph )
)
4 df-rmo 2825 . . 3  |-  ( E* x  e.  A  ph  <->  E* x ( x  e.  A  /\  ph )
)
53, 4anbi12i 697 . 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 277 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 184    /\ wa 369   E.wex 1596    e. wcel 1767   E!weu 2275   E*wmo 2276   E.wrex 2818   E!wreu 2819   E*wrmo 2820
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1601  ax-4 1612  ax-5 1680  ax-6 1719
This theorem depends on definitions:  df-bi 185  df-an 371  df-ex 1597  df-eu 2279  df-mo 2280  df-rex 2823  df-reu 2824  df-rmo 2825
This theorem is referenced by:  reurex  3083  reurmo  3084  reu4  3302  reueq  3306  reusv1  4653  wereu  4881  wereu2  4882  fncnv  5658  moriotass  6285  supeu  7926  resqreu  13066  sqrtneg  13081  sqreu  13173  catideu  14947  poslubd  15652  ismgmid  15765  mndideu  15807  evlseu  18055  frlmup4  18704  ply1divalg  22406  tglinethrueu  23872  foot  23944  mideu  23956  pjhtheu  26135  pjpreeq  26139  cnlnadjeui  26819  cvmliftlem14  28567  cvmlift2lem13  28585  cvmlift3  28598  linethrueu  29733  2reu5a  31972  reuan  31975  2reurex  31976  2rexreu  31980  2reu1  31981
  Copyright terms: Public domain W3C validator