Definition df-reu 2491

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 2486	. 2 wff E! x e. A ph
5	2	cv 1372	. . . . 5 class x
6	5, 3	wcel 2176	. . . 4 wff x e. A
7	6, 1	wa 104	. . 3 wff ( x e. A /\ ph )
8	7, 2	weu 2054	. 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  2678  nfreudxy  2680  reubida  2688  reubiia  2691  reueq1f  2700  reu5  2723  rmo5  2726  cbvreu  2736  cbvreuvw  2744  reuv  2791  reu2  2961  reu6  2962  reu3  2963  2reuswapdc  2977  cbvreucsf  3158  reuss2  3453  reuun2  3456  reupick  3457  reupick3  3458  reusn  3704  rabsneu  3706  reuhypd  4518  funcnv3  5336  feu  5458  dff4im  5726  f1ompt  5731  fsn  5752  riotauni  5906  riotacl2  5913  riota1  5918  riota1a  5919  riota2df  5920  snriota  5929  riotaund  5934  acexmid  5943  climreu  11608  divalgb  12236  uptx  14746  txcn  14747  dedekindicc  15105  bdcriota  15819