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

Definition df-reu 2814
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 2809 . 2
52cv 1394 . . . . 5
65, 3wcel 1818 . . . 4
76, 1wa 369 . . 3
87, 2weu 2282 . 2
94, 8wb 184 1
Colors of variables: wff setvar class
This definition is referenced by:  nfreu1  3028  nfreud  3030  reubida  3040  reubiia  3043  reueq1f  3052  reu5  3073  rmo5  3076  cbvreu  3082  reuv  3125  reu2  3287  reu6  3288  reu3  3289  2reuswap  3302  2reu5lem1  3305  cbvreucsf  3468  reuss2  3777  reuun2  3780  reupick  3781  reupick3  3782  reusn  4103  rabsneu  4105  reusv2lem4  4656  reusv2lem5  4657  reusv6OLD  4663  reusv7OLD  4664  reuhypd  4679  funcnv3  5654  feu  5766  dff4  6045  f1ompt  6053  fsn  6069  riotauni  6263  riotacl2  6271  riota1  6276  riota1a  6277  riota2df  6278  snriota  6287  riotaund  6293  aceq1  8519  dfac2  8532  nqerf  9329  zmin  11207  climreu  13379  divalglem10  14060  divalgb  14062  uptx  20126  txcn  20127  q1peqb  22555  axcontlem2  24268  frgra3vlem2  25001  3vfriswmgralem  25004  frgrancvvdeqlem3  25032  frgraeu  25054  adjeu  26808  2reuswap2  27387  rmoxfrdOLD  27391  rmoxfrd  27392  neibastop3  30180  euelss  32553
  Copyright terms: Public domain W3C validator