# Metamath Proof Explorer

## Theorem iotaval

Description: Theorem 8.19 in Quine p. 57. This theorem is the fundamental property of iota. (Contributed by Andrew Salmon, 11-Jul-2011)

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

### Proof

Step Hyp Ref Expression
1 dfiota2 ${⊢}\left(\iota {x}|{\phi }\right)=\bigcup \left\{{z}|\forall {x}\phantom{\rule{.4em}{0ex}}\left({\phi }↔{x}={z}\right)\right\}$
2 sbeqalb ${⊢}{y}\in \mathrm{V}\to \left(\left(\forall {x}\phantom{\rule{.4em}{0ex}}\left({\phi }↔{x}={y}\right)\wedge \forall {x}\phantom{\rule{.4em}{0ex}}\left({\phi }↔{x}={z}\right)\right)\to {y}={z}\right)$
3 2 elv ${⊢}\left(\forall {x}\phantom{\rule{.4em}{0ex}}\left({\phi }↔{x}={y}\right)\wedge \forall {x}\phantom{\rule{.4em}{0ex}}\left({\phi }↔{x}={z}\right)\right)\to {y}={z}$
4 3 ex ${⊢}\forall {x}\phantom{\rule{.4em}{0ex}}\left({\phi }↔{x}={y}\right)\to \left(\forall {x}\phantom{\rule{.4em}{0ex}}\left({\phi }↔{x}={z}\right)\to {y}={z}\right)$
5 equequ2 ${⊢}{y}={z}\to \left({x}={y}↔{x}={z}\right)$
6 5 bibi2d ${⊢}{y}={z}\to \left(\left({\phi }↔{x}={y}\right)↔\left({\phi }↔{x}={z}\right)\right)$
7 6 biimpd ${⊢}{y}={z}\to \left(\left({\phi }↔{x}={y}\right)\to \left({\phi }↔{x}={z}\right)\right)$
8 7 alimdv ${⊢}{y}={z}\to \left(\forall {x}\phantom{\rule{.4em}{0ex}}\left({\phi }↔{x}={y}\right)\to \forall {x}\phantom{\rule{.4em}{0ex}}\left({\phi }↔{x}={z}\right)\right)$
9 8 com12 ${⊢}\forall {x}\phantom{\rule{.4em}{0ex}}\left({\phi }↔{x}={y}\right)\to \left({y}={z}\to \forall {x}\phantom{\rule{.4em}{0ex}}\left({\phi }↔{x}={z}\right)\right)$
10 4 9 impbid ${⊢}\forall {x}\phantom{\rule{.4em}{0ex}}\left({\phi }↔{x}={y}\right)\to \left(\forall {x}\phantom{\rule{.4em}{0ex}}\left({\phi }↔{x}={z}\right)↔{y}={z}\right)$
11 equcom ${⊢}{y}={z}↔{z}={y}$
12 10 11 syl6bb ${⊢}\forall {x}\phantom{\rule{.4em}{0ex}}\left({\phi }↔{x}={y}\right)\to \left(\forall {x}\phantom{\rule{.4em}{0ex}}\left({\phi }↔{x}={z}\right)↔{z}={y}\right)$
13 12 alrimiv ${⊢}\forall {x}\phantom{\rule{.4em}{0ex}}\left({\phi }↔{x}={y}\right)\to \forall {z}\phantom{\rule{.4em}{0ex}}\left(\forall {x}\phantom{\rule{.4em}{0ex}}\left({\phi }↔{x}={z}\right)↔{z}={y}\right)$
14 uniabio ${⊢}\forall {z}\phantom{\rule{.4em}{0ex}}\left(\forall {x}\phantom{\rule{.4em}{0ex}}\left({\phi }↔{x}={z}\right)↔{z}={y}\right)\to \bigcup \left\{{z}|\forall {x}\phantom{\rule{.4em}{0ex}}\left({\phi }↔{x}={z}\right)\right\}={y}$
15 13 14 syl ${⊢}\forall {x}\phantom{\rule{.4em}{0ex}}\left({\phi }↔{x}={y}\right)\to \bigcup \left\{{z}|\forall {x}\phantom{\rule{.4em}{0ex}}\left({\phi }↔{x}={z}\right)\right\}={y}$
16 1 15 syl5eq ${⊢}\forall {x}\phantom{\rule{.4em}{0ex}}\left({\phi }↔{x}={y}\right)\to \left(\iota {x}|{\phi }\right)={y}$