ILE Home Intuitionistic Logic Explorer < Previous   Next >
Nearby theorems
Mirrors  >  Home  >  ILE Home  >  Th. List  >  reu5 Unicode version

Theorem reu5 2539
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 1963 . 2  |-  ( E! x ( x  e.  A  /\  ph )  <->  ( E. x ( x  e.  A  /\  ph )  /\  E* x ( x  e.  A  /\  ph ) ) )
2 df-reu 2330 . 2  |-  ( E! x  e.  A  ph  <->  E! x ( x  e.  A  /\  ph )
)
3 df-rex 2329 . . 3  |-  ( E. x  e.  A  ph  <->  E. x ( x  e.  A  /\  ph )
)
4 df-rmo 2331 . . 3  |-  ( E* x  e.  A  ph  <->  E* x ( x  e.  A  /\  ph )
)
53, 4anbi12i 441 . 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 205 1  |-  ( E! x  e.  A  ph  <->  ( E. x  e.  A  ph 
/\  E* x  e.  A  ph ) )
Colors of variables: wff set class
Syntax hints:    /\ wa 101    <-> wb 102   E.wex 1397    e. wcel 1409   E!weu 1916   E*wmo 1917   E.wrex 2324   E!wreu 2325   E*wrmo 2326
This theorem was proved from axioms:  ax-1 5  ax-2 6  ax-mp 7  ax-ia1 103  ax-ia2 104  ax-ia3 105  ax-io 640  ax-5 1352  ax-7 1353  ax-gen 1354  ax-ie1 1398  ax-ie2 1399  ax-8 1411  ax-10 1412  ax-11 1413  ax-i12 1414  ax-bndl 1415  ax-4 1416  ax-17 1435  ax-i9 1439  ax-ial 1443  ax-i5r 1444
This theorem depends on definitions:  df-bi 114  df-nf 1366  df-sb 1662  df-eu 1919  df-mo 1920  df-rex 2329  df-reu 2330  df-rmo 2331
This theorem is referenced by:  reurex  2540  reurmo  2541  reu4  2758  reueq  2761  reusv1  4218  fncnv  4993  moriotass  5524  supeuti  6400  lteupri  6773  elrealeu  6964  rereceu  7021  qbtwnz  9208  rersqreu  9855  divalglemeunn  10233  divalglemeuneg  10235  pw2dvdseu  10256
  Copyright terms: Public domain W3C validator