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

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	$⊢ {(A \cap B)}^{-1} = A^{-1} \cap B^{-1}$

Proof

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