Metamath Proof Explorer


Theorem xpexg

Description: The Cartesian product of two sets is a set. Proposition 6.2 of TakeutiZaring p. 23. See also xpexgALT . (Contributed by NM, 14-Aug-1994)

Ref Expression
Assertion xpexg AVBWA×BV

Proof

Step Hyp Ref Expression
1 xpsspw A×B𝒫𝒫AB
2 unexg AVBWABV
3 pwexg ABV𝒫ABV
4 pwexg 𝒫ABV𝒫𝒫ABV
5 2 3 4 3syl AVBW𝒫𝒫ABV
6 ssexg A×B𝒫𝒫AB𝒫𝒫ABVA×BV
7 1 5 6 sylancr AVBWA×BV