Theorem xpss2 5102

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 3508	. 2 |- C C_ C
2		xpss12 5098	. 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 3461   X. cxp 4987

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1605  ax-4 1618  ax-5 1691  ax-6 1734  ax-7 1776  ax-10 1823  ax-11 1828  ax-12 1840  ax-13 1985  ax-ext 2421

This theorem depends on definitions:  df-bi 185  df-or 370  df-an 371  df-tru 1386  df-ex 1600  df-nf 1604  df-sb 1727  df-clab 2429  df-cleq 2435  df-clel 2438  df-nfc 2593  df-in 3468  df-ss 3475  df-opab 4496  df-xp 4995

This theorem is referenced by:  xpdom3  7617  marypha1lem  7895  unctb  8588  axresscn  9528  imasvscafn  14811  imasvscaf  14813  xpsc0  14834  xpsc1  14835  gass  16213  gsum2d  16873  gsum2dOLD  16874  tx2cn  19984  txtube  20014  txcmplem1  20015  hausdiag  20019  xkoinjcn  20061  caussi  21609  dvfval  22174  issh2  25998  qtophaus  27712  2ndmbfm  28105  sxbrsigalem0  28115  cvmlift2lem9  28629  cvmlift2lem11  28631  filnetlem3  30173