Definition df-reu 2622

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 2617	. 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  2782  nfreud  2784  reubida  2794  reubiia  2797  reueq1f  2806  reu5  2825  rmo5  2828  cbvreu  2834  reuv  2875  reu2  3025  reu6  3026  reu3  3027  2reuswap  3039  2reu5lem1  3042  cbvreucsf  3201  reuss2  3536  reuun2  3539  reupick  3540  reupick3  3541  reusn  3794  rabsneu  3796  reiotacl2  4364  reiota2  4369  funcnv3  5158  feu  5243  dff4  5422  fsn  5433