Definition df-reu 2529

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 2524	. 2 wff E! x e. A ph
5	2	cv 1397	. . . . 5 class x
6	5, 3	wcel 2205	. . . 4 wff x e. A
7	6, 1	wa 104	. . 3 wff ( x e. A /\ ph )
8	7, 2	weu 2082	. 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  2717  nfreudxy  2719  reubida  2728  reubiia  2732  reueq1f  2741  reu5  2764  rmo5  2767  cbvreu  2778  cbvreuvw  2786  reuv  2835  reu2  3007  reu6  3008  reu3  3009  2reuswapdc  3023  cbvreucsf  3205  reuss2  3503  reuun2  3506  reupick  3507  reupick3  3508  reusn  3764  rabsneu  3766  reuhypd  4594  funcnv3  5420  feu  5551  dff4im  5825  f1ompt  5830  fsn  5851  riotauni  6012  riotacl2  6020  riota1  6025  riota1a  6026  riota2df  6027  snriota  6037  riotaund  6042  acexmid  6051  climreu  11986  divalgb  12615  uptx  15156  txcn  15157  dedekindicc  15515  bdcriota  16670