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

Definition df-reu 2523
Description: Define restricted existential uniqueness. (Contributed by NM, 22-Nov-1994.)
Assertion
Ref Expression
df-reu  |-  ( E! x  e.  A  ph  <->  E! x ( x  e.  A  /\  ph )
)

Detailed syntax breakdown of Definition df-reu
StepHypRef Expression
1 wph . . 3  wff  ph
2 vx . . 3  set  x
3 cA . . 3  class  A
41, 2, 3wreu 2518 . 2  wff  E! x  e.  A  ph
52cv 1618 . . . . 5  class  x
65, 3wcel 1621 . . . 4  wff  x  e.  A
76, 1wa 360 . . 3  wff  ( x  e.  A  /\  ph )
87, 2weu 2117 . 2  wff  E! x
( x  e.  A  /\  ph )
94, 8wb 178 1  wff  ( E! x  e.  A  ph  <->  E! x ( x  e.  A  /\  ph )
)
Colors of variables: wff set class
This definition is referenced by:  nfreu1  2683  nfreud  2685  reubida  2695  reubiia  2698  reueq1f  2707  reu5  2723  rmo5  2726  cbvreu  2732  reuv  2772  reu2  2921  reu6  2922  reu3  2923  2reuswap  2933  cbvreucsf  3106  reuss2  3409  reuun2  3412  reupick  3413  reupick3  3414  reusn  3660  rabsneu  3662  reusv2lem4  4496  reusv2lem5  4497  reusv6OLD  4503  reusv7OLD  4504  reuhypd  4519  funcnv3  5235  feu  5341  dff4  5594  f1ompt  5602  fsn  5616  riotaeqdv  6259  riotauni  6265  riotacl2  6272  riota1  6277  riota1a  6278  riota2df  6279  snriota  6289  riotaprc  6296  aceq1  7698  dfac2  7711  nqerf  8508  zmin  10265  climreu  11981  divalglem10  12549  divalgb  12551  uptx  17267  txcn  17268  q1peqb  19488  adjeu  22415  axcontlem2  23954  neibastop3  25664
  Copyright terms: Public domain W3C validator