# Metamath Proof Explorer

## 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 ${setvar}{x}$
1 wph ${wff}{\phi }$
2 1 0 cio ${class}\left(\iota {x}|{\phi }\right)$
3 vy ${setvar}{y}$
4 1 0 cab ${class}\left\{{x}|{\phi }\right\}$
5 3 cv ${setvar}{y}$
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\}$