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

Definition df-reu 2719
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 2714 . 2
52cv 1653 . . . . 5
65, 3wcel 1728 . . . 4
76, 1wa 360 . . 3
87, 2weu 2288 . 2
94, 8wb 178 1
Colors of variables: wff set class
This definition is referenced by:  nfreu1  2885  nfreud  2887  reubida  2897  reubiia  2900  reueq1f  2909  reu5  2930  rmo5  2933  cbvreu  2939  reuv  2980  reu2  3131  reu6  3132  reu3  3133  2reuswap  3145  2reu5lem1  3148  cbvreucsf  3302  reuss2  3609  reuun2  3612  reupick  3613  reupick3  3614  reusn  3905  rabsneu  3907  reusv2lem4  4768  reusv2lem5  4769  reusv6OLD  4775  reusv7OLD  4776  reuhypd  4791  funcnv3  5559  feu  5666  dff4  5931  f1ompt  5939  fsn  5954  riotaeqdv  6600  riotauni  6606  riotacl2  6613  riota1  6618  riota1a  6619  riota2df  6620  snriota  6629  riotaprc  6636  aceq1  8049  dfac2  8062  nqerf  8858  zmin  10621  climreu  12401  divalglem10  12973  divalgb  12975  uptx  17708  txcn  17709  q1peqb  20128  adjeu  23443  2reuswap2  24024  rmoxfrdOLD  24028  rmoxfrd  24029  axcontlem2  26008  neibastop3  26502  frgra3vlem2  28629  3vfriswmgralem  28632  frgrancvvdeqlem3  28659  frgraeu  28681
  Copyright terms: Public domain W3C validator