Metamath Proof Explorer


Theorem inxp

Description: Intersection of two Cartesian products. Exercise 9 of TakeutiZaring p. 25. (Contributed by NM, 3-Aug-1994) (Proof shortened by Andrew Salmon, 27-Aug-2011) Avoid ax-10 , ax-12 . (Revised by SN, 5-May-2025)

Ref Expression
Assertion inxp A × B C × D = A C × B D

Proof

Step Hyp Ref Expression
1 relinxp Rel A × B C × D
2 relxp Rel A C × B D
3 an4 x A y B x C y D x A x C y B y D
4 opelxp x y A × B x A y B
5 opelxp x y C × D x C y D
6 4 5 anbi12i x y A × B x y C × D x A y B x C y D
7 elin x A C x A x C
8 elin y B D y B y D
9 7 8 anbi12i x A C y B D x A x C y B y D
10 3 6 9 3bitr4i x y A × B x y C × D x A C y B D
11 elin x y A × B C × D x y A × B x y C × D
12 opelxp x y A C × B D x A C y B D
13 10 11 12 3bitr4i x y A × B C × D x y A C × B D
14 1 2 13 eqrelriiv A × B C × D = A C × B D