Theorem euor2

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

	Ref	Expression
Assertion	euor2	$$⊢\neg \exists x\phi \to \left(\exists !x\left(\phi \vee \psi \right)\leftrightarrow \exists !x\psi \right)$$

Proof

Step	Hyp	Ref	Expression
1		nfe1	$$⊢Ⅎx\exists x\phi$$
2	1	nfn	$$⊢Ⅎx\neg \exists x\phi$$
3		19.8a	$$⊢\phi \to \exists x\phi$$
4		biorf	$$⊢\neg \phi \to \left(\psi \leftrightarrow \left(\phi \vee \psi \right)\right)$$
5	4	bicomd	$$⊢\neg \phi \to \left(\left(\phi \vee \psi \right)\leftrightarrow \psi \right)$$
6	3 5	nsyl5	$$⊢\neg \exists x\phi \to \left(\left(\phi \vee \psi \right)\leftrightarrow \psi \right)$$
7	2 6	eubid	$$⊢\neg \exists x\phi \to \left(\exists !x\left(\phi \vee \psi \right)\leftrightarrow \exists !x\psi \right)$$