Theorem euanv

Introduction of a conjunct into unique existential quantifier. (Contributed by NM, 23-Mar-1995.) Reduce dependencies on axioms. (Revised by Wolf Lammen, 14-Jan-2023.)

Conclusion
\( \vdash \exists{!} x \, (\varphi \wedge \psi) \leftrightarrow \varphi \wedge \exists{!} x \, \psi \)
Proof
l0
euex
\( \vdash \exists{!} x \, (\varphi \wedge \psi) \rightarrow \exists x \, (\varphi \wedge \psi) \)
simpl
exlimiv _
\( \vdash \exists x \, (\varphi \wedge \psi) \rightarrow \varphi \)
l3
syl l0 _
ibar
l5
eubidv _
biimprcd _
l7
jcai l3 _
biimpa l5
impbii l7 _