Theorem euan

Introduction of a conjunct into unique existential quantifier. (Contributed by NM, 19-Feb-2005.) (Proof shortened by Andrew Salmon, 9-Jul-2011.) (Proof shortened by Wolf Lammen, 24-Dec-2018.)

Hypothesis
moanim.1
\( \vdash \Finv x \, \varphi \)
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) \)
l1
moanim.1
simpl
exlimi l1 _
\( \vdash \exists x \, (\varphi \wedge \psi) \rightarrow \varphi \)
l4
syl l0 _
l5
moanim.1
ibar
l7
eubid l5 _
biimprcd _
l9
jcai l4 _
biimpa l7
impbii l9 _