ILE Home Intuitionistic Logic Explorer < Previous   Next >
Nearby theorems
Mirrors  >  Home  >  ILE Home  >  Th. List  >  df-reu GIF version

Definition df-reu 2356
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 wff 𝜑
2 vx . . 3 setvar 𝑥
3 cA . . 3 class 𝐴
41, 2, 3wreu 2351 . 2 wff ∃!𝑥𝐴 𝜑
52cv 1284 . . . . 5 class 𝑥
65, 3wcel 1434 . . . 4 wff 𝑥𝐴
76, 1wa 102 . . 3 wff (𝑥𝐴𝜑)
87, 2weu 1942 . 2 wff ∃!𝑥(𝑥𝐴𝜑)
94, 8wb 103 1 wff (∃!𝑥𝐴 𝜑 ↔ ∃!𝑥(𝑥𝐴𝜑))
Colors of variables: wff set class
This definition is referenced by:  nfreu1  2526  nfreudxy  2528  reubida  2536  reubiia  2539  reueq1f  2548  reu5  2567  rmo5  2570  cbvreu  2576  reuv  2619  reu2  2781  reu6  2782  reu3  2783  2reuswapdc  2795  cbvreucsf  2967  reuss2  3245  reuun2  3248  reupick  3249  reupick3  3250  reusn  3465  rabsneu  3467  reuhypd  4223  funcnv3  4986  feu  5097  dff4im  5339  f1ompt  5346  fsn  5361  riotauni  5499  riotacl2  5506  riota1  5511  riota1a  5512  riota2df  5513  snriota  5522  riotaund  5527  acexmid  5536  climreu  10263  divalgb  10458  bdcriota  10817
  Copyright terms: Public domain W3C validator