# Metamath Proof Explorer

## Theorem iotabi

Description: Equivalence theorem for descriptions. (Contributed by Andrew Salmon, 30-Jun-2011)

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

### Proof

Step Hyp Ref Expression
1 abbi1 ${⊢}\forall {x}\phantom{\rule{.4em}{0ex}}\left({\phi }↔{\psi }\right)\to \left\{{x}|{\phi }\right\}=\left\{{x}|{\psi }\right\}$
2 1 eqeq1d ${⊢}\forall {x}\phantom{\rule{.4em}{0ex}}\left({\phi }↔{\psi }\right)\to \left(\left\{{x}|{\phi }\right\}=\left\{{z}\right\}↔\left\{{x}|{\psi }\right\}=\left\{{z}\right\}\right)$
3 2 abbidv ${⊢}\forall {x}\phantom{\rule{.4em}{0ex}}\left({\phi }↔{\psi }\right)\to \left\{{z}|\left\{{x}|{\phi }\right\}=\left\{{z}\right\}\right\}=\left\{{z}|\left\{{x}|{\psi }\right\}=\left\{{z}\right\}\right\}$
4 3 unieqd ${⊢}\forall {x}\phantom{\rule{.4em}{0ex}}\left({\phi }↔{\psi }\right)\to \bigcup \left\{{z}|\left\{{x}|{\phi }\right\}=\left\{{z}\right\}\right\}=\bigcup \left\{{z}|\left\{{x}|{\psi }\right\}=\left\{{z}\right\}\right\}$
5 df-iota ${⊢}\left(\iota {x}|{\phi }\right)=\bigcup \left\{{z}|\left\{{x}|{\phi }\right\}=\left\{{z}\right\}\right\}$
6 df-iota ${⊢}\left(\iota {x}|{\psi }\right)=\bigcup \left\{{z}|\left\{{x}|{\psi }\right\}=\left\{{z}\right\}\right\}$
7 4 5 6 3eqtr4g ${⊢}\forall {x}\phantom{\rule{.4em}{0ex}}\left({\phi }↔{\psi }\right)\to \left(\iota {x}|{\phi }\right)=\left(\iota {x}|{\psi }\right)$