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 ( ( { 𝑥 ∈ 𝐴 ∣ 𝜑 } ∪ { 𝑥 ∈ 𝐴 ∣ 𝜓 } ) ∪ { 𝑥 ∈ 𝐴 ∣ 𝜒 } ) = { 𝑥 ∈ 𝐴 ∣ ( 𝜑 ∨ 𝜓 ∨ 𝜒 ) }

Proof

Step Hyp Ref Expression
1 unrab ⊢ ( { 𝑥 ∈ 𝐴 ∣ ( 𝜑 ∨ 𝜓 ) } ∪ { 𝑥 ∈ 𝐴 ∣ 𝜒 } ) = { 𝑥 ∈ 𝐴 ∣ ( ( 𝜑 ∨ 𝜓 ) ∨ 𝜒 ) }
2 unrab ⊢ ( { 𝑥 ∈ 𝐴 ∣ 𝜑 } ∪ { 𝑥 ∈ 𝐴 ∣ 𝜓 } ) = { 𝑥 ∈ 𝐴 ∣ ( 𝜑 ∨ 𝜓 ) }
3 2 uneq1i ⊢ ( ( { 𝑥 ∈ 𝐴 ∣ 𝜑 } ∪ { 𝑥 ∈ 𝐴 ∣ 𝜓 } ) ∪ { 𝑥 ∈ 𝐴 ∣ 𝜒 } ) = ( { 𝑥 ∈ 𝐴 ∣ ( 𝜑 ∨ 𝜓 ) } ∪ { 𝑥 ∈ 𝐴 ∣ 𝜒 } )
4 df-3or ⊢ ( ( 𝜑 ∨ 𝜓 ∨ 𝜒 ) ↔ ( ( 𝜑 ∨ 𝜓 ) ∨ 𝜒 ) )
5 4 rabbii ⊢ { 𝑥 ∈ 𝐴 ∣ ( 𝜑 ∨ 𝜓 ∨ 𝜒 ) } = { 𝑥 ∈ 𝐴 ∣ ( ( 𝜑 ∨ 𝜓 ) ∨ 𝜒 ) }
6 1 3 5 3eqtr4i ⊢ ( ( { 𝑥 ∈ 𝐴 ∣ 𝜑 } ∪ { 𝑥 ∈ 𝐴 ∣ 𝜓 } ) ∪ { 𝑥 ∈ 𝐴 ∣ 𝜒 } ) = { 𝑥 ∈ 𝐴 ∣ ( 𝜑 ∨ 𝜓 ∨ 𝜒 ) }