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

Definition df-reu 2766
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 2761 . 2
52cv 1669 . . . . 5
65, 3wcel 1732 . . . 4
76, 1wa 360 . . 3
87, 2weu 2313 . 2
94, 8wb 178 1
Colors of variables: wff set class
This definition is referenced by:  nfreu1  2934  nfreud  2936  reubida  2946  reubiia  2949  reueq1f  2958  reu5  2979  rmo5  2982  cbvreu  2988  reuv  3030  reu2  3185  reu6  3186  reu3  3187  2reuswap  3199  2reu5lem1  3202  cbvreucsf  3358  reuss2  3666  reuun2  3669  reupick  3670  reupick3  3671  reusn  3977  rabsneu  3979  reusv2lem4  4519  reusv2lem5  4520  reusv6OLD  4526  reusv7OLD  4527  reuhypd  4542  funcnv3  5497  feu  5604  dff4  5873  f1ompt  5881  fsn  5896  riotauni  6069  riotacl2  6077  riota1  6082  riota1a  6083  riota2df  6084  snriota  6093  riotaund  6099  aceq1  8169  dfac2  8182  nqerf  8978  zmin  10813  climreu  12881  divalglem10  13453  divalgb  13455  uptx  18672  txcn  18673  q1peqb  21092  adjeu  24415  2reuswap2  25000  rmoxfrdOLD  25004  rmoxfrd  25005  axcontlem2  27243  neibastop3  27763  frgra3vlem2  29774  3vfriswmgralem  29777  frgrancvvdeqlem3  29806  frgraeu  29828
  Copyright terms: Public domain W3C validator