# Metamath Proof Explorer

## Theorem dfiota4

Description: The iota operation using the if operator. (Contributed by Scott Fenton, 6-Oct-2017) (Proof shortened by JJ, 28-Oct-2021)

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

### Proof

Step Hyp Ref Expression
1 iotauni ${⊢}\exists !{x}\phantom{\rule{.4em}{0ex}}{\phi }\to \left(\iota {x}|{\phi }\right)=\bigcup \left\{{x}|{\phi }\right\}$
2 iotanul ${⊢}¬\exists !{x}\phantom{\rule{.4em}{0ex}}{\phi }\to \left(\iota {x}|{\phi }\right)=\varnothing$
3 ifval ${⊢}\left(\iota {x}|{\phi }\right)=if\left(\exists !{x}\phantom{\rule{.4em}{0ex}}{\phi },\bigcup \left\{{x}|{\phi }\right\},\varnothing \right)↔\left(\left(\exists !{x}\phantom{\rule{.4em}{0ex}}{\phi }\to \left(\iota {x}|{\phi }\right)=\bigcup \left\{{x}|{\phi }\right\}\right)\wedge \left(¬\exists !{x}\phantom{\rule{.4em}{0ex}}{\phi }\to \left(\iota {x}|{\phi }\right)=\varnothing \right)\right)$
4 1 2 3 mpbir2an ${⊢}\left(\iota {x}|{\phi }\right)=if\left(\exists !{x}\phantom{\rule{.4em}{0ex}}{\phi },\bigcup \left\{{x}|{\phi }\right\},\varnothing \right)$