Definition df-reu 2479

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 2474	. 2 wff E! x e. A ph
5	2	cv 1363	. . . . 5 class x
6	5, 3	wcel 2164	. . . 4 wff x e. A
7	6, 1	wa 104	. . 3 wff ( x e. A /\ ph )
8	7, 2	weu 2042	. 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  2666  nfreudxy  2668  reubida  2676  reubiia  2679  reueq1f  2688  reu5  2711  rmo5  2714  cbvreu  2724  cbvreuvw  2732  reuv  2779  reu2  2949  reu6  2950  reu3  2951  2reuswapdc  2965  cbvreucsf  3146  reuss2  3440  reuun2  3443  reupick  3444  reupick3  3445  reusn  3690  rabsneu  3692  reuhypd  4503  funcnv3  5317  feu  5437  dff4im  5705  f1ompt  5710  fsn  5731  riotauni  5881  riotacl2  5888  riota1  5893  riota1a  5894  riota2df  5895  snriota  5904  riotaund  5909  acexmid  5918  climreu  11443  divalgb  12069  uptx  14453  txcn  14454  dedekindicc  14812  bdcriota  15445