Definition df-reu 1643

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 1639	. 2 wff E!x e. A ph
5	2	cv 952	. . . . 5 class x
6	5, 3	wcel 955	. . . 4 wff x e. A
7	6, 1	wa 223	. . 3 wff (x e. A /\ ph)
8	7, 2	weu 1373	. 2 wff E!x(x e. A /\ ph)
9	4, 8	wb 146	1 wff (E!x e. A ph <-> E!x(x e. A /\ ph))

This definition is referenced by:  hbreu1 1760  reubidva 1771  reubiia 1773  reueq1f 1777  cbvreuv 1793  reurex 1918  reu5 1919  reu2 1920  reu3 1921  reu6 1922  2reuswap 1927  reuss2 2265  reuun2 2268  reupick 2269  reuuni1 2872  reucl 2875  reusn 2882  reuxfr 2894  reuhyp 2895  funcnv3 3544  feu 3632  dff3 3803  fsn 3819  aceq1 4701  aceq6b 4714  supxrre 6030  zmin 6167  climreu 7038  isumclimtf 7131  pjtheut 9151

Copyright terms: Public domain