Theorem eu6im

Description: One direction of eu6 needs fewer axioms. (Contributed by Wolf Lammen, 2-Mar-2023)

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

Proof

Step	Hyp	Ref	Expression
1		exsbim	$$⊢\exists y\forall x\left(x=y\to \phi \right)\to \exists x\phi$$
2	1	anim1i	$$⊢\left(\exists y\forall x\left(x=y\to \phi \right)\wedge \exists z\forall x\left(\phi \to x=z\right)\right)\to \left(\exists x\phi \wedge \exists z\forall x\left(\phi \to x=z\right)\right)$$
3		eu6lem	$$⊢\exists y\forall x\left(\phi \leftrightarrow x=y\right)\leftrightarrow \left(\exists y\forall x\left(x=y\to \phi \right)\wedge \exists z\forall x\left(\phi \to x=z\right)\right)$$
4		eu3v	$$⊢\exists !x\phi \leftrightarrow \left(\exists x\phi \wedge \exists z\forall x\left(\phi \to x=z\right)\right)$$
5	2 3 4	3imtr4i	$$⊢\exists y\forall x\left(\phi \leftrightarrow x=y\right)\to \exists !x\phi$$