Metamath Proof Explorer


Theorem xrninxp2

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 ) ) }

Proof

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 ) ) }