Theorem mojust

Soundness justification theorem for [df-mo]. (Contributed by NM, 11-Mar-2010.) Added this theorem by adapting the proof of eujust. (Revised by BJ, 30-Sep-2022.)

Conclusion
\( \vdash \exists y \, \forall x \, (\varphi \rightarrow x = y) \leftrightarrow \exists z \, \forall x \, (\varphi \rightarrow x = z) \)
Proof
equequ2
imbi2d _
albidv _
cbvexvw _