Theorem nfeu1ALT

Alternate version of nfeu1 with a shorter proof but using [ax-12]. Bound-variable hypothesis builder for uniqueness. See also nfeu1. (Contributed by NM, 9-Jul-1994.) (Revised by Mario Carneiro, 7-Oct-2016.) (Proof modification is discouraged.) (New usage is discouraged.)

Conclusion
\( \vdash \Finv x \, \exists{!} x \, \varphi \)
Proof
l0
eu6
\( \vdash \exists{!} x \, \varphi \leftrightarrow \exists y \, \forall x \, (\varphi \leftrightarrow x = y) \)
nfexa2
\( \vdash \Finv x \, \exists y \, \forall x \, (\varphi \leftrightarrow x = y) \)
nfxfr l0 _