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)

Ref Expression
Assertion inxp A×BC×D=AC×BD

Proof

Step Hyp Ref Expression
1 inopab xy|xAyBxy|xCyD=xy|xAyBxCyD
2 an4 xAyBxCyDxAxCyByD
3 elin xACxAxC
4 elin yBDyByD
5 3 4 anbi12i xACyBDxAxCyByD
6 2 5 bitr4i xAyBxCyDxACyBD
7 6 opabbii xy|xAyBxCyD=xy|xACyBD
8 1 7 eqtri xy|xAyBxy|xCyD=xy|xACyBD
9 df-xp A×B=xy|xAyB
10 df-xp C×D=xy|xCyD
11 9 10 ineq12i A×BC×D=xy|xAyBxy|xCyD
12 df-xp AC×BD=xy|xACyBD
13 8 11 12 3eqtr4i A×BC×D=AC×BD