Definition df-reu 2621

Description: Define restricted existential uniqueness. (Contributed by NM, 22-Nov-1994.)

Assertion

Ref	Expression
df-reu	|- (E!x e. A ph <-> E!x(x e. A /\ ph))

Detailed syntax breakdown of Definition df-reu

Step	Hyp	Ref	Expression
1		wph	. . 3 wff ph
2		vx	. . 3 setvar x
3		cA	. . 3 class A
4	1, 2, 3	wreu 2616	. 2 wff E!x e. A ph
5	2	cv 1641	. . . . 5 class x
6	5, 3	wcel 1710	. . . 4 wff x e. A
7	6, 1	wa 358	. . 3 wff (x e. A /\ ph)
8	7, 2	weu 2204	. 2 wff E!x(x e. A /\ ph)
9	4, 8	wb 176	1 wff (E!x e. A ph <-> E!x(x e. A /\ ph))

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