Definition df-reu 1651

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 1647	. 2 wff E!x e. A ph
5	2	cv 955	. . . . 5 class x
6	5, 3	wcel 958	. . . 4 wff x e. A
7	6, 1	wa 223	. . 3 wff (x e. A /\ ph)
8	7, 2	weu 1380	. 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 1768  reubidva 1779  reubiia 1781  reueq1f 1785  cbvreuv 1802  reurex 1928  reu5 1929  reu2 1930  reu3 1931  reu6 1932  2reuswap 1937  reuss2 2275  reuun2 2278  reupick 2279  reuuni1 2882  reucl 2885  reusn 2892  reuxfr 2904  reuhyp 2905  funcnv3 3558  feu 3647  dff3 3818  fsn 3834  aceq1 4721  aceq6b 4734  supxrre 6071  zmin 6207  climreu 7086  isumclimtf 7180  pjtheut 9221

Copyright terms: Public domain