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

Definition df-reu 2712
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 2707 . 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 2281 . 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  2878  nfreud  2880  reubida  2890  reubiia  2893  reueq1f  2902  reu5  2921  rmo5  2924  cbvreu  2930  reuv  2971  reu2  3122  reu6  3123  reu3  3124  2reuswap  3136  2reu5lem1  3139  cbvreucsf  3313  reuss2  3621  reuun2  3624  reupick  3625  reupick3  3626  reusn  3877  rabsneu  3879  reusv2lem4  4727  reusv2lem5  4728  reusv6OLD  4734  reusv7OLD  4735  reuhypd  4750  funcnv3  5512  feu  5619  dff4  5883  f1ompt  5891  fsn  5906  riotaeqdv  6550  riotauni  6556  riotacl2  6563  riota1  6568  riota1a  6569  riota2df  6570  snriota  6580  riotaprc  6587  aceq1  7998  dfac2  8011  nqerf  8807  zmin  10570  climreu  12350  divalglem10  12922  divalgb  12924  uptx  17657  txcn  17658  q1peqb  20077  adjeu  23392  2reuswap2  23975  rmoxfrdOLD  23979  rmoxfrd  23980  axcontlem2  25904  neibastop3  26391  frgra3vlem2  28391  3vfriswmgralem  28394  frgrancvvdeqlem3  28421  frgraeu  28443
  Copyright terms: Public domain W3C validator