Theorem euor

Description: 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)

	Ref	Expression
Hypothesis	euor.nf	$$⊢Ⅎx\phi$$
Assertion	euor	$$⊢\left(\neg \phi \wedge \exists !x\psi \right)\to \exists !x\left(\phi \vee \psi \right)$$

Proof

Step	Hyp	Ref	Expression
1		euor.nf	$$⊢Ⅎx\phi$$
2	1	nfn	$$⊢Ⅎx\neg \phi$$
3		biorf	$$⊢\neg \phi \to \left(\psi \leftrightarrow \left(\phi \vee \psi \right)\right)$$
4	2 3	eubid	$$⊢\neg \phi \to \left(\exists !x\psi \leftrightarrow \exists !x\left(\phi \vee \psi \right)\right)$$
5	4	biimpa	$$⊢\left(\neg \phi \wedge \exists !x\psi \right)\to \exists !x\left(\phi \vee \psi \right)$$