Theorem bj-eu3f

Description: Version of eu3v where the disjoint variable condition is replaced with a nonfreeness hypothesis. This is a "backup" of a theorem that used to be in the main part with label "eu3" and was deprecated in favor of eu3v . (Contributed by NM, 8-Jul-1994) (Proof shortened by BJ, 31-May-2019)

	Ref	Expression
Hypothesis	bj-eu3f.1	$$⊢Ⅎy\phi$$
Assertion	bj-eu3f	$$⊢\exists !x\phi \leftrightarrow \left(\exists x\phi \wedge \exists y\forall x\left(\phi \to x=y\right)\right)$$

Proof

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