Definition df-reu 2482

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 2477	. 2 wff E! x e. A ph
5	2	cv 1363	. . . . 5 class x
6	5, 3	wcel 2167	. . . 4 wff x e. A
7	6, 1	wa 104	. . 3 wff ( x e. A /\ ph )
8	7, 2	weu 2045	. 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  2669  nfreudxy  2671  reubida  2679  reubiia  2682  reueq1f  2691  reu5  2714  rmo5  2717  cbvreu  2727  cbvreuvw  2735  reuv  2782  reu2  2952  reu6  2953  reu3  2954  2reuswapdc  2968  cbvreucsf  3149  reuss2  3443  reuun2  3446  reupick  3447  reupick3  3448  reusn  3693  rabsneu  3695  reuhypd  4506  funcnv3  5320  feu  5440  dff4im  5708  f1ompt  5713  fsn  5734  riotauni  5884  riotacl2  5891  riota1  5896  riota1a  5897  riota2df  5898  snriota  5907  riotaund  5912  acexmid  5921  climreu  11462  divalgb  12090  uptx  14510  txcn  14511  dedekindicc  14869  bdcriota  15529