Metamath Proof Explorer

Theorem undisjrab

Description: Union of two disjoint restricted class abstractions; compare unrab . (Contributed by Steve Rodriguez, 28-Feb-2020)

Ref Expression
Assertion undisjrab ⊢ x ∈ A | φ ∩ x ∈ A | ψ = ∅ ↔ x ∈ A | φ ∪ x ∈ A | ψ = x ∈ A | φ ⊻ ψ

Proof

Step Hyp Ref Expression
1 rabeq0 ⊢ x ∈ A | φ ∧ ψ = ∅ ↔ ∀ x ∈ A ¬ φ ∧ ψ
2 df-nan ⊢ φ ⊼ ψ ↔ ¬ φ ∧ ψ
3 nanorxor ⊢ φ ⊼ ψ ↔ φ ∨ ψ ↔ φ ⊻ ψ
4 2 3 bitr3i ⊢ ¬ φ ∧ ψ ↔ φ ∨ ψ ↔ φ ⊻ ψ
5 4 ralbii ⊢ ∀ x ∈ A ¬ φ ∧ ψ ↔ ∀ x ∈ A φ ∨ ψ ↔ φ ⊻ ψ
6 rabbi ⊢ ∀ x ∈ A φ ∨ ψ ↔ φ ⊻ ψ ↔ x ∈ A | φ ∨ ψ = x ∈ A | φ ⊻ ψ
7 1 5 6 3bitri ⊢ x ∈ A | φ ∧ ψ = ∅ ↔ x ∈ A | φ ∨ ψ = x ∈ A | φ ⊻ ψ
8 inrab ⊢ x ∈ A | φ ∩ x ∈ A | ψ = x ∈ A | φ ∧ ψ
9 8 eqeq1i ⊢ x ∈ A | φ ∩ x ∈ A | ψ = ∅ ↔ x ∈ A | φ ∧ ψ = ∅
10 unrab ⊢ x ∈ A | φ ∪ x ∈ A | ψ = x ∈ A | φ ∨ ψ
11 10 eqeq1i ⊢ x ∈ A | φ ∪ x ∈ A | ψ = x ∈ A | φ ⊻ ψ ↔ x ∈ A | φ ∨ ψ = x ∈ A | φ ⊻ ψ
12 7 9 11 3bitr4i ⊢ x ∈ A | φ ∩ x ∈ A | ψ = ∅ ↔ x ∈ A | φ ∪ x ∈ A | ψ = x ∈ A | φ ⊻ ψ