Metamath Proof Explorer


Theorem brin

Description: The intersection of two relations. (Contributed by FL, 7-Oct-2008)

Ref Expression
Assertion brin ARSBARBASB

Proof

Step Hyp Ref Expression
1 elin ABRSABRABS
2 df-br ARSBABRS
3 df-br ARBABR
4 df-br ASBABS
5 3 4 anbi12i ARBASBABRABS
6 1 2 5 3bitr4i ARSBARBASB