Definition df-iota

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 ); otherwise, it evaluates to the empty set (see iotanul ). 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 riotacl2 (or iotacl for unbounded iota), as demonstrated in the proof of supub . This can be easier than applying riotasbc or 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)

	Ref	Expression
Assertion	df-iota	$$⊢\left(\iota x|\phi \right)=\bigcup \left\{y|\left\{x|\phi \right\}=\left\{y\right\}\right\}$$

Detailed syntax breakdown

Step	Hyp	Ref	Expression
0		vx	$$setvarx$$
1		wph	$$wff\phi$$
2	1 0	cio	$$class\left(\iota x|\phi \right)$$
3		vy	$$setvary$$
4	1 0	cab	$$class\left\{x|\phi \right\}$$
5	3	cv	$$setvary$$
6	5	csn	$$class\left\{y\right\}$$
7	4 6	wceq	$$wff\left\{x|\phi \right\}=\left\{y\right\}$$
8	7 3	cab	$$class\left\{y|\left\{x|\phi \right\}=\left\{y\right\}\right\}$$
9	8	cuni	$$class\bigcup \left\{y|\left\{x|\phi \right\}=\left\{y\right\}\right\}$$
10	2 9	wceq	$$wff\left(\iota x|\phi \right)=\bigcup \left\{y|\left\{x|\phi \right\}=\left\{y\right\}\right\}$$