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 A V B W A R S B A R S B B

Proof

Step Hyp Ref Expression
1 brin A R S B A R B A S B
2 brxrn A V B W B W A R S B B A R B A S B
3 2 3anidm23 A V B W A R S B B A R B A S B
4 1 3 bitr4id A V B W A R S B A R S B B