Theorem dfeumo

Description: An elementary proof showing the reverse direction of dfmoeu . Here the characterizing expression of existential uniqueness ( eu6 ) is derived from that of uniqueness ( df-mo ). (Contributed by Wolf Lammen, 3-Oct-2023)

	Ref	Expression
Assertion	dfeumo	$$⊢\left(\exists x\phi \wedge \exists y\forall x\left(\phi \to x=y\right)\right)\leftrightarrow \exists y\forall x\left(\phi \leftrightarrow x=y\right)$$

Proof

Step	Hyp	Ref	Expression
1		ax6ev	$$⊢\exists xx=y$$
2		biimpr	$$⊢\left(\phi \leftrightarrow x=y\right)\to \left(x=y\to \phi \right)$$
3	2	aleximi	$$⊢\forall x\left(\phi \leftrightarrow x=y\right)\to \left(\exists xx=y\to \exists x\phi \right)$$
4	1 3	mpi	$$⊢\forall x\left(\phi \leftrightarrow x=y\right)\to \exists x\phi$$
5	4	exlimiv	$$⊢\exists y\forall x\left(\phi \leftrightarrow x=y\right)\to \exists x\phi$$
6	5	pm4.71ri	$$⊢\exists y\forall x\left(\phi \leftrightarrow x=y\right)\leftrightarrow \left(\exists x\phi \wedge \exists y\forall x\left(\phi \leftrightarrow x=y\right)\right)$$
7		abai	$$⊢\left(\exists x\phi \wedge \exists y\forall x\left(\phi \leftrightarrow x=y\right)\right)\leftrightarrow \left(\exists x\phi \wedge \left(\exists x\phi \to \exists y\forall x\left(\phi \leftrightarrow x=y\right)\right)\right)$$
8		dfmoeu	$$⊢\left(\exists x\phi \to \exists y\forall x\left(\phi \leftrightarrow x=y\right)\right)\leftrightarrow \exists y\forall x\left(\phi \to x=y\right)$$
9	8	anbi2i	$$⊢\left(\exists x\phi \wedge \left(\exists x\phi \to \exists y\forall x\left(\phi \leftrightarrow x=y\right)\right)\right)\leftrightarrow \left(\exists x\phi \wedge \exists y\forall x\left(\phi \to x=y\right)\right)$$
10	6 7 9	3bitrri	$$⊢\left(\exists x\phi \wedge \exists y\forall x\left(\phi \to x=y\right)\right)\leftrightarrow \exists y\forall x\left(\phi \leftrightarrow x=y\right)$$