Metamath Proof Explorer


Theorem cnvco2

Description: Another distributive law of converse over class composition. (Contributed by Scott Fenton, 3-May-2014)

Ref Expression
Assertion cnvco2 A B -1 -1 = B A -1

Proof

Step Hyp Ref Expression
1 relcnv Rel A B -1 -1
2 relco Rel B A -1
3 vex y V
4 vex z V
5 3 4 brcnv y B -1 z z B y
6 vex x V
7 6 4 brcnv x A -1 z z A x
8 7 bicomi z A x x A -1 z
9 5 8 anbi12ci y B -1 z z A x x A -1 z z B y
10 9 exbii z y B -1 z z A x z x A -1 z z B y
11 6 3 opelcnv x y A B -1 -1 y x A B -1
12 3 6 opelco y x A B -1 z y B -1 z z A x
13 11 12 bitri x y A B -1 -1 z y B -1 z z A x
14 6 3 opelco x y B A -1 z x A -1 z z B y
15 10 13 14 3bitr4i x y A B -1 -1 x y B A -1
16 1 2 15 eqrelriiv A B -1 -1 = B A -1