# Metamath Proof Explorer

## Theorem uniabio

Description: Part of Theorem 8.17 in Quine p. 56. This theorem serves as a lemma for the fundamental property of iota. (Contributed by Andrew Salmon, 11-Jul-2011)

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

### Proof

Step Hyp Ref Expression
1 abbi1 ${⊢}\forall {x}\phantom{\rule{.4em}{0ex}}\left({\phi }↔{x}={y}\right)\to \left\{{x}|{\phi }\right\}=\left\{{x}|{x}={y}\right\}$
2 df-sn ${⊢}\left\{{y}\right\}=\left\{{x}|{x}={y}\right\}$
3 1 2 syl6eqr ${⊢}\forall {x}\phantom{\rule{.4em}{0ex}}\left({\phi }↔{x}={y}\right)\to \left\{{x}|{\phi }\right\}=\left\{{y}\right\}$
4 3 unieqd ${⊢}\forall {x}\phantom{\rule{.4em}{0ex}}\left({\phi }↔{x}={y}\right)\to \bigcup \left\{{x}|{\phi }\right\}=\bigcup \left\{{y}\right\}$
5 vex ${⊢}{y}\in \mathrm{V}$
6 5 unisn ${⊢}\bigcup \left\{{y}\right\}={y}$
7 4 6 syl6eq ${⊢}\forall {x}\phantom{\rule{.4em}{0ex}}\left({\phi }↔{x}={y}\right)\to \bigcup \left\{{x}|{\phi }\right\}={y}$