Definition df-reu 1627

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 1623	. 2 wff E!x e. A ph
5	2	cv 1098	. . . . 5 class x
6	5, 3	wcel 1105	. . . 4 wff x e. A
7	6, 1	wa 223	. . 3 wff (x e. A /\ ph)
8	7, 2	weu 1357	. 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 1744  reubidva 1755  reubiia 1757  reueq1f 1761  cbvreuv 1777  reurex 1899  reu5 1900  reu2 1901  reu3 1902  reu6 1903  2reuswap 1908  reuss2 2246  reuun2 2249  reupick 2250  reuuni1 2845  reucl 2848  reusn 2855  reuxfr 2867  reuhyp 2868  funcnv3 3498  feu 3586  dff3 3757  fsn 3773  aceq1 4653  aceq6b 4666  supxrre 5981  zmin 6118  climreu 6989  isumclimtf 7082  pjtheut 9365

Copyright terms: Public domain