Metamath Proof Explorer

Theorem reuun2

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

Ref Expression
Assertion reuun2 ⊢ ¬ ∃ x ∈ B φ → ∃! x ∈ A ∪ B φ ↔ ∃! x ∈ A φ

Proof

Step Hyp Ref Expression
1 df-rex ⊢ ∃ x ∈ B φ ↔ ∃ x x ∈ B ∧ φ
2 euor2 ⊢ ¬ ∃ x x ∈ B ∧ φ → ∃! x x ∈ B ∧ φ ∨ x ∈ A ∧ φ ↔ ∃! x x ∈ A ∧ φ
3 1 2 sylnbi ⊢ ¬ ∃ x ∈ B φ → ∃! x x ∈ B ∧ φ ∨ x ∈ A ∧ φ ↔ ∃! x x ∈ A ∧ φ
4 df-reu ⊢ ∃! x ∈ A ∪ B φ ↔ ∃! x x ∈ A ∪ B ∧ φ
5 elun ⊢ x ∈ A ∪ B ↔ x ∈ A ∨ x ∈ B
6 5 anbi1i ⊢ x ∈ A ∪ B ∧ φ ↔ x ∈ A ∨ x ∈ B ∧ φ
7 andir ⊢ x ∈ A ∨ x ∈ B ∧ φ ↔ x ∈ A ∧ φ ∨ x ∈ B ∧ φ
8 orcom ⊢ x ∈ A ∧ φ ∨ x ∈ B ∧ φ ↔ x ∈ B ∧ φ ∨ x ∈ A ∧ φ
9 7 8 bitri ⊢ x ∈ A ∨ x ∈ B ∧ φ ↔ x ∈ B ∧ φ ∨ x ∈ A ∧ φ
10 6 9 bitri ⊢ x ∈ A ∪ B ∧ φ ↔ x ∈ B ∧ φ ∨ x ∈ A ∧ φ
11 10 eubii ⊢ ∃! x x ∈ A ∪ B ∧ φ ↔ ∃! x x ∈ B ∧ φ ∨ x ∈ A ∧ φ
12 4 11 bitri ⊢ ∃! x ∈ A ∪ B φ ↔ ∃! x x ∈ B ∧ φ ∨ x ∈ A ∧ φ
13 df-reu ⊢ ∃! x ∈ A φ ↔ ∃! x x ∈ A ∧ φ
14 3 12 13 3bitr4g ⊢ ¬ ∃ x ∈ B φ → ∃! x ∈ A ∪ B φ ↔ ∃! x ∈ A φ