This is an inofficial mirror of http://metamath.tirix.org for personal testing of a visualizer extension only.

Metamath Proof Explorer

Theorem 3unrab

Description: Union of three restricted class abstractions. (Contributed by Thierry Arnoux, 6-Jul-2025)

Ref Expression
Assertion 3unrab ⊢ x ∈ A | φ ∪ x ∈ A | ψ ∪ x ∈ A | χ = x ∈ A | φ ∨ ψ ∨ χ

Proof

Step Hyp Ref Expression
1 unrab ⊢ x ∈ A | φ ∨ ψ ∪ x ∈ A | χ = x ∈ A | φ ∨ ψ ∨ χ
2 unrab ⊢ x ∈ A | φ ∪ x ∈ A | ψ = x ∈ A | φ ∨ ψ
3 2 uneq1i ⊢ x ∈ A | φ ∪ x ∈ A | ψ ∪ x ∈ A | χ = x ∈ A | φ ∨ ψ ∪ x ∈ A | χ
4 df-3or ⊢ φ ∨ ψ ∨ χ ↔ φ ∨ ψ ∨ χ
5 4 rabbii ⊢ x ∈ A | φ ∨ ψ ∨ χ = x ∈ A | φ ∨ ψ ∨ χ
6 1 3 5 3eqtr4i ⊢ x ∈ A | φ ∪ x ∈ A | ψ ∪ x ∈ A | χ = x ∈ A | φ ∨ ψ ∨ χ