Metamath Proof Explorer

Theorem unab

Description: Union of two class abstractions. (Contributed by NM, 29-Sep-2002) (Proof shortened by Andrew Salmon, 26-Jun-2011)

Ref Expression
Assertion unab ⊢ x | φ ∪ x | ψ = x | φ ∨ ψ

Proof

Step Hyp Ref Expression
1 sbor ⊢ y x φ ∨ ψ ↔ y x φ ∨ y x ψ
2 df-clab ⊢ y ∈ x | φ ∨ ψ ↔ y x φ ∨ ψ
3 df-clab ⊢ y ∈ x | φ ↔ y x φ
4 df-clab ⊢ y ∈ x | ψ ↔ y x ψ
5 3 4 orbi12i ⊢ y ∈ x | φ ∨ y ∈ x | ψ ↔ y x φ ∨ y x ψ
6 1 2 5 3bitr4ri ⊢ y ∈ x | φ ∨ y ∈ x | ψ ↔ y ∈ x | φ ∨ ψ
7 6 uneqri ⊢ x | φ ∪ x | ψ = x | φ ∨ ψ