Theorem xpss2 5105

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

Assertion

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

Proof of Theorem xpss2

Step	Hyp	Ref	Expression
1		ssid 3518	. 2 |- C C_ C
2		xpss12 5101	. 2 |- ( ( C C_ C /\ A C_ B ) -> ( C X. A ) C_ ( C X. B ) )
3	1, 2	mpan 670	1 |- ( A C_ B -> ( C X. A ) C_ ( C X. B ) )

Syntax hints:   -> wi 4   C_ wss 3471   X. cxp 4992

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1596  ax-4 1607  ax-5 1675  ax-6 1714  ax-7 1734  ax-10 1781  ax-11 1786  ax-12 1798  ax-13 1963  ax-ext 2440

This theorem depends on definitions:  df-bi 185  df-or 370  df-an 371  df-tru 1377  df-ex 1592  df-nf 1595  df-sb 1707  df-clab 2448  df-cleq 2454  df-clel 2457  df-nfc 2612  df-in 3478  df-ss 3485  df-opab 4501  df-xp 5000

This theorem is referenced by:  xpdom3  7607  marypha1lem  7884  unctb  8576  axresscn  9516  imasvscafn  14783  imasvscaf  14785  xpsc0  14806  xpsc1  14807  gass  16129  gsum2d  16785  gsum2dOLD  16786  tx2cn  19841  txtube  19871  txcmplem1  19872  hausdiag  19876  xkoinjcn  19918  caussi  21466  dvfval  22031  issh2  25790  qtophaus  27625  2ndmbfm  27860  sxbrsigalem0  27870  cvmlift2lem9  28384  cvmlift2lem11  28386  filnetlem3  29790