Definition df-iota 5160

Description: Define Russell's definition description binder, which can be read as "the unique x such that ph," where ph ordinarily contains x as a free variable. Our definition is meaningful only when there is exactly one x such that ph is true (see iotaval 5171); otherwise, it evaluates to the empty set (see iotanul 5175). Russell used the inverted iota symbol iota to represent the binder.

Sometimes proofs need to expand an iota-based definition. That is, given "X = the x for which ... x ... x ..." holds, the proof needs to get to "... X ... X ...". A general strategy to do this is to use iotacl 5183 (for unbounded iota). This can be easier than applying a version that applies an explicit substitution, because substituting an iota into its own property always has a bound variable clash which must be first renamed or else guarded with NF.

(Contributed by Andrew Salmon, 30-Jun-2011.)

Assertion

Ref	Expression
df-iota	|- ( iota x ph ) = U. { y | { x | ph } = { y } }

Distinct variable groups:   x, y   ph, y

Allowed substitution hint:   ph( x)

Detailed syntax breakdown of Definition df-iota

Step	Hyp	Ref	Expression
1		wph	. . 3 wff ph
2		vx	. . 3 setvar x
3	1, 2	cio 5158	. 2 class ( iota x ph )
4	1, 2	cab 2156	. . . . 5 class { x | ph }
5		vy	. . . . . . 7 setvar y
6	5	cv 1347	. . . . . 6 class y
7	6	csn 3583	. . . . 5 class { y }
8	4, 7	wceq 1348	. . . 4 wff { x | ph } = { y }
9	8, 5	cab 2156	. . 3 class { y | { x | ph } = { y } }
10	9	cuni 3796	. 2 class U. { y | { x | ph } = { y } }
11	3, 10	wceq 1348	1 wff ( iota x ph ) = U. { y | { x | ph } = { y } }

This definition is referenced by:  dfiota2  5161  iotaeq  5168  iotabi  5169  iotass  5177  dffv4g  5493  nfvres  5529