Theorem xpss2 4949

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 3437	. 2 |- C C_ C
2		xpss12 4945	. 2 |- ( ( C C_ C /\ A C_ B ) -> ( C X. A ) C_ ( C X. B ) )
3	1, 2	mpan 684	1 |- ( A C_ B -> ( C X. A ) C_ ( C X. B ) )

Syntax hints:   -> wi 4   C_ wss 3390   X. cxp 4837

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1677  ax-4 1690  ax-5 1766  ax-6 1813  ax-7 1859  ax-10 1932  ax-11 1937  ax-12 1950  ax-13 2104  ax-ext 2451

This theorem depends on definitions:  df-bi 190  df-or 377  df-an 378  df-tru 1455  df-ex 1672  df-nf 1676  df-sb 1806  df-clab 2458  df-cleq 2464  df-clel 2467  df-nfc 2601  df-in 3397  df-ss 3404  df-opab 4455  df-xp 4845

This theorem is referenced by:  xpdom3  7688  marypha1lem  7965  unctb  8653  axresscn  9590  imasvscafn  15521  imasvscaf  15523  xpsc0  15544  xpsc1  15545  gass  17033  gsum2d  17682  tx2cn  20702  txtube  20732  txcmplem1  20733  hausdiag  20737  xkoinjcn  20779  caussi  22345  dvfval  22931  issh2  26943  qtophaus  28737  2ndmbfm  29156  sxbrsigalem0  29166  cvmlift2lem9  30106  cvmlift2lem11  30108  filnetlem3  31107  trclexi  36298  cnvtrcl0  36304  ovolval5lem2  38593  ovnovollem1  38596  ovnovollem2  38597