Description: A rearrangement of intersection. (Contributed by NM, 27-Aug-2012)
Ref | Expression | ||
---|---|---|---|
Assertion | in13 | ⊢ ( 𝐴 ∩ ( 𝐵 ∩ 𝐶 ) ) = ( 𝐶 ∩ ( 𝐵 ∩ 𝐴 ) ) |
Step | Hyp | Ref | Expression |
---|---|---|---|
1 | in32 | ⊢ ( ( 𝐵 ∩ 𝐶 ) ∩ 𝐴 ) = ( ( 𝐵 ∩ 𝐴 ) ∩ 𝐶 ) | |
2 | incom | ⊢ ( 𝐴 ∩ ( 𝐵 ∩ 𝐶 ) ) = ( ( 𝐵 ∩ 𝐶 ) ∩ 𝐴 ) | |
3 | incom | ⊢ ( 𝐶 ∩ ( 𝐵 ∩ 𝐴 ) ) = ( ( 𝐵 ∩ 𝐴 ) ∩ 𝐶 ) | |
4 | 1 2 3 | 3eqtr4i | ⊢ ( 𝐴 ∩ ( 𝐵 ∩ 𝐶 ) ) = ( 𝐶 ∩ ( 𝐵 ∩ 𝐴 ) ) |