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 
|- ( ( A e. V /\ B e. W ) -> ( A X. B ) ~~ ( B X. A ) )

Proof

Step Hyp Ref Expression
1 xpeq1 
 |-  ( x = A -> ( x X. y ) = ( A X. y ) )
2 xpeq2 
 |-  ( x = A -> ( y X. x ) = ( y X. A ) )
3 1 2 breq12d 
 |-  ( x = A -> ( ( x X. y ) ~~ ( y X. x ) <-> ( A X. y ) ~~ ( y X. A ) ) )
4 xpeq2 
 |-  ( y = B -> ( A X. y ) = ( A X. B ) )
5 xpeq1 
 |-  ( y = B -> ( y X. A ) = ( B X. A ) )
6 4 5 breq12d 
 |-  ( y = B -> ( ( A X. y ) ~~ ( y X. A ) <-> ( A X. B ) ~~ ( B X. A ) ) )
7 vex 
 |-  x e. _V
8 vex 
 |-  y e. _V
9 7 8 xpcomen 
 |-  ( x X. y ) ~~ ( y X. x )
10 3 6 9 vtocl2g 
 |-  ( ( A e. V /\ B e. W ) -> ( A X. B ) ~~ ( B X. A ) )