Definition df-reu 1207

Description: Define restricted existential uniqueness.

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 set x
3		cA	. . 3 class A
4	1, 2, 3	wreu 1203	. 2 wff E!x e. A ph
5	2	cv 1089	. . . . 5 class x
6	5, 3	wcel 1092	. . . 4 wff x e. A
7	6, 1	wa 196	. . 3 wff (x e. A /\ ph)
8	7, 2	weu 1007	. 2 wff E!x(x e. A /\ ph)
9	4, 8	wb 127	1 wff (E!x e. A ph <-> E!x(x e. A /\ ph))

This definition is referenced by:  hbreu1 1307  bireudva 1317  bireua 1319  reueqf 1323  cbvreuv 1335  reurex 1337  reu2 1338  reu5 1339  2reuswap 1341  reuss 1577  reupick 1578  reuxfr 1580  reuhyp 1581  reuuni1 1955  reucl 1957  feu 2767  fsn 2895  aceq1 3552  aceq6b 3565  zmin 4617  pjthut 5243

metamath.org