Description: Intersection of a range Cartesian product with a Cartesian product. (Contributed by Peter Mazsa, 8-Apr-2020)
Ref | Expression | ||
---|---|---|---|
Assertion | xrninxp2 | |- ( ( R |X. S ) i^i ( A X. ( B X. C ) ) ) = { <. u , x >. | ( x e. ( B X. C ) /\ ( u e. A /\ u ( R |X. S ) x ) ) } |
Step | Hyp | Ref | Expression |
---|---|---|---|
1 | inxp2 | |- ( ( R |X. S ) i^i ( A X. ( B X. C ) ) ) = { <. u , x >. | ( ( u e. A /\ x e. ( B X. C ) ) /\ u ( R |X. S ) x ) } |
|
2 | an21 | |- ( ( ( u e. A /\ x e. ( B X. C ) ) /\ u ( R |X. S ) x ) <-> ( x e. ( B X. C ) /\ ( u e. A /\ u ( R |X. S ) x ) ) ) |
|
3 | 2 | opabbii | |- { <. u , x >. | ( ( u e. A /\ x e. ( B X. C ) ) /\ u ( R |X. S ) x ) } = { <. u , x >. | ( x e. ( B X. C ) /\ ( u e. A /\ u ( R |X. S ) x ) ) } |
4 | 1 3 | eqtri | |- ( ( R |X. S ) i^i ( A X. ( B X. C ) ) ) = { <. u , x >. | ( x e. ( B X. C ) /\ ( u e. A /\ u ( R |X. S ) x ) ) } |