Metamath Proof Explorer

Theorem xpss1

Description: Subset relation for Cartesian product. (Contributed by Jeff Hankins, 30-Aug-2009)

Ref Expression
Assertion xpss1 
|- ( A C_ B -> ( A X. C ) C_ ( B X. C ) )

Proof

Step Hyp Ref Expression
1 ssid 
 |-  C C_ C
2 xpss12 
 |-  ( ( A C_ B /\ C C_ C ) -> ( A X. C ) C_ ( B X. C ) )
3 1 2 mpan2 
 |-  ( A C_ B -> ( A X. C ) C_ ( B X. C ) )