# Metamath Proof Explorer

## Theorem cnvin

Description: Distributive law for converse over intersection. Theorem 15 of Suppes p. 62. (Contributed by NM, 25-Mar-1998) (Revised by Mario Carneiro, 26-Jun-2014)

Ref Expression
Assertion cnvin ${⊢}{\left({A}\cap {B}\right)}^{-1}={{A}}^{-1}\cap {{B}}^{-1}$

### Proof

Step Hyp Ref Expression
1 cnvdif ${⊢}{\left({A}\setminus \left({A}\setminus {B}\right)\right)}^{-1}={{A}}^{-1}\setminus {\left({A}\setminus {B}\right)}^{-1}$
2 cnvdif ${⊢}{\left({A}\setminus {B}\right)}^{-1}={{A}}^{-1}\setminus {{B}}^{-1}$
3 2 difeq2i ${⊢}{{A}}^{-1}\setminus {\left({A}\setminus {B}\right)}^{-1}={{A}}^{-1}\setminus \left({{A}}^{-1}\setminus {{B}}^{-1}\right)$
4 1 3 eqtri ${⊢}{\left({A}\setminus \left({A}\setminus {B}\right)\right)}^{-1}={{A}}^{-1}\setminus \left({{A}}^{-1}\setminus {{B}}^{-1}\right)$
5 dfin4 ${⊢}{A}\cap {B}={A}\setminus \left({A}\setminus {B}\right)$
6 5 cnveqi ${⊢}{\left({A}\cap {B}\right)}^{-1}={\left({A}\setminus \left({A}\setminus {B}\right)\right)}^{-1}$
7 dfin4 ${⊢}{{A}}^{-1}\cap {{B}}^{-1}={{A}}^{-1}\setminus \left({{A}}^{-1}\setminus {{B}}^{-1}\right)$
8 4 6 7 3eqtr4i ${⊢}{\left({A}\cap {B}\right)}^{-1}={{A}}^{-1}\cap {{B}}^{-1}$