# Metamath Proof Explorer

## Theorem iotaexeu

Description: The iota class exists. This theorem does not require ax-nul for its proof. (Contributed by Andrew Salmon, 11-Jul-2011)

Ref Expression
Assertion iotaexeu ${⊢}\exists !{x}\phantom{\rule{.4em}{0ex}}{\phi }\to \left(\iota {x}|{\phi }\right)\in \mathrm{V}$

### Proof

Step Hyp Ref Expression
1 iotaval ${⊢}\forall {x}\phantom{\rule{.4em}{0ex}}\left({\phi }↔{x}={y}\right)\to \left(\iota {x}|{\phi }\right)={y}$
2 1 eqcomd ${⊢}\forall {x}\phantom{\rule{.4em}{0ex}}\left({\phi }↔{x}={y}\right)\to {y}=\left(\iota {x}|{\phi }\right)$
3 2 eximi ${⊢}\exists {y}\phantom{\rule{.4em}{0ex}}\forall {x}\phantom{\rule{.4em}{0ex}}\left({\phi }↔{x}={y}\right)\to \exists {y}\phantom{\rule{.4em}{0ex}}{y}=\left(\iota {x}|{\phi }\right)$
4 eu6 ${⊢}\exists !{x}\phantom{\rule{.4em}{0ex}}{\phi }↔\exists {y}\phantom{\rule{.4em}{0ex}}\forall {x}\phantom{\rule{.4em}{0ex}}\left({\phi }↔{x}={y}\right)$
5 isset ${⊢}\left(\iota {x}|{\phi }\right)\in \mathrm{V}↔\exists {y}\phantom{\rule{.4em}{0ex}}{y}=\left(\iota {x}|{\phi }\right)$
6 3 4 5 3imtr4i ${⊢}\exists !{x}\phantom{\rule{.4em}{0ex}}{\phi }\to \left(\iota {x}|{\phi }\right)\in \mathrm{V}$