Definition df-reu 2535

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 2530	. 2 wff E! x e. A ph
5	2	cv 1401	. . . . 5 class x
6	5, 3	wcel 2209	. . . 4 wff x e. A
7	6, 1	wa 104	. . 3 wff ( x e. A /\ ph )
8	7, 2	weu 2086	. 2 wff E! x ( x e. A /\ ph )
9	4, 8	wb 105	1 wff ( E! x e. A ph <-> E! x ( x e. A /\ ph ) )

This definition is referenced by:  nfreu1  2723  nfreudxy  2725  reubida  2734  reubiia  2738  reueq1f  2747  reu5  2770  rmo5  2773  cbvreu  2784  cbvreuvw  2792  reuv  2841  reu2  3014  reu6  3015  reu3  3016  2reuswapdc  3030  cbvreucsf  3212  reuss2  3513  reuun2  3516  reupick  3517  reupick3  3518  reusn  3781  rabsneu  3783  reuhypd  4615  funcnv3  5441  feu  5572  dff4im  5848  f1ompt  5853  fsn  5874  riotauni  6038  riotacl2  6046  riota1  6051  riota1a  6052  riota2df  6053  snriota  6063  riotaund  6068  acexmid  6077  climreu  12044  divalgb  12673  uptx  15301  txcn  15302  dedekindicc  15660  bdcriota  16826