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

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 ( ( 𝐴 ∩ 𝐵 ) ∩ 𝐶 ) = ( 𝐴 ∩ ( 𝐵 ∩ 𝐶 ) )

Proof

Step Hyp Ref Expression
1 anass ⊢ ( ( ( 𝑥 ∈ 𝐴 ∧ 𝑥 ∈ 𝐵 ) ∧ 𝑥 ∈ 𝐶 ) ↔ ( 𝑥 ∈ 𝐴 ∧ ( 𝑥 ∈ 𝐵 ∧ 𝑥 ∈ 𝐶 ) ) )
2 elin ⊢ ( 𝑥 ∈ ( 𝐵 ∩ 𝐶 ) ↔ ( 𝑥 ∈ 𝐵 ∧ 𝑥 ∈ 𝐶 ) )
3 2 anbi2i ⊢ ( ( 𝑥 ∈ 𝐴 ∧ 𝑥 ∈ ( 𝐵 ∩ 𝐶 ) ) ↔ ( 𝑥 ∈ 𝐴 ∧ ( 𝑥 ∈ 𝐵 ∧ 𝑥 ∈ 𝐶 ) ) )
4 1 3 bitr4i ⊢ ( ( ( 𝑥 ∈ 𝐴 ∧ 𝑥 ∈ 𝐵 ) ∧ 𝑥 ∈ 𝐶 ) ↔ ( 𝑥 ∈ 𝐴 ∧ 𝑥 ∈ ( 𝐵 ∩ 𝐶 ) ) )
5 elin ⊢ ( 𝑥 ∈ ( 𝐴 ∩ 𝐵 ) ↔ ( 𝑥 ∈ 𝐴 ∧ 𝑥 ∈ 𝐵 ) )
6 5 anbi1i ⊢ ( ( 𝑥 ∈ ( 𝐴 ∩ 𝐵 ) ∧ 𝑥 ∈ 𝐶 ) ↔ ( ( 𝑥 ∈ 𝐴 ∧ 𝑥 ∈ 𝐵 ) ∧ 𝑥 ∈ 𝐶 ) )
7 elin ⊢ ( 𝑥 ∈ ( 𝐴 ∩ ( 𝐵 ∩ 𝐶 ) ) ↔ ( 𝑥 ∈ 𝐴 ∧ 𝑥 ∈ ( 𝐵 ∩ 𝐶 ) ) )
8 4 6 7 3bitr4i ⊢ ( ( 𝑥 ∈ ( 𝐴 ∩ 𝐵 ) ∧ 𝑥 ∈ 𝐶 ) ↔ 𝑥 ∈ ( 𝐴 ∩ ( 𝐵 ∩ 𝐶 ) ) )
9 8 ineqri ⊢ ( ( 𝐴 ∩ 𝐵 ) ∩ 𝐶 ) = ( 𝐴 ∩ ( 𝐵 ∩ 𝐶 ) )