Theorem exbii

Inference adding existential quantifier to both sides of an equivalence. (Contributed by NM, 24-May-1994.)

Hypothesis
exbii.1
\( \vdash \varphi \leftrightarrow \psi \)
Conclusion
\( \vdash \exists x \, \varphi \leftrightarrow \exists x \, \psi \)
Proof
l0
exbi
\( \vdash \forall x \, (\varphi \leftrightarrow \psi) \rightarrow (\exists x \, \varphi \leftrightarrow \exists x \, \psi) \)
exbii.1
\( \vdash \varphi \leftrightarrow \psi \)
mpg l0 _