Theorem mof

Version of [df-mo] with disjoint variable condition replaced by nonfreeness hypothesis. (Contributed by NM, 8-Mar-1995.) Extract dfmo from this proof, and prove mof from it (as of 30-Sep-2022, directly from [df-mo] ). (Revised by Wolf Lammen, 28-May-2019.) Avoid [ax-13]. (Revised by Wolf Lammen, 16-Oct-2022.)

Hypothesis
mof.1
\( \vdash \Finv y \, \varphi \)
Conclusion
\( \vdash \exists^\ast x \, \varphi \leftrightarrow \exists y \, \forall x \, (\varphi \rightarrow x = y) \)
Proof
l0
dfmo
\( \vdash \exists^\ast x \, \varphi \leftrightarrow \exists z \, \forall x \, (\varphi \rightarrow x = z) \)
l1
mof.1
nfv
nfim l1 _
l4
nfal _
l5
nfv
equequ2
imbi2d _
albidv _
cbvexv1 l4 l5 _
\( \vdash \exists z \, \forall x \, (\varphi \rightarrow x = z) \leftrightarrow \exists y \, \forall x \, (\varphi \rightarrow x = y) \)
bitri l0 _