Metamath Proof Explorer


Theorem brres2

Description: Binary relation on a restriction. (Contributed by Peter Mazsa, 2-Jan-2019) (Revised by Peter Mazsa, 16-Dec-2021)

Ref Expression
Assertion brres2 B R A C B R A × ran R A C

Proof

Step Hyp Ref Expression
1 brres C ran R A B R A C B A B R C
2 1 pm5.32i C ran R A B R A C C ran R A B A B R C
3 relres Rel R A
4 3 relelrni B R A C C ran R A
5 4 pm4.71ri B R A C C ran R A B R A C
6 brinxp2 B R A × ran R A C B A C ran R A B R C
7 df-3an B A C ran R A B R C B A C ran R A B R C
8 3anan12 B A C ran R A B R C C ran R A B A B R C
9 6 7 8 3bitr2i B R A × ran R A C C ran R A B A B R C
10 2 5 9 3bitr4i B R A C B R A × ran R A C