# Metamath Proof Explorer

## Theorem iotaeq

Description: Equality theorem for descriptions. Usage of this theorem is discouraged because it depends on ax-13 . (Contributed by Andrew Salmon, 30-Jun-2011) (New usage is discouraged.)

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

### Proof

Step Hyp Ref Expression
1 drsb1 ${⊢}\forall {x}\phantom{\rule{.4em}{0ex}}{x}={y}\to \left(\left[{z}/{x}\right]{\phi }↔\left[{z}/{y}\right]{\phi }\right)$
2 df-clab ${⊢}{z}\in \left\{{x}|{\phi }\right\}↔\left[{z}/{x}\right]{\phi }$
3 df-clab ${⊢}{z}\in \left\{{y}|{\phi }\right\}↔\left[{z}/{y}\right]{\phi }$
4 1 2 3 3bitr4g ${⊢}\forall {x}\phantom{\rule{.4em}{0ex}}{x}={y}\to \left({z}\in \left\{{x}|{\phi }\right\}↔{z}\in \left\{{y}|{\phi }\right\}\right)$
5 4 eqrdv ${⊢}\forall {x}\phantom{\rule{.4em}{0ex}}{x}={y}\to \left\{{x}|{\phi }\right\}=\left\{{y}|{\phi }\right\}$
6 5 eqeq1d ${⊢}\forall {x}\phantom{\rule{.4em}{0ex}}{x}={y}\to \left(\left\{{x}|{\phi }\right\}=\left\{{z}\right\}↔\left\{{y}|{\phi }\right\}=\left\{{z}\right\}\right)$
7 6 abbidv ${⊢}\forall {x}\phantom{\rule{.4em}{0ex}}{x}={y}\to \left\{{z}|\left\{{x}|{\phi }\right\}=\left\{{z}\right\}\right\}=\left\{{z}|\left\{{y}|{\phi }\right\}=\left\{{z}\right\}\right\}$
8 7 unieqd ${⊢}\forall {x}\phantom{\rule{.4em}{0ex}}{x}={y}\to \bigcup \left\{{z}|\left\{{x}|{\phi }\right\}=\left\{{z}\right\}\right\}=\bigcup \left\{{z}|\left\{{y}|{\phi }\right\}=\left\{{z}\right\}\right\}$
9 df-iota ${⊢}\left(\iota {x}|{\phi }\right)=\bigcup \left\{{z}|\left\{{x}|{\phi }\right\}=\left\{{z}\right\}\right\}$
10 df-iota ${⊢}\left(\iota {y}|{\phi }\right)=\bigcup \left\{{z}|\left\{{y}|{\phi }\right\}=\left\{{z}\right\}\right\}$
11 8 9 10 3eqtr4g ${⊢}\forall {x}\phantom{\rule{.4em}{0ex}}{x}={y}\to \left(\iota {x}|{\phi }\right)=\left(\iota {y}|{\phi }\right)$