# Metamath Proof Explorer

## Theorem unass

Description: Associative law for union of classes. Exercise 8 of TakeutiZaring p. 17. (Contributed by NM, 3-May-1994) (Proof shortened by Andrew Salmon, 26-Jun-2011)

Ref Expression
Assertion unass ${⊢}\left({A}\cup {B}\right)\cup {C}={A}\cup \left({B}\cup {C}\right)$

### Proof

Step Hyp Ref Expression
1 elun ${⊢}{x}\in \left({A}\cup \left({B}\cup {C}\right)\right)↔\left({x}\in {A}\vee {x}\in \left({B}\cup {C}\right)\right)$
2 elun ${⊢}{x}\in \left({B}\cup {C}\right)↔\left({x}\in {B}\vee {x}\in {C}\right)$
3 2 orbi2i ${⊢}\left({x}\in {A}\vee {x}\in \left({B}\cup {C}\right)\right)↔\left({x}\in {A}\vee \left({x}\in {B}\vee {x}\in {C}\right)\right)$
4 elun ${⊢}{x}\in \left({A}\cup {B}\right)↔\left({x}\in {A}\vee {x}\in {B}\right)$
5 4 orbi1i ${⊢}\left({x}\in \left({A}\cup {B}\right)\vee {x}\in {C}\right)↔\left(\left({x}\in {A}\vee {x}\in {B}\right)\vee {x}\in {C}\right)$
6 orass ${⊢}\left(\left({x}\in {A}\vee {x}\in {B}\right)\vee {x}\in {C}\right)↔\left({x}\in {A}\vee \left({x}\in {B}\vee {x}\in {C}\right)\right)$
7 5 6 bitr2i ${⊢}\left({x}\in {A}\vee \left({x}\in {B}\vee {x}\in {C}\right)\right)↔\left({x}\in \left({A}\cup {B}\right)\vee {x}\in {C}\right)$
8 1 3 7 3bitrri ${⊢}\left({x}\in \left({A}\cup {B}\right)\vee {x}\in {C}\right)↔{x}\in \left({A}\cup \left({B}\cup {C}\right)\right)$
9 8 uneqri ${⊢}\left({A}\cup {B}\right)\cup {C}={A}\cup \left({B}\cup {C}\right)$