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

Definition df-reu 2563
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 2558 . 2  wff  E! x  e.  A  ph
52cv 1631 . . . . 5  class  x
65, 3wcel 1696 . . . 4  wff  x  e.  A
76, 1wa 358 . . 3  wff  ( x  e.  A  /\  ph )
87, 2weu 2156 . 2  wff  E! x
( x  e.  A  /\  ph )
94, 8wb 176 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  2723  nfreud  2725  reubida  2735  reubiia  2738  reueq1f  2747  reu5  2766  rmo5  2769  cbvreu  2775  reuv  2816  reu2  2966  reu6  2967  reu3  2968  2reuswap  2980  2reu5lem1  2983  cbvreucsf  3158  reuss2  3461  reuun2  3464  reupick  3465  reupick3  3466  reusn  3713  rabsneu  3715  reusv2lem4  4554  reusv2lem5  4555  reusv6OLD  4561  reusv7OLD  4562  reuhypd  4577  funcnv3  5327  feu  5433  dff4  5690  f1ompt  5698  fsn  5712  riotaeqdv  6321  riotauni  6327  riotacl2  6334  riota1  6339  riota1a  6340  riota2df  6341  snriota  6351  riotaprc  6358  aceq1  7760  dfac2  7773  nqerf  8570  zmin  10328  climreu  12046  divalglem10  12617  divalgb  12619  uptx  17335  txcn  17336  q1peqb  19556  adjeu  22485  2reuswap2  23153  rmoxfrdOLD  23162  rmoxfrd  23163  axcontlem2  24665  neibastop3  26414  frgra3vlem2  28425  3vfriswmgralem  28428
  Copyright terms: Public domain W3C validator