Definition df-iota 5219

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 5230); otherwise, it evaluates to the empty set (see iotanul 5234). 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 5243 (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 5217	. 2 class ( iota x ph )
4	1, 2	cab 2182	. . . . 5 class { x | ph }
5		vy	. . . . . . 7 setvar y
6	5	cv 1363	. . . . . 6 class y
7	6	csn 3622	. . . . 5 class { y }
8	4, 7	wceq 1364	. . . 4 wff { x | ph } = { y }
9	8, 5	cab 2182	. . 3 class { y | { x | ph } = { y } }
10	9	cuni 3839	. 2 class U. { y | { x | ph } = { y } }
11	3, 10	wceq 1364	1 wff ( iota x ph ) = U. { y | { x | ph } = { y } }

This definition is referenced by:  dfiota2  5220  iotaeq  5227  iotabi  5228  iotass  5236  dffv4g  5555  nfvres  5592