Description: Intersection of binary relation with Cartesian product. (Contributed by NM, 3-Mar-2007) (Revised by Mario Carneiro, 26-Apr-2015) Group conjuncts and avoid df-3an . (Revised by Peter Mazsa, 18-Sep-2022)
Ref | Expression | ||
---|---|---|---|
Assertion | brinxp2 | |- ( C ( R i^i ( A X. B ) ) D <-> ( ( C e. A /\ D e. B ) /\ C R D ) ) |
Step | Hyp | Ref | Expression |
---|---|---|---|
1 | brin | |- ( C ( R i^i ( A X. B ) ) D <-> ( C R D /\ C ( A X. B ) D ) ) |
|
2 | ancom | |- ( ( C R D /\ C ( A X. B ) D ) <-> ( C ( A X. B ) D /\ C R D ) ) |
|
3 | brxp | |- ( C ( A X. B ) D <-> ( C e. A /\ D e. B ) ) |
|
4 | 3 | anbi1i | |- ( ( C ( A X. B ) D /\ C R D ) <-> ( ( C e. A /\ D e. B ) /\ C R D ) ) |
5 | 1 2 4 | 3bitri | |- ( C ( R i^i ( A X. B ) ) D <-> ( ( C e. A /\ D e. B ) /\ C R D ) ) |