df-iota - New Foundations Explorer

	New Foundations Explorer		< Previous Next > Nearby theorems
Mirrors > Home > NFE Home > Th. List > df-iota		Unicode version

Definition df-iota 4339

Description: Define Russell's definition description binder, which can be read as "the unique

such that

," where

ordinarily contains

as a free variable. Our definition is meaningful only when there is exactly one

such that

is true (see iotaval 4350); otherwise, it evaluates to the empty set (see iotanul 4354). Russell used the inverted iota symbol

to represent the binder. (Contributed by SF, 12-Jan-2015.)

**Assertion**
Ref	Expression
df-iota

(

)

**Detailed syntax breakdown of Definition df-iota**
Step	Hyp	Ref	Expression
1		wph	. . 3
2		vx	. . 3
3	1, 2	cio 4337	. 2
4	1, 2	cab 2339	. . . . 5
5		vy	. . . . . . 7
6	5	cv 1641	. . . . . 6
7	6	csn 3737	. . . . 5
8	4, 7	wceq 1642	. . . 4
9	8, 5	cab 2339	. . 3
10	9	cuni 3891	. 2
11	3, 10	wceq 1642	1

Colors of variables: wff setvar class

This definition is referenced by: dfiota2 4340 iotaeq 4347 iotabi 4348 fvco2 5382