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}$$