# Metamath Proof Explorer

## Theorem reuabaiotaiota

Description: The iota and the alternate iota over a wff ph are equal iff there is a unique satisfying value of { x | ph } = { y } . (Contributed by AV, 25-Aug-2022)

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

### Proof

Step Hyp Ref Expression
1 uniintab ${⊢}\exists !{y}\phantom{\rule{.4em}{0ex}}\left\{{x}|{\phi }\right\}=\left\{{y}\right\}↔\bigcup \left\{{y}|\left\{{x}|{\phi }\right\}=\left\{{y}\right\}\right\}=\bigcap \left\{{y}|\left\{{x}|{\phi }\right\}=\left\{{y}\right\}\right\}$
2 df-iota ${⊢}\left(\iota {x}|{\phi }\right)=\bigcup \left\{{y}|\left\{{x}|{\phi }\right\}=\left\{{y}\right\}\right\}$
3 df-aiota ${⊢}\iota =\bigcap \left\{{y}|\left\{{x}|{\phi }\right\}=\left\{{y}\right\}\right\}$
4 2 3 eqeq12i ${⊢}\left(\iota {x}|{\phi }\right)=\iota ↔\bigcup \left\{{y}|\left\{{x}|{\phi }\right\}=\left\{{y}\right\}\right\}=\bigcap \left\{{y}|\left\{{x}|{\phi }\right\}=\left\{{y}\right\}\right\}$
5 1 4 bitr4i ${⊢}\exists !{y}\phantom{\rule{.4em}{0ex}}\left\{{x}|{\phi }\right\}=\left\{{y}\right\}↔\left(\iota {x}|{\phi }\right)=\iota$