Theorem euf

Version of eu6 with disjoint variable condition replaced by nonfreeness hypothesis. (Contributed by NM, 12-Aug-1993.) (Proof shortened by Wolf Lammen, 30-Oct-2018.) Avoid [ax-13]. (Revised by Wolf Lammen, 16-Oct-2022.)

Hypothesis
euf.1
\( \vdash \Finv y \, \varphi \)
Conclusion
\( \vdash \exists{!} x \, \varphi \leftrightarrow \exists y \, \forall x \, (\varphi \leftrightarrow x = y) \)
Proof
l0
eu6
\( \vdash \exists{!} x \, \varphi \leftrightarrow \exists z \, \forall x \, (\varphi \leftrightarrow x = z) \)
l1
euf.1
nfv
nfbi l1 _
l4
nfal _
l5
nfv
equequ2
bibi2d _
albidv _
cbvexv1 l4 l5 _
\( \vdash \exists z \, \forall x \, (\varphi \leftrightarrow x = z) \leftrightarrow \exists y \, \forall x \, (\varphi \leftrightarrow x = y) \)
bitri l0 _