Metamath Proof Explorer


Theorem brin2

Description: Binary relation on an intersection is a special case of binary relation on range Cartesian product. (Contributed by Peter Mazsa, 21-Aug-2021)

Ref Expression
Assertion brin2 AVBWARSBARSBB

Proof

Step Hyp Ref Expression
1 brin ARSBARBASB
2 brxrn AVBWBWARSBBARBASB
3 2 3anidm23 AVBWARSBBARBASB
4 1 3 bitr4id AVBWARSBARSBB