# Metamath Proof Explorer

## Theorem eu4

Description: Uniqueness using implicit substitution. (Contributed by NM, 26-Jul-1995)

Ref Expression
Hypothesis eu4.1 ${⊢}{x}={y}\to \left({\phi }↔{\psi }\right)$
Assertion eu4 ${⊢}\exists !{x}\phantom{\rule{.4em}{0ex}}{\phi }↔\left(\exists {x}\phantom{\rule{.4em}{0ex}}{\phi }\wedge \forall {x}\phantom{\rule{.4em}{0ex}}\forall {y}\phantom{\rule{.4em}{0ex}}\left(\left({\phi }\wedge {\psi }\right)\to {x}={y}\right)\right)$

### Proof

Step Hyp Ref Expression
1 eu4.1 ${⊢}{x}={y}\to \left({\phi }↔{\psi }\right)$
2 df-eu ${⊢}\exists !{x}\phantom{\rule{.4em}{0ex}}{\phi }↔\left(\exists {x}\phantom{\rule{.4em}{0ex}}{\phi }\wedge {\exists }^{*}{x}\phantom{\rule{.4em}{0ex}}{\phi }\right)$
3 1 mo4 ${⊢}{\exists }^{*}{x}\phantom{\rule{.4em}{0ex}}{\phi }↔\forall {x}\phantom{\rule{.4em}{0ex}}\forall {y}\phantom{\rule{.4em}{0ex}}\left(\left({\phi }\wedge {\psi }\right)\to {x}={y}\right)$
4 3 anbi2i ${⊢}\left(\exists {x}\phantom{\rule{.4em}{0ex}}{\phi }\wedge {\exists }^{*}{x}\phantom{\rule{.4em}{0ex}}{\phi }\right)↔\left(\exists {x}\phantom{\rule{.4em}{0ex}}{\phi }\wedge \forall {x}\phantom{\rule{.4em}{0ex}}\forall {y}\phantom{\rule{.4em}{0ex}}\left(\left({\phi }\wedge {\psi }\right)\to {x}={y}\right)\right)$
5 2 4 bitri ${⊢}\exists !{x}\phantom{\rule{.4em}{0ex}}{\phi }↔\left(\exists {x}\phantom{\rule{.4em}{0ex}}{\phi }\wedge \forall {x}\phantom{\rule{.4em}{0ex}}\forall {y}\phantom{\rule{.4em}{0ex}}\left(\left({\phi }\wedge {\psi }\right)\to {x}={y}\right)\right)$