Theorem xpss2 4948

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 3374	. 2 |- C C_ C
2		xpss12 4944	. 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 3327   X. cxp 4837

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1591  ax-4 1602  ax-5 1670  ax-6 1708  ax-7 1728  ax-10 1775  ax-11 1780  ax-12 1792  ax-13 1943  ax-ext 2423

This theorem depends on definitions:  df-bi 185  df-or 370  df-an 371  df-ex 1587  df-nf 1590  df-sb 1701  df-clab 2429  df-cleq 2435  df-clel 2438  df-nfc 2567  df-in 3334  df-ss 3341  df-opab 4350  df-xp 4845

This theorem is referenced by:  xpdom3  7408  marypha1lem  7682  unctb  8373  axresscn  9314  imasvscafn  14474  imasvscaf  14476  xpsc0  14497  xpsc1  14498  gass  15818  gsum2d  16462  gsum2dOLD  16463  tx2cn  19182  txtube  19212  txcmplem1  19213  hausdiag  19217  xkoinjcn  19259  caussi  20807  dvfval  21371  issh2  24610  2ndmbfm  26675  sxbrsigalem0  26685  cvmlift2lem9  27199  cvmlift2lem11  27201  filnetlem3  28599