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 X. B ) C_ ( _V X. _V )

Proof

Step Hyp Ref Expression
1 ssv 
 |-  A C_ _V
2 ssv 
 |-  B C_ _V
3 xpss12 
 |-  ( ( A C_ _V /\ B C_ _V ) -> ( A X. B ) C_ ( _V X. _V ) )
4 1 2 3 mp2an 
 |-  ( A X. B ) C_ ( _V X. _V )