# Metamath Proof Explorer

## Theorem aiotaval

Description: Theorem 8.19 in Quine p. 57. This theorem is the fundamental property of (alternate) iota. (Contributed by AV, 24-Aug-2022)

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

### Proof

Step Hyp Ref Expression
1 eusnsn ${⊢}\exists !{z}\phantom{\rule{.4em}{0ex}}\left\{{z}\right\}=\left\{{y}\right\}$
2 eqcom ${⊢}\left\{{y}\right\}=\left\{{z}\right\}↔\left\{{z}\right\}=\left\{{y}\right\}$
3 2 eubii ${⊢}\exists !{z}\phantom{\rule{.4em}{0ex}}\left\{{y}\right\}=\left\{{z}\right\}↔\exists !{z}\phantom{\rule{.4em}{0ex}}\left\{{z}\right\}=\left\{{y}\right\}$
4 1 3 mpbir ${⊢}\exists !{z}\phantom{\rule{.4em}{0ex}}\left\{{y}\right\}=\left\{{z}\right\}$
5 eqeq1 ${⊢}\left\{{x}|{\phi }\right\}=\left\{{y}\right\}\to \left(\left\{{x}|{\phi }\right\}=\left\{{z}\right\}↔\left\{{y}\right\}=\left\{{z}\right\}\right)$
6 5 eubidv ${⊢}\left\{{x}|{\phi }\right\}=\left\{{y}\right\}\to \left(\exists !{z}\phantom{\rule{.4em}{0ex}}\left\{{x}|{\phi }\right\}=\left\{{z}\right\}↔\exists !{z}\phantom{\rule{.4em}{0ex}}\left\{{y}\right\}=\left\{{z}\right\}\right)$
7 4 6 mpbiri ${⊢}\left\{{x}|{\phi }\right\}=\left\{{y}\right\}\to \exists !{z}\phantom{\rule{.4em}{0ex}}\left\{{x}|{\phi }\right\}=\left\{{z}\right\}$
8 absn ${⊢}\left\{{x}|{\phi }\right\}=\left\{{y}\right\}↔\forall {x}\phantom{\rule{.4em}{0ex}}\left({\phi }↔{x}={y}\right)$
9 reuabaiotaiota ${⊢}\exists !{z}\phantom{\rule{.4em}{0ex}}\left\{{x}|{\phi }\right\}=\left\{{z}\right\}↔\left(\iota {x}|{\phi }\right)=\iota$
10 eqcom ${⊢}\left(\iota {x}|{\phi }\right)=\iota ↔\iota =\left(\iota {x}|{\phi }\right)$
11 9 10 bitri ${⊢}\exists !{z}\phantom{\rule{.4em}{0ex}}\left\{{x}|{\phi }\right\}=\left\{{z}\right\}↔\iota =\left(\iota {x}|{\phi }\right)$
12 7 8 11 3imtr3i ${⊢}\forall {x}\phantom{\rule{.4em}{0ex}}\left({\phi }↔{x}={y}\right)\to \iota =\left(\iota {x}|{\phi }\right)$
13 iotaval ${⊢}\forall {x}\phantom{\rule{.4em}{0ex}}\left({\phi }↔{x}={y}\right)\to \left(\iota {x}|{\phi }\right)={y}$
14 12 13 eqtrd ${⊢}\forall {x}\phantom{\rule{.4em}{0ex}}\left({\phi }↔{x}={y}\right)\to \iota ={y}$