Theorem eujustALT

Alternate proof of eujust illustrating the use of dvelim. (Contributed by NM, 11-Mar-2010.) (Proof modification is discouraged.) (New usage is discouraged.)

Conclusion

\( \vdash \exists y \, \forall x \, (\varphi \leftrightarrow x = y) \leftrightarrow \exists z \, \forall x \, (\varphi \leftrightarrow x = z) \)

Proof

eujust