Theorem eupickb

Existential uniqueness "pick" showing wff equivalence. (Contributed by NM, 25-Nov-1994.) (Proof shortened by Wolf Lammen, 27-Dec-2018.)

Conclusion
\( \vdash \exists{!} x \, \varphi \wedge \exists{!} x \, \psi \wedge \exists x \, (\varphi \wedge \psi) \rightarrow (\varphi \leftrightarrow \psi) \)
Proof
eupick
l1
3adant2 _
l2
exancom
\( \vdash \exists x \, (\varphi \wedge \psi) \leftrightarrow \exists x \, (\psi \wedge \varphi) \)
eupick
\( \vdash \exists{!} x \, \psi \wedge \exists x \, (\psi \wedge \varphi) \rightarrow \psi \rightarrow \varphi \)
sylan2b l2 _
3adant1 _
impbid l1 _