Description: Intersection of binary relation with Cartesian product. (Contributed by NM, 9-Mar-1997)
Ref | Expression | ||
---|---|---|---|
Assertion | brinxp | |- ( ( A e. C /\ B e. D ) -> ( A R B <-> A ( R i^i ( C X. D ) ) B ) ) |
Step | Hyp | Ref | Expression |
---|---|---|---|
1 | brinxp2 | |- ( A ( R i^i ( C X. D ) ) B <-> ( ( A e. C /\ B e. D ) /\ A R B ) ) |
|
2 | 1 | baibr | |- ( ( A e. C /\ B e. D ) -> ( A R B <-> A ( R i^i ( C X. D ) ) B ) ) |