Definition df-reu 2449

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 2444	. 2 wff E! x e. A ph
5	2	cv 1341	. . . . 5 class x
6	5, 3	wcel 2135	. . . 4 wff x e. A
7	6, 1	wa 103	. . 3 wff ( x e. A /\ ph )
8	7, 2	weu 2013	. 2 wff E! x ( x e. A /\ ph )
9	4, 8	wb 104	1 wff ( E! x e. A ph <-> E! x ( x e. A /\ ph ) )

This definition is referenced by:  nfreu1  2635  nfreudxy  2637  reubida  2645  reubiia  2648  reueq1f  2657  reu5  2676  rmo5  2679  cbvreu  2687  cbvreuvw  2695  reuv  2740  reu2  2909  reu6  2910  reu3  2911  2reuswapdc  2925  cbvreucsf  3104  reuss2  3397  reuun2  3400  reupick  3401  reupick3  3402  reusn  3641  rabsneu  3643  reuhypd  4443  funcnv3  5244  feu  5364  dff4im  5625  f1ompt  5630  fsn  5651  riotauni  5798  riotacl2  5805  riota1  5810  riota1a  5811  riota2df  5812  snriota  5821  riotaund  5826  acexmid  5835  climreu  11224  divalgb  11847  uptx  12815  txcn  12816  dedekindicc  13152  bdcriota  13600