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

Metamath Proof Explorer

Theorem cnvdif

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

Ref Expression
Assertion cnvdif 
|- `' ( A \ B ) = ( `' A \ `' B )

Proof

Step Hyp Ref Expression
1 relcnv 
 |-  Rel `' ( A \ B )
2 difss 
 |-  ( `' A \ `' B ) C_ `' A
3 relcnv 
 |-  Rel `' A
4 relss 
 |-  ( ( `' A \ `' B ) C_ `' A -> ( Rel `' A -> Rel ( `' A \ `' B ) ) )
5 2 3 4 mp2 
 |-  Rel ( `' A \ `' B )
6 eldif 
 |-  ( <. y , x >. e. ( A \ B ) <-> ( <. y , x >. e. A /\ -. <. y , x >. e. B ) )
7 vex 
 |-  x e. _V
8 vex 
 |-  y e. _V
9 7 8 opelcnv 
 |-  ( <. x , y >. e. `' ( A \ B ) <-> <. y , x >. e. ( A \ B ) )
10 eldif 
 |-  ( <. x , y >. e. ( `' A \ `' B ) <-> ( <. x , y >. e. `' A /\ -. <. x , y >. e. `' B ) )
11 7 8 opelcnv 
 |-  ( <. x , y >. e. `' A <-> <. y , x >. e. A )
12 7 8 opelcnv 
 |-  ( <. x , y >. e. `' B <-> <. y , x >. e. B )
13 12 notbii 
 |-  ( -. <. x , y >. e. `' B <-> -. <. y , x >. e. B )
14 11 13 anbi12i 
 |-  ( ( <. x , y >. e. `' A /\ -. <. x , y >. e. `' B ) <-> ( <. y , x >. e. A /\ -. <. y , x >. e. B ) )
15 10 14 bitri 
 |-  ( <. x , y >. e. ( `' A \ `' B ) <-> ( <. y , x >. e. A /\ -. <. y , x >. e. B ) )
16 6 9 15 3bitr4i 
 |-  ( <. x , y >. e. `' ( A \ B ) <-> <. x , y >. e. ( `' A \ `' B ) )
17 1 5 16 eqrelriiv 
 |-  `' ( A \ B ) = ( `' A \ `' B )