Description: The intersection of two relations. (Contributed by FL, 7-Oct-2008)
Ref | Expression | ||
---|---|---|---|
Assertion | brin | |
Step | Hyp | Ref | Expression |
---|---|---|---|
1 | elin | |
|
2 | df-br | |
|
3 | df-br | |
|
4 | df-br | |
|
5 | 3 4 | anbi12i | |
6 | 1 2 5 | 3bitr4i | |