Theorem moabs

Absorption of existence condition by uniqueness. (Contributed by NM, 4-Nov-2002.) Shorten proof and avoid [df-eu]. (Revised by BJ, 14-Oct-2022.)

Conclusion
\( \vdash \exists^\ast x \, \varphi \leftrightarrow \exists x \, \varphi \rightarrow \exists^\ast x \, \varphi \)
Proof
l0
ax-1
l1
nexmo
id
ja l1 _
impbii l0 _