Theorem eu4

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

	Ref	Expression
Hypothesis	eu4.1	$$⊢x=y\to \left(\phi \leftrightarrow \psi \right)$$
Assertion	eu4	$$⊢\exists !x\phi \leftrightarrow \left(\exists x\phi \wedge \forall x\forall y\left(\left(\phi \wedge \psi \right)\to x=y\right)\right)$$

Proof

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