Theorem euor

Introduce a disjunct into a unique existential quantifier. For a version requiring disjoint variables, but fewer axioms, see euorv. (Contributed by NM, 21-Oct-2005.)

Hypothesis
euor.nf
\( \vdash \Finv x \, \varphi \)
Conclusion
\( \vdash \neg \varphi \wedge \exists{!} x \, \psi \rightarrow \exists{!} x \, (\varphi \vee \psi) \)
Proof
euor.nf
l1
nfn _
biorf
eubid l1 _
biimpa _