# Metamath Proof Explorer

## Theorem iotauni

Description: Equivalence between two different forms of iota . (Contributed by Andrew Salmon, 12-Jul-2011)

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

### Proof

Step Hyp Ref Expression
1 eu6 ${⊢}\exists !{x}\phantom{\rule{.4em}{0ex}}{\phi }↔\exists {z}\phantom{\rule{.4em}{0ex}}\forall {x}\phantom{\rule{.4em}{0ex}}\left({\phi }↔{x}={z}\right)$
2 iotaval ${⊢}\forall {x}\phantom{\rule{.4em}{0ex}}\left({\phi }↔{x}={z}\right)\to \left(\iota {x}|{\phi }\right)={z}$
3 uniabio ${⊢}\forall {x}\phantom{\rule{.4em}{0ex}}\left({\phi }↔{x}={z}\right)\to \bigcup \left\{{x}|{\phi }\right\}={z}$
4 2 3 eqtr4d ${⊢}\forall {x}\phantom{\rule{.4em}{0ex}}\left({\phi }↔{x}={z}\right)\to \left(\iota {x}|{\phi }\right)=\bigcup \left\{{x}|{\phi }\right\}$
5 4 exlimiv ${⊢}\exists {z}\phantom{\rule{.4em}{0ex}}\forall {x}\phantom{\rule{.4em}{0ex}}\left({\phi }↔{x}={z}\right)\to \left(\iota {x}|{\phi }\right)=\bigcup \left\{{x}|{\phi }\right\}$
6 1 5 sylbi ${⊢}\exists !{x}\phantom{\rule{.4em}{0ex}}{\phi }\to \left(\iota {x}|{\phi }\right)=\bigcup \left\{{x}|{\phi }\right\}$