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

Definition df-reu 2704
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 2699 . 2  wff  E! x  e.  A  ph
52cv 1651 . . . . 5  class  x
65, 3wcel 1725 . . . 4  wff  x  e.  A
76, 1wa 359 . . 3  wff  ( x  e.  A  /\  ph )
87, 2weu 2280 . 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  2870  nfreud  2872  reubida  2882  reubiia  2885  reueq1f  2894  reu5  2913  rmo5  2916  cbvreu  2922  reuv  2963  reu2  3114  reu6  3115  reu3  3116  2reuswap  3128  2reu5lem1  3131  cbvreucsf  3305  reuss2  3613  reuun2  3616  reupick  3617  reupick3  3618  reusn  3869  rabsneu  3871  reusv2lem4  4719  reusv2lem5  4720  reusv6OLD  4726  reusv7OLD  4727  reuhypd  4742  funcnv3  5504  feu  5611  dff4  5875  f1ompt  5883  fsn  5898  riotaeqdv  6542  riotauni  6548  riotacl2  6555  riota1  6560  riota1a  6561  riota2df  6562  snriota  6572  riotaprc  6579  aceq1  7990  dfac2  8003  nqerf  8799  zmin  10562  climreu  12342  divalglem10  12914  divalgb  12916  uptx  17649  txcn  17650  q1peqb  20069  adjeu  23384  2reuswap2  23967  rmoxfrdOLD  23971  rmoxfrd  23972  axcontlem2  25896  neibastop3  26382  frgra3vlem2  28328  3vfriswmgralem  28331  frgrancvvdeqlem3  28358  frgraeu  28380
  Copyright terms: Public domain W3C validator