# Metamath Proof Explorer

## Theorem riotauni

Description: Restricted iota in terms of class union. (Contributed by NM, 11-Oct-2011)

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

### Proof

Step Hyp Ref Expression
1 df-reu ${⊢}\exists !{x}\in {A}\phantom{\rule{.4em}{0ex}}{\phi }↔\exists !{x}\phantom{\rule{.4em}{0ex}}\left({x}\in {A}\wedge {\phi }\right)$
2 iotauni ${⊢}\exists !{x}\phantom{\rule{.4em}{0ex}}\left({x}\in {A}\wedge {\phi }\right)\to \left(\iota {x}|\left({x}\in {A}\wedge {\phi }\right)\right)=\bigcup \left\{{x}|\left({x}\in {A}\wedge {\phi }\right)\right\}$
3 1 2 sylbi ${⊢}\exists !{x}\in {A}\phantom{\rule{.4em}{0ex}}{\phi }\to \left(\iota {x}|\left({x}\in {A}\wedge {\phi }\right)\right)=\bigcup \left\{{x}|\left({x}\in {A}\wedge {\phi }\right)\right\}$
4 df-riota ${⊢}\left(\iota {x}\in {A}|{\phi }\right)=\left(\iota {x}|\left({x}\in {A}\wedge {\phi }\right)\right)$
5 df-rab ${⊢}\left\{{x}\in {A}|{\phi }\right\}=\left\{{x}|\left({x}\in {A}\wedge {\phi }\right)\right\}$
6 5 unieqi ${⊢}\bigcup \left\{{x}\in {A}|{\phi }\right\}=\bigcup \left\{{x}|\left({x}\in {A}\wedge {\phi }\right)\right\}$
7 3 4 6 3eqtr4g ${⊢}\exists !{x}\in {A}\phantom{\rule{.4em}{0ex}}{\phi }\to \left(\iota {x}\in {A}|{\phi }\right)=\bigcup \left\{{x}\in {A}|{\phi }\right\}$