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  2819  reu2  2991  reu6  2992  reu3  2993  2reuswapdc  3007  cbvreucsf  3189  reuss2  3484  reuun2  3487  reupick  3488  reupick3  3489  reusn  3737  rabsneu  3739  reuhypd  4561  funcnv3  5382  feu  5507  dff4im  5780  f1ompt  5785  fsn  5806  riotauni  5960  riotacl2  5968  riota1  5973  riota1a  5974  riota2df  5975  snriota  5985  riotaund  5990  acexmid  5999  climreu  11803  divalgb  12431  uptx  14942  txcn  14943  dedekindicc  15301  bdcriota  16204