# Metamath Proof Explorer

## 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)↔\left(⟨{y},{x}⟩\in {A}\wedge ¬⟨{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}↔⟨{y},{x}⟩\in \left({A}\setminus {B}\right)$
10 eldif ${⊢}⟨{x},{y}⟩\in \left({{A}}^{-1}\setminus {{B}}^{-1}\right)↔\left(⟨{x},{y}⟩\in {{A}}^{-1}\wedge ¬⟨{x},{y}⟩\in {{B}}^{-1}\right)$
11 7 8 opelcnv ${⊢}⟨{x},{y}⟩\in {{A}}^{-1}↔⟨{y},{x}⟩\in {A}$
12 7 8 opelcnv ${⊢}⟨{x},{y}⟩\in {{B}}^{-1}↔⟨{y},{x}⟩\in {B}$
13 12 notbii ${⊢}¬⟨{x},{y}⟩\in {{B}}^{-1}↔¬⟨{y},{x}⟩\in {B}$
14 11 13 anbi12i ${⊢}\left(⟨{x},{y}⟩\in {{A}}^{-1}\wedge ¬⟨{x},{y}⟩\in {{B}}^{-1}\right)↔\left(⟨{y},{x}⟩\in {A}\wedge ¬⟨{y},{x}⟩\in {B}\right)$
15 10 14 bitri ${⊢}⟨{x},{y}⟩\in \left({{A}}^{-1}\setminus {{B}}^{-1}\right)↔\left(⟨{y},{x}⟩\in {A}\wedge ¬⟨{y},{x}⟩\in {B}\right)$
16 6 9 15 3bitr4i ${⊢}⟨{x},{y}⟩\in {\left({A}\setminus {B}\right)}^{-1}↔⟨{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}$