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

Definition df-reu 2550
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 2545 . 2  wff  E! x  e.  A  ph
52cv 1622 . . . . 5  class  x
65, 3wcel 1684 . . . 4  wff  x  e.  A
76, 1wa 358 . . 3  wff  ( x  e.  A  /\  ph )
87, 2weu 2143 . 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  2710  nfreud  2712  reubida  2722  reubiia  2725  reueq1f  2734  reu5  2753  rmo5  2756  cbvreu  2762  reuv  2803  reu2  2953  reu6  2954  reu3  2955  2reuswap  2967  2reu5lem1  2970  cbvreucsf  3145  reuss2  3448  reuun2  3451  reupick  3452  reupick3  3453  reusn  3700  rabsneu  3702  reusv2lem4  4538  reusv2lem5  4539  reusv6OLD  4545  reusv7OLD  4546  reuhypd  4561  funcnv3  5311  feu  5417  dff4  5674  f1ompt  5682  fsn  5696  riotaeqdv  6305  riotauni  6311  riotacl2  6318  riota1  6323  riota1a  6324  riota2df  6325  snriota  6335  riotaprc  6342  aceq1  7744  dfac2  7757  nqerf  8554  zmin  10312  climreu  12030  divalglem10  12601  divalgb  12603  uptx  17319  txcn  17320  q1peqb  19540  adjeu  22469  2reuswap2  23137  rmoxfrdOLD  23146  rmoxfrd  23147  axcontlem2  24593  neibastop3  26311  frgra3vlem2  28179  3vfriswmgralem  28182
  Copyright terms: Public domain W3C validator