Definition df-reu 1697

Description: Define restricted existential uniqueness.

Assertion

Ref	Expression
df-reu	⊢ (∃!x ∈ A φ ↔ ∃!x(x ∈ A ⋀ φ))

Detailed syntax breakdown of Definition df-reu

Step	Hyp	Ref	Expression
1		wph	. . 3 wff φ
2		vx	. . 3 set x
3		cA	. . 3 class A
4	1, 2, 3	wreu 1693	. 2 wff ∃!x ∈ A φ
5	2	cv 991	. . . . 5 class x
6	5, 3	wcel 994	. . . 4 wff x ∈ A
7	6, 1	wa 221	. . 3 wff (x ∈ A ⋀ φ)
8	7, 2	weu 1419	. 2 wff ∃!x(x ∈ A ⋀ φ)
9	4, 8	wb 144	1 wff (∃!x ∈ A φ ↔ ∃!x(x ∈ A ⋀ φ))

This definition is referenced by:  hbreu1 1814  reubidva 1825  reubiia 1827  reueq1f 1831  cbvreuv 1848  reurex 1974  reu5 1975  reu2 1976  reu3 1977  reu6 1978  2reuswap 1983  reuss2 2327  reuun2 2330  reupick 2331  reucl 2584  reuuni1 3106  reusn 3115  reuxfr 3127  reuhyp 3128  funcnv3 3663  feu 3754  dff4 3932  fsn 3948  aceq1 4875  aceq6b 4888  supxrre 6251  zmin 6391  climreu 7304  isumclimtfi 7399  pjtheu 9512  neibastop3 11585  ufileu 11658  uptx 11978

Copyright terms: Public domain