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

Definition df-reu 2656
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 2651 . 2  wff  E! x  e.  A  ph
52cv 1648 . . . . 5  class  x
65, 3wcel 1717 . . . 4  wff  x  e.  A
76, 1wa 359 . . 3  wff  ( x  e.  A  /\  ph )
87, 2weu 2238 . 2  wff  E! x
( x  e.  A  /\  ph )
94, 8wb 177 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  2821  nfreud  2823  reubida  2833  reubiia  2836  reueq1f  2845  reu5  2864  rmo5  2867  cbvreu  2873  reuv  2914  reu2  3065  reu6  3066  reu3  3067  2reuswap  3079  2reu5lem1  3082  cbvreucsf  3256  reuss2  3564  reuun2  3567  reupick  3568  reupick3  3569  reusn  3820  rabsneu  3822  reusv2lem4  4667  reusv2lem5  4668  reusv6OLD  4674  reusv7OLD  4675  reuhypd  4690  funcnv3  5452  feu  5559  dff4  5822  f1ompt  5830  fsn  5845  riotaeqdv  6486  riotauni  6492  riotacl2  6499  riota1  6504  riota1a  6505  riota2df  6506  snriota  6516  riotaprc  6523  aceq1  7931  dfac2  7944  nqerf  8740  zmin  10502  climreu  12277  divalglem10  12849  divalgb  12851  uptx  17578  txcn  17579  q1peqb  19944  adjeu  23240  2reuswap2  23819  rmoxfrdOLD  23823  rmoxfrd  23824  axcontlem2  25618  neibastop3  26082  frgra3vlem2  27754  3vfriswmgralem  27757  frgrancvvdeqlem3  27784
  Copyright terms: Public domain W3C validator