Theorem euor2

Introduce or eliminate a disjunct in a unique existential quantifier. (Contributed by NM, 21-Oct-2005.) (Proof shortened by Andrew Salmon, 9-Jul-2011.) (Proof shortened by Wolf Lammen, 27-Dec-2018.)

Conclusion
\( \vdash \neg \exists x \, \varphi \rightarrow (\exists{!} x \, (\varphi \vee \psi) \leftrightarrow \exists{!} x \, \psi) \)
Proof
nfe1
l1
nfn _
l2
19.8a
\( \vdash \varphi \rightarrow \exists x \, \varphi \)
biorf
bicomd _
\( \vdash \neg \varphi \rightarrow (\varphi \vee \psi \leftrightarrow \psi) \)
nsyl5 l2 _
eubid l1 _