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\phi \to \exists x\neg \phi$$

Proof

Step	Hyp	Ref	Expression
1		dtru	$$⊢\neg \forall xx=y$$
2		albi	$$⊢\forall x\left(\phi \leftrightarrow x=y\right)\to \left(\forall x\phi \leftrightarrow \forall xx=y\right)$$
3	1 2	mtbiri	$$⊢\forall x\left(\phi \leftrightarrow x=y\right)\to \neg \forall x\phi$$
4	3	exlimiv	$$⊢\exists y\forall x\left(\phi \leftrightarrow x=y\right)\to \neg \forall x\phi$$
5		eu6	$$⊢\exists !x\phi \leftrightarrow \exists y\forall x\left(\phi \leftrightarrow x=y\right)$$
6		exnal	$$⊢\exists x\neg \phi \leftrightarrow \neg \forall x\phi$$
7	4 5 6	3imtr4i	$$⊢\exists !x\phi \to \exists x\neg \phi$$