Metamath Proof Explorer


Theorem xpcomeng

Description: Commutative law for equinumerosity of Cartesian product. Proposition 4.22(d) of Mendelson p. 254. (Contributed by NM, 27-Mar-2006)

Ref Expression
Assertion xpcomeng AVBWA×BB×A

Proof

Step Hyp Ref Expression
1 xpeq1 x=Ax×y=A×y
2 xpeq2 x=Ay×x=y×A
3 1 2 breq12d x=Ax×yy×xA×yy×A
4 xpeq2 y=BA×y=A×B
5 xpeq1 y=By×A=B×A
6 4 5 breq12d y=BA×yy×AA×BB×A
7 vex xV
8 vex yV
9 7 8 xpcomen x×yy×x
10 3 6 9 vtocl2g AVBWA×BB×A