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

Definition df-reu 2701
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 2696 . 2
52cv 1686 . . . . 5
65, 3wcel 1749 . . . 4
76, 1wa 362 . . 3
87, 2weu 2244 . 2
94, 8wb 178 1
Colors of variables: wff setvar class
This definition is referenced by:  nfreu1  2870  nfreud  2872  reubida  2882  reubiia  2885  reueq1f  2894  reu5  2915  rmo5  2918  cbvreu  2924  reuv  2967  reu2  3125  reu6  3126  reu3  3127  2reuswap  3139  2reu5lem1  3142  cbvreucsf  3298  reuss2  3607  reuun2  3610  reupick  3611  reupick3  3612  reusn  3923  rabsneu  3925  reusv2lem4  4468  reusv2lem5  4469  reusv6OLD  4475  reusv7OLD  4476  reuhypd  4491  funcnv3  5449  feu  5557  dff4  5827  f1ompt  5835  fsn  5850  riotauni  6027  riotacl2  6035  riota1  6040  riota1a  6041  riota2df  6042  snriota  6051  riotaund  6057  aceq1  8234  dfac2  8247  nqerf  9045  zmin  10894  climreu  12975  divalglem10  13546  divalgb  13548  uptx  18902  txcn  18903  q1peqb  21367  axcontlem2  22890  adjeu  24972  2reuswap2  25552  rmoxfrdOLD  25556  rmoxfrd  25557  neibastop3  28254  frgra3vlem2  30267  3vfriswmgralem  30270  frgrancvvdeqlem3  30299  frgraeu  30321
  Copyright terms: Public domain W3C validator