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

Definition df-reu 2799
Description: Define restricted existential uniqueness. (Contributed by NM, 22-Nov-1994.)
Assertion
Ref Expression
df-reu

Detailed syntax breakdown of Definition df-reu
StepHypRef Expression
1 wph . . 3
2 vx . . 3
3 cA . . 3
41, 2, 3wreu 2794 . 2
52cv 1369 . . . . 5
65, 3wcel 1757 . . . 4
76, 1wa 369 . . 3
87, 2weu 2259 . 2
94, 8wb 184 1
Colors of variables: wff setvar class
This definition is referenced by:  nfreu1  2971  nfreud  2973  reubida  2983  reubiia  2986  reueq1f  2995  reu5  3016  rmo5  3019  cbvreu  3025  reuv  3068  reu2  3228  reu6  3229  reu3  3230  2reuswap  3243  2reu5lem1  3246  cbvreucsf  3403  reuss2  3712  reuun2  3715  reupick  3716  reupick3  3717  reusn  4030  rabsneu  4032  reusv2lem4  4578  reusv2lem5  4579  reusv6OLD  4585  reusv7OLD  4586  reuhypd  4601  funcnv3  5561  feu  5669  dff4  5940  f1ompt  5948  fsn  5964  riotauni  6141  riotacl2  6149  riota1  6154  riota1a  6155  riota2df  6156  snriota  6165  riotaund  6171  aceq1  8372  dfac2  8385  nqerf  9184  zmin  11034  climreu  13120  divalglem10  13692  divalgb  13694  uptx  19298  txcn  19299  q1peqb  21726  axcontlem2  23330  adjeu  25412  2reuswap2  25991  rmoxfrdOLD  25995  rmoxfrd  25996  neibastop3  28705  frgra3vlem2  30715  3vfriswmgralem  30718  frgrancvvdeqlem3  30747  frgraeu  30769
  Copyright terms: Public domain W3C validator