Theorem cnvdif

Description: Distributive law for converse over class difference. (Contributed by Mario Carneiro, 26-Jun-2014)

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

Proof

Step	Hyp	Ref	Expression
1		relcnv	$$⊢\mathrm{Rel}{\left(A\setminus B\right)}^{-1}$$
2		difss	$$⊢A^{-1}\setminus B^{-1}\subseteq A^{-1}$$
3		relcnv	$$⊢\mathrm{Rel}{A}^{-1}$$
4		relss	$$⊢A^{-1}\setminus B^{-1}\subseteq A^{-1}\to \left(\mathrm{Rel}{A}^{-1}\to \mathrm{Rel}\left(A^{-1}\setminus B^{-1}\right)\right)$$
5	2 3 4	mp2	$$⊢\mathrm{Rel}\left(A^{-1}\setminus B^{-1}\right)$$
6		eldif	$$⊢⟨y,x⟩\in \left(A\setminus B\right)\leftrightarrow \left(⟨y,x⟩\in A\wedge \neg ⟨y,x⟩\in B\right)$$
7		vex	$$⊢x\in \mathrm{V}$$
8		vex	$$⊢y\in \mathrm{V}$$
9	7 8	opelcnv	$$⊢⟨x,y⟩\in {\left(A\setminus B\right)}^{-1}\leftrightarrow ⟨y,x⟩\in \left(A\setminus B\right)$$
10		eldif	$$⊢⟨x,y⟩\in \left(A^{-1}\setminus B^{-1}\right)\leftrightarrow \left(⟨x,y⟩\in A^{-1}\wedge \neg ⟨x,y⟩\in B^{-1}\right)$$
11	7 8	opelcnv	$$⊢⟨x,y⟩\in A^{-1}\leftrightarrow ⟨y,x⟩\in A$$
12	7 8	opelcnv	$$⊢⟨x,y⟩\in B^{-1}\leftrightarrow ⟨y,x⟩\in B$$
13	12	notbii	$$⊢\neg ⟨x,y⟩\in B^{-1}\leftrightarrow \neg ⟨y,x⟩\in B$$
14	11 13	anbi12i	$$⊢\left(⟨x,y⟩\in A^{-1}\wedge \neg ⟨x,y⟩\in B^{-1}\right)\leftrightarrow \left(⟨y,x⟩\in A\wedge \neg ⟨y,x⟩\in B\right)$$
15	10 14	bitri	$$⊢⟨x,y⟩\in \left(A^{-1}\setminus B^{-1}\right)\leftrightarrow \left(⟨y,x⟩\in A\wedge \neg ⟨y,x⟩\in B\right)$$
16	6 9 15	3bitr4i	$$⊢⟨x,y⟩\in {\left(A\setminus B\right)}^{-1}\leftrightarrow ⟨x,y⟩\in \left(A^{-1}\setminus B^{-1}\right)$$
17	1 5 16	eqrelriiv	$$⊢{\left(A\setminus B\right)}^{-1}=A^{-1}\setminus B^{-1}$$