Metamath Proof Explorer


Theorem xpsneng

Description: A set is equinumerous to its Cartesian product with a singleton. Proposition 4.22(c) of Mendelson p. 254. (Contributed by NM, 22-Oct-2004)

Ref Expression
Assertion xpsneng AVBWA×BA

Proof

Step Hyp Ref Expression
1 xpeq1 x=Ax×y=A×y
2 id x=Ax=A
3 1 2 breq12d x=Ax×yxA×yA
4 sneq y=By=B
5 4 xpeq2d y=BA×y=A×B
6 5 breq1d y=BA×yAA×BA
7 vex xV
8 vex yV
9 7 8 xpsnen x×yx
10 3 6 9 vtocl2g AVBWA×BA