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

Definition df-reu 2714
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 2709 . 2  wff  E! x  e.  A  ph
52cv 1652 . . . . 5  class  x
65, 3wcel 1726 . . . 4  wff  x  e.  A
76, 1wa 360 . . 3  wff  ( x  e.  A  /\  ph )
87, 2weu 2283 . 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  2880  nfreud  2882  reubida  2892  reubiia  2895  reueq1f  2904  reu5  2923  rmo5  2926  cbvreu  2932  reuv  2973  reu2  3124  reu6  3125  reu3  3126  2reuswap  3138  2reu5lem1  3141  cbvreucsf  3315  reuss2  3623  reuun2  3626  reupick  3627  reupick3  3628  reusn  3879  rabsneu  3881  reusv2lem4  4730  reusv2lem5  4731  reusv6OLD  4737  reusv7OLD  4738  reuhypd  4753  funcnv3  5515  feu  5622  dff4  5886  f1ompt  5894  fsn  5909  riotaeqdv  6553  riotauni  6559  riotacl2  6566  riota1  6571  riota1a  6572  riota2df  6573  snriota  6583  riotaprc  6590  aceq1  8003  dfac2  8016  nqerf  8812  zmin  10575  climreu  12355  divalglem10  12927  divalgb  12929  uptx  17662  txcn  17663  q1peqb  20082  adjeu  23397  2reuswap2  23980  rmoxfrdOLD  23984  rmoxfrd  23985  axcontlem2  25909  neibastop3  26405  frgra3vlem2  28465  3vfriswmgralem  28468  frgrancvvdeqlem3  28495  frgraeu  28517
  Copyright terms: Public domain W3C validator