Definition df-reu 2515

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 2510	. 2 wff E! x e. A ph
5	2	cv 1394	. . . . 5 class x
6	5, 3	wcel 2200	. . . 4 wff x e. A
7	6, 1	wa 104	. . 3 wff ( x e. A /\ ph )
8	7, 2	weu 2077	. 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  2703  nfreudxy  2705  reubida  2713  reubiia  2717  reueq1f  2726  reu5  2749  rmo5  2752  cbvreu  2763  cbvreuvw  2771  reuv  2820  reu2  2992  reu6  2993  reu3  2994  2reuswapdc  3008  cbvreucsf  3190  reuss2  3485  reuun2  3488  reupick  3489  reupick3  3490  reusn  3740  rabsneu  3742  reuhypd  4566  funcnv3  5389  feu  5516  dff4im  5789  f1ompt  5794  fsn  5815  riotauni  5973  riotacl2  5981  riota1  5986  riota1a  5987  riota2df  5988  snriota  5998  riotaund  6003  acexmid  6012  climreu  11848  divalgb  12476  uptx  14988  txcn  14989  dedekindicc  15347  bdcriota  16414