Theorem dfeu

Rederive [df-eu] from the old definition eu6. (Contributed by NM, 23-Mar-1995.) (Proof shortened by Wolf Lammen, 25-May-2019.) (Proof shortened by BJ, 7-Oct-2022.) (Proof modification is discouraged.) Use [df-eu] instead. (New usage is discouraged.)

Conclusion
\( \vdash \exists{!} x \, \varphi \leftrightarrow \exists x \, \varphi \wedge \exists^\ast x \, \varphi \)
Proof
l0
abai
\( \vdash \exists x \, \varphi \wedge \exists{!} x \, \varphi \leftrightarrow \exists x \, \varphi \wedge (\exists x \, \varphi \rightarrow \exists{!} x \, \varphi) \)
euex
l2
pm4.71ri _
\( \vdash \exists{!} x \, \varphi \leftrightarrow \exists x \, \varphi \wedge \exists{!} x \, \varphi \)
moeu
anbi2i _
\( \vdash \exists x \, \varphi \wedge \exists^\ast x \, \varphi \leftrightarrow \exists x \, \varphi \wedge (\exists x \, \varphi \rightarrow \exists{!} x \, \varphi) \)
3bitr4i l0 l2 _