Definition df-reu 2493

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 2488	. 2 wff E! x e. A ph
5	2	cv 1372	. . . . 5 class x
6	5, 3	wcel 2178	. . . 4 wff x e. A
7	6, 1	wa 104	. . 3 wff ( x e. A /\ ph )
8	7, 2	weu 2055	. 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  2680  nfreudxy  2682  reubida  2690  reubiia  2694  reueq1f  2703  reu5  2726  rmo5  2729  cbvreu  2740  cbvreuvw  2748  reuv  2796  reu2  2968  reu6  2969  reu3  2970  2reuswapdc  2984  cbvreucsf  3166  reuss2  3461  reuun2  3464  reupick  3465  reupick3  3466  reusn  3714  rabsneu  3716  reuhypd  4536  funcnv3  5355  feu  5480  dff4im  5749  f1ompt  5754  fsn  5775  riotauni  5929  riotacl2  5936  riota1  5941  riota1a  5942  riota2df  5943  snriota  5952  riotaund  5957  acexmid  5966  climreu  11723  divalgb  12351  uptx  14861  txcn  14862  dedekindicc  15220  bdcriota  16018