Metamath Proof Explorer


Theorem xpss

Description: A Cartesian product is included in the ordered pair universe. Exercise 3 of TakeutiZaring p. 25. (Contributed by NM, 2-Aug-1994)

Ref Expression
Assertion xpss A×BV×V

Proof

Step Hyp Ref Expression
1 ssv AV
2 ssv BV
3 xpss12 AVBVA×BV×V
4 1 2 3 mp2an A×BV×V