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

Metamath Proof Explorer

Theorem euorv

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

Ref Expression
Assertion euorv ⊢ ¬ φ ∧ ∃! x ψ → ∃! x φ ∨ ψ

Proof

Step Hyp Ref Expression
1 biorf ⊢ ¬ φ → ψ ↔ φ ∨ ψ
2 1 eubidv ⊢ ¬ φ → ∃! x ψ ↔ ∃! x φ ∨ ψ
3 2 biimpa ⊢ ¬ φ ∧ ∃! x ψ → ∃! x φ ∨ ψ