# Metamath Proof Explorer

## Theorem eunex

Description: Existential uniqueness implies there is a value for which the wff argument is false. (Contributed by NM, 24-Oct-2010) (Proof shortened by BJ, 2-Jan-2023)

Ref Expression
Assertion eunex ${⊢}\exists !{x}\phantom{\rule{.4em}{0ex}}{\phi }\to \exists {x}\phantom{\rule{.4em}{0ex}}¬{\phi }$

### Proof

Step Hyp Ref Expression
1 dtru ${⊢}¬\forall {x}\phantom{\rule{.4em}{0ex}}{x}={y}$
2 albi ${⊢}\forall {x}\phantom{\rule{.4em}{0ex}}\left({\phi }↔{x}={y}\right)\to \left(\forall {x}\phantom{\rule{.4em}{0ex}}{\phi }↔\forall {x}\phantom{\rule{.4em}{0ex}}{x}={y}\right)$
3 1 2 mtbiri ${⊢}\forall {x}\phantom{\rule{.4em}{0ex}}\left({\phi }↔{x}={y}\right)\to ¬\forall {x}\phantom{\rule{.4em}{0ex}}{\phi }$
4 3 exlimiv ${⊢}\exists {y}\phantom{\rule{.4em}{0ex}}\forall {x}\phantom{\rule{.4em}{0ex}}\left({\phi }↔{x}={y}\right)\to ¬\forall {x}\phantom{\rule{.4em}{0ex}}{\phi }$
5 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)$
6 exnal ${⊢}\exists {x}\phantom{\rule{.4em}{0ex}}¬{\phi }↔¬\forall {x}\phantom{\rule{.4em}{0ex}}{\phi }$
7 4 5 6 3imtr4i ${⊢}\exists !{x}\phantom{\rule{.4em}{0ex}}{\phi }\to \exists {x}\phantom{\rule{.4em}{0ex}}¬{\phi }$