# Metamath Proof Explorer

## Theorem iota1

Description: Property of iota. (Contributed by NM, 23-Aug-2011) (Revised by Mario Carneiro, 23-Dec-2016)

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

### Proof

Step Hyp Ref Expression
1 eu6 ${⊢}\exists !{x}\phantom{\rule{.4em}{0ex}}{\phi }↔\exists {z}\phantom{\rule{.4em}{0ex}}\forall {x}\phantom{\rule{.4em}{0ex}}\left({\phi }↔{x}={z}\right)$
2 sp ${⊢}\forall {x}\phantom{\rule{.4em}{0ex}}\left({\phi }↔{x}={z}\right)\to \left({\phi }↔{x}={z}\right)$
3 iotaval ${⊢}\forall {x}\phantom{\rule{.4em}{0ex}}\left({\phi }↔{x}={z}\right)\to \left(\iota {x}|{\phi }\right)={z}$
4 3 eqeq2d ${⊢}\forall {x}\phantom{\rule{.4em}{0ex}}\left({\phi }↔{x}={z}\right)\to \left({x}=\left(\iota {x}|{\phi }\right)↔{x}={z}\right)$
5 2 4 bitr4d ${⊢}\forall {x}\phantom{\rule{.4em}{0ex}}\left({\phi }↔{x}={z}\right)\to \left({\phi }↔{x}=\left(\iota {x}|{\phi }\right)\right)$
6 eqcom ${⊢}{x}=\left(\iota {x}|{\phi }\right)↔\left(\iota {x}|{\phi }\right)={x}$
7 5 6 syl6bb ${⊢}\forall {x}\phantom{\rule{.4em}{0ex}}\left({\phi }↔{x}={z}\right)\to \left({\phi }↔\left(\iota {x}|{\phi }\right)={x}\right)$
8 7 exlimiv ${⊢}\exists {z}\phantom{\rule{.4em}{0ex}}\forall {x}\phantom{\rule{.4em}{0ex}}\left({\phi }↔{x}={z}\right)\to \left({\phi }↔\left(\iota {x}|{\phi }\right)={x}\right)$
9 1 8 sylbi ${⊢}\exists !{x}\phantom{\rule{.4em}{0ex}}{\phi }\to \left({\phi }↔\left(\iota {x}|{\phi }\right)={x}\right)$