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

Metamath Proof Explorer

Theorem reuun1

Description: Transfer uniqueness to a smaller class. (Contributed by NM, 21-Oct-2005)

Ref Expression
Assertion reuun1 ⊢ ∃ x ∈ A φ ∧ ∃! x ∈ A ∪ B φ ∨ ψ → ∃! x ∈ A φ

Proof

Step Hyp Ref Expression
1 ssun1 ⊢ A ⊆ A ∪ B
2 orc ⊢ φ → φ ∨ ψ
3 2 rgenw ⊢ ∀ x ∈ A φ → φ ∨ ψ
4 reuss2 ⊢ A ⊆ A ∪ B ∧ ∀ x ∈ A φ → φ ∨ ψ ∧ ∃ x ∈ A φ ∧ ∃! x ∈ A ∪ B φ ∨ ψ → ∃! x ∈ A φ
5 1 3 4 mpanl12 ⊢ ∃ x ∈ A φ ∧ ∃! x ∈ A ∪ B φ ∨ ψ → ∃! x ∈ A φ