# Metamath Proof Explorer

## Theorem dfaiota2

Description: Alternate definition of the alternate version of Russell's definition of a description binder. Definition 8.18 in Quine p. 56. (Contributed by AV, 24-Aug-2022)

Ref Expression
Assertion dfaiota2 ${⊢}\iota =\bigcap \left\{{y}|\forall {x}\phantom{\rule{.4em}{0ex}}\left({\phi }↔{x}={y}\right)\right\}$

### Proof

Step Hyp Ref Expression
1 df-aiota ${⊢}\iota =\bigcap \left\{{y}|\left\{{x}|{\phi }\right\}=\left\{{y}\right\}\right\}$
2 absn ${⊢}\left\{{x}|{\phi }\right\}=\left\{{y}\right\}↔\forall {x}\phantom{\rule{.4em}{0ex}}\left({\phi }↔{x}={y}\right)$
3 2 abbii ${⊢}\left\{{y}|\left\{{x}|{\phi }\right\}=\left\{{y}\right\}\right\}=\left\{{y}|\forall {x}\phantom{\rule{.4em}{0ex}}\left({\phi }↔{x}={y}\right)\right\}$
4 3 inteqi ${⊢}\bigcap \left\{{y}|\left\{{x}|{\phi }\right\}=\left\{{y}\right\}\right\}=\bigcap \left\{{y}|\forall {x}\phantom{\rule{.4em}{0ex}}\left({\phi }↔{x}={y}\right)\right\}$
5 1 4 eqtri ${⊢}\iota =\bigcap \left\{{y}|\forall {x}\phantom{\rule{.4em}{0ex}}\left({\phi }↔{x}={y}\right)\right\}$