Metamath Proof Explorer


Theorem resco

Description: Associative law for the restriction of a composition. (Contributed by NM, 12-Dec-2006)

Ref Expression
Assertion resco ABC=ABC

Proof

Step Hyp Ref Expression
1 relres RelABC
2 relco RelABC
3 vex xV
4 vex yV
5 3 4 brco xAByzxBzzAy
6 5 anbi2i xCxAByxCzxBzzAy
7 19.42v zxCxBzzAyxCzxBzzAy
8 vex zV
9 8 brresi xBCzxCxBz
10 9 anbi1i xBCzzAyxCxBzzAy
11 anass xCxBzzAyxCxBzzAy
12 10 11 bitr2i xCxBzzAyxBCzzAy
13 12 exbii zxCxBzzAyzxBCzzAy
14 6 7 13 3bitr2i xCxAByzxBCzzAy
15 4 brresi xABCyxCxABy
16 3 4 brco xABCyzxBCzzAy
17 14 15 16 3bitr4i xABCyxABCy
18 1 2 17 eqbrriv ABC=ABC