Theorem eu2

Description: An alternate way of defining existential uniqueness. Definition 6.10 of TakeutiZaring p. 26. (Contributed by NM, 8-Jul-1994) (Proof shortened by Wolf Lammen, 2-Dec-2018)

	Ref	Expression
Hypothesis	eu2.nf	$$⊢Ⅎy\phi$$
Assertion	eu2	$$⊢\exists !x\phi \leftrightarrow \left(\exists x\phi \wedge \forall x\forall y\left(\left(\phi \wedge \left[y/x\right]\phi \right)\to x=y\right)\right)$$

Proof

Step	Hyp	Ref	Expression
1		eu2.nf	$$⊢Ⅎy\phi$$
2		df-eu	$$⊢\exists !x\phi \leftrightarrow \left(\exists x\phi \wedge {\exists }^{*}x\phi \right)$$
3	1	mo3	$$⊢{\exists }^{*}x\phi \leftrightarrow \forall x\forall y\left(\left(\phi \wedge \left[y/x\right]\phi \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 \left[y/x\right]\phi \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 \left[y/x\right]\phi \right)\to x=y\right)\right)$$