Theorem eubii

Introduce unique existential quantifier to both sides of an equivalence. (Contributed by NM, 9-Jul-1994.) (Revised by Mario Carneiro, 6-Oct-2016.)

Hypothesis
eubii.1
\( \vdash \varphi \leftrightarrow \psi \)
Conclusion
\( \vdash \exists{!} x \, \varphi \leftrightarrow \exists{!} x \, \psi \)
Proof
l0
eubi
\( \vdash \forall x \, (\varphi \leftrightarrow \psi) \rightarrow (\exists{!} x \, \varphi \leftrightarrow \exists{!} x \, \psi) \)
eubii.1
\( \vdash \varphi \leftrightarrow \psi \)
mpg l0 _