Metamath Proof Explorer

Theorem reuun2

Description: Transfer uniqueness to a smaller or larger class. (Contributed by NM, 21-Oct-2005) (Proof shortened by Wolf Lammen, 15-May-2025)

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 6 7 8 3bitri ⊢ x ∈ A ∪ B ∧ φ ↔ x ∈ B ∧ φ ∨ x ∈ A ∧ φ
10 9 eubii ⊢ ∃! x x ∈ A ∪ B ∧ φ ↔ ∃! x x ∈ B ∧ φ ∨ x ∈ A ∧ φ
11 4 10 bitri ⊢ ∃! x ∈ A ∪ B φ ↔ ∃! x x ∈ B ∧ φ ∨ x ∈ A ∧ φ
12 df-reu ⊢ ∃! x ∈ A φ ↔ ∃! x x ∈ A ∧ φ
13 3 11 12 3bitr4g ⊢ ¬ ∃ x ∈ B φ → ∃! x ∈ A ∪ B φ ↔ ∃! x ∈ A φ