Theorem euorv

Introduce a disjunct into a unique existential quantifier. Version of euor requiring disjoint variables, but fewer axioms. (Contributed by NM, 23-Mar-1995.) Reduce dependencies on axioms. (Revised by Wolf Lammen, 14-Jan-2023.)

Conclusion
\( \vdash \neg \varphi \wedge \exists{!} x \, \psi \rightarrow \exists{!} x \, (\varphi \vee \psi) \)
Proof
biorf
eubidv _
biimpa _