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|φ⊻ψ