Definition df-iota 4340

Description: Define Russell's definition description binder, which can be read as "the unique x such that φ," where φ ordinarily contains x as a free variable. Our definition is meaningful only when there is exactly one x such that φ is true (see iotaval 4351); otherwise, it evaluates to the empty set (see iotanul 4355). Russell used the inverted iota symbol ℩ to represent the binder. (Contributed by SF, 12-Jan-2015.)

Assertion

Ref	Expression
df-iota	⊢ (℩xφ) = ∪{y ∣ {x ∣ φ} = {y}}

Distinct variable groups:   x,y   φ,y

Allowed substitution hint:   φ(x)

Detailed syntax breakdown of Definition df-iota

Step	Hyp	Ref	Expression
1		wph	. . 3 wff φ
2		vx	. . 3 setvar x
3	1, 2	cio 4338	. 2 class (℩xφ)
4	1, 2	cab 2339	. . . . 5 class {x ∣ φ}
5		vy	. . . . . . 7 setvar y
6	5	cv 1641	. . . . . 6 class y
7	6	csn 3738	. . . . 5 class {y}
8	4, 7	wceq 1642	. . . 4 wff {x ∣ φ} = {y}
9	8, 5	cab 2339	. . 3 class {y ∣ {x ∣ φ} = {y}}
10	9	cuni 3892	. 2 class ∪{y ∣ {x ∣ φ} = {y}}
11	3, 10	wceq 1642	1 wff (℩xφ) = ∪{y ∣ {x ∣ φ} = {y}}

This definition is referenced by:  dfiota2  4341  iotaeq  4348  iotabi  4349  fvco2  5383