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

Definition df-reu 2758
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 2753 . 2
52cv 1661 . . . . 5
65, 3wcel 1724 . . . 4
76, 1wa 360 . . 3
87, 2weu 2305 . 2
94, 8wb 178 1
Colors of variables: wff set class
This definition is referenced by:  nfreu1  2925  nfreud  2927  reubida  2937  reubiia  2940  reueq1f  2949  reu5  2970  rmo5  2973  cbvreu  2979  reuv  3021  reu2  3173  reu6  3174  reu3  3175  2reuswap  3187  2reu5lem1  3190  cbvreucsf  3346  reuss2  3653  reuun2  3656  reupick  3657  reupick3  3658  reusn  3962  rabsneu  3964  reusv2lem4  4503  reusv2lem5  4504  reusv6OLD  4510  reusv7OLD  4511  reuhypd  4526  funcnv3  5476  feu  5583  dff4  5845  f1ompt  5853  fsn  5868  riotauni  6033  riotacl2  6041  riota1  6046  riota1a  6047  riota2df  6048  snriota  6057  riotaund  6063  aceq1  8112  dfac2  8125  nqerf  8921  zmin  10756  climreu  12820  divalglem10  13392  divalgb  13394  uptx  18161  txcn  18162  q1peqb  20581  adjeu  23903  2reuswap2  24488  rmoxfrdOLD  24492  rmoxfrd  24493  axcontlem2  26734  neibastop3  27254  frgra3vlem2  29452  3vfriswmgralem  29455  frgrancvvdeqlem3  29484  frgraeu  29506
  Copyright terms: Public domain W3C validator