Definition df-reu 2490

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 2485	. 2 wff E! x e. A ph
5	2	cv 1371	. . . . 5 class x
6	5, 3	wcel 2175	. . . 4 wff x e. A
7	6, 1	wa 104	. . 3 wff ( x e. A /\ ph )
8	7, 2	weu 2053	. 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  2677  nfreudxy  2679  reubida  2687  reubiia  2690  reueq1f  2699  reu5  2722  rmo5  2725  cbvreu  2735  cbvreuvw  2743  reuv  2790  reu2  2960  reu6  2961  reu3  2962  2reuswapdc  2976  cbvreucsf  3157  reuss2  3452  reuun2  3455  reupick  3456  reupick3  3457  reusn  3703  rabsneu  3705  reuhypd  4517  funcnv3  5335  feu  5457  dff4im  5725  f1ompt  5730  fsn  5751  riotauni  5905  riotacl2  5912  riota1  5917  riota1a  5918  riota2df  5919  snriota  5928  riotaund  5933  acexmid  5942  climreu  11579  divalgb  12207  uptx  14717  txcn  14718  dedekindicc  15076  bdcriota  15781