NFE Home New Foundations Explorer < Previous   Next >
Nearby theorems
Mirrors  >  Home  >  NFE Home  >  Th. List  >  df-reu Unicode version

Definition df-reu 2621
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 2616 . 2
52cv 1641 . . . . 5
65, 3wcel 1710 . . . 4
76, 1wa 358 . . 3
87, 2weu 2204 . 2
94, 8wb 176 1
Colors of variables: wff setvar class
This definition is referenced by:  nfreu1  2781  nfreud  2783  reubida  2793  reubiia  2796  reueq1f  2805  reu5  2824  rmo5  2827  cbvreu  2833  reuv  2874  reu2  3024  reu6  3025  reu3  3026  2reuswap  3038  2reu5lem1  3041  cbvreucsf  3200  reuss2  3535  reuun2  3538  reupick  3539  reupick3  3540  reusn  3793  rabsneu  3795  reiotacl2  4363  reiota2  4368  funcnv3  5157  feu  5242  dff4  5421  fsn  5432
  Copyright terms: Public domain W3C validator