Definition df-reu 2355

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 2350	. 2 wff E! x e. A ph
5	2	cv 1283	. . . . 5 class x
6	5, 3	wcel 1433	. . . 4 wff x e. A
7	6, 1	wa 102	. . 3 wff ( x e. A /\ ph )
8	7, 2	weu 1941	. 2 wff E! x ( x e. A /\ ph )
9	4, 8	wb 103	1 wff ( E! x e. A ph <-> E! x ( x e. A /\ ph ) )

This definition is referenced by:  nfreu1  2525  nfreudxy  2527  reubida  2535  reubiia  2538  reueq1f  2547  reu5  2566  rmo5  2569  cbvreu  2575  reuv  2618  reu2  2780  reu6  2781  reu3  2782  2reuswapdc  2794  cbvreucsf  2966  reuss2  3244  reuun2  3247  reupick  3248  reupick3  3249  reusn  3463  rabsneu  3465  reuhypd  4221  funcnv3  4981  feu  5092  dff4im  5334  f1ompt  5341  fsn  5356  riotauni  5494  riotacl2  5501  riota1  5506  riota1a  5507  riota2df  5508  snriota  5517  riotaund  5522  acexmid  5531  climreu  10136  divalgb  10325  bdcriota  10674