Metamath Proof Explorer


Theorem cnviin

Description: The converse of an intersection is the intersection of the converse. (Contributed by FL, 15-Oct-2012)

Ref Expression
Assertion cnviin AxAB-1=xAB-1

Proof

Step Hyp Ref Expression
1 relcnv RelxAB-1
2 relcnv RelB-1
3 df-rel RelB-1B-1V×V
4 2 3 mpbi B-1V×V
5 4 rgenw xAB-1V×V
6 r19.2z AxAB-1V×VxAB-1V×V
7 5 6 mpan2 AxAB-1V×V
8 iinss xAB-1V×VxAB-1V×V
9 7 8 syl AxAB-1V×V
10 df-rel RelxAB-1xAB-1V×V
11 9 10 sylibr ARelxAB-1
12 opex baV
13 eliin baVbaxABxAbaB
14 12 13 ax-mp baxABxAbaB
15 vex aV
16 vex bV
17 15 16 opelcnv abxAB-1baxAB
18 opex abV
19 eliin abVabxAB-1xAabB-1
20 18 19 ax-mp abxAB-1xAabB-1
21 15 16 opelcnv abB-1baB
22 21 ralbii xAabB-1xAbaB
23 20 22 bitri abxAB-1xAbaB
24 14 17 23 3bitr4i abxAB-1abxAB-1
25 24 eqrelriv RelxAB-1RelxAB-1xAB-1=xAB-1
26 1 11 25 sylancr AxAB-1=xAB-1