This is an inofficial mirror of http://metamath.tirix.org for personal testing of a visualizer extension only.

Metamath Proof Explorer

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	⊢ ( ¬ ∃ 𝑥 𝜑 → ( ∃! 𝑥 ( 𝜑 ∨ 𝜓 ) ↔ ∃! 𝑥 𝜓 ) )

Proof

Step	Hyp	Ref	Expression
1		nfe1	⊢ Ⅎ 𝑥 ∃ 𝑥 𝜑
2	1	nfn	⊢ Ⅎ 𝑥 ¬ ∃ 𝑥 𝜑
3		19.8a	⊢ ( 𝜑 → ∃ 𝑥 𝜑 )
4		biorf	⊢ ( ¬ 𝜑 → ( 𝜓 ↔ ( 𝜑 ∨ 𝜓 ) ) )
5	4	bicomd	⊢ ( ¬ 𝜑 → ( ( 𝜑 ∨ 𝜓 ) ↔ 𝜓 ) )
6	3 5	nsyl5	⊢ ( ¬ ∃ 𝑥 𝜑 → ( ( 𝜑 ∨ 𝜓 ) ↔ 𝜓 ) )
7	2 6	eubid	⊢ ( ¬ ∃ 𝑥 𝜑 → ( ∃! 𝑥 ( 𝜑 ∨ 𝜓 ) ↔ ∃! 𝑥 𝜓 ) )