Metamath Proof Explorer

Theorem inass

Description: Associative law for intersection of classes. Exercise 9 of TakeutiZaring p. 17. (Contributed by NM, 3-May-1994)

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

Proof

Step Hyp Ref Expression
1 anass ${⊢}\left(\left({x}\in {A}\wedge {x}\in {B}\right)\wedge {x}\in {C}\right)↔\left({x}\in {A}\wedge \left({x}\in {B}\wedge {x}\in {C}\right)\right)$
2 elin ${⊢}{x}\in \left({B}\cap {C}\right)↔\left({x}\in {B}\wedge {x}\in {C}\right)$
3 2 anbi2i ${⊢}\left({x}\in {A}\wedge {x}\in \left({B}\cap {C}\right)\right)↔\left({x}\in {A}\wedge \left({x}\in {B}\wedge {x}\in {C}\right)\right)$
4 1 3 bitr4i ${⊢}\left(\left({x}\in {A}\wedge {x}\in {B}\right)\wedge {x}\in {C}\right)↔\left({x}\in {A}\wedge {x}\in \left({B}\cap {C}\right)\right)$
5 elin ${⊢}{x}\in \left({A}\cap {B}\right)↔\left({x}\in {A}\wedge {x}\in {B}\right)$
6 5 anbi1i ${⊢}\left({x}\in \left({A}\cap {B}\right)\wedge {x}\in {C}\right)↔\left(\left({x}\in {A}\wedge {x}\in {B}\right)\wedge {x}\in {C}\right)$
7 elin ${⊢}{x}\in \left({A}\cap \left({B}\cap {C}\right)\right)↔\left({x}\in {A}\wedge {x}\in \left({B}\cap {C}\right)\right)$
8 4 6 7 3bitr4i ${⊢}\left({x}\in \left({A}\cap {B}\right)\wedge {x}\in {C}\right)↔{x}\in \left({A}\cap \left({B}\cap {C}\right)\right)$
9 8 ineqri ${⊢}\left({A}\cap {B}\right)\cap {C}={A}\cap \left({B}\cap {C}\right)$