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  4562  funcnv3  5383  feu  5508  dff4im  5781  f1ompt  5786  fsn  5807  riotauni  5961  riotacl2  5969  riota1  5974  riota1a  5975  riota2df  5976  snriota  5986  riotaund  5991  acexmid  6000  climreu  11808  divalgb  12436  uptx  14948  txcn  14949  dedekindicc  15307  bdcriota  16246