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×BC×D=AC×BD

Proof

Step Hyp Ref Expression
1 relinxp RelA×BC×D
2 relxp RelAC×BD
3 an4 xAyBxCyDxAxCyByD
4 opelxp xyA×BxAyB
5 opelxp xyC×DxCyD
6 4 5 anbi12i xyA×BxyC×DxAyBxCyD
7 elin xACxAxC
8 elin yBDyByD
9 7 8 anbi12i xACyBDxAxCyByD
10 3 6 9 3bitr4i xyA×BxyC×DxACyBD
11 elin xyA×BC×DxyA×BxyC×D
12 opelxp xyAC×BDxACyBD
13 10 11 12 3bitr4i xyA×BC×DxyAC×BD
14 1 2 13 eqrelriiv A×BC×D=AC×BD