Theorem xpss2 5229

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

Syntax hints:   -> wi 4   C_ wss 3574   X. cxp 5112

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1722  ax-4 1737  ax-5 1839  ax-6 1888  ax-7 1935  ax-9 1999  ax-10 2019  ax-11 2034  ax-12 2047  ax-13 2246  ax-ext 2602

This theorem depends on definitions:  df-bi 197  df-or 385  df-an 386  df-tru 1486  df-ex 1705  df-nf 1710  df-sb 1881  df-clab 2609  df-cleq 2615  df-clel 2618  df-nfc 2753  df-in 3581  df-ss 3588  df-opab 4713  df-xp 5120

This theorem is referenced by:  xpdom3  8058  marypha1lem  8339  unctb  9027  axresscn  9969  imasvscafn  16197  imasvscaf  16199  xpsc0  16220  xpsc1  16221  gass  17734  gsum2d  18371  tx2cn  21413  txtube  21443  txcmplem1  21444  hausdiag  21448  xkoinjcn  21490  caussi  23095  dvfval  23661  issh2  28066  qtophaus  29903  2ndmbfm  30323  sxbrsigalem0  30333  cvmlift2lem9  31293  cvmlift2lem11  31295  filnetlem3  32375  idresssidinxp  34079  trclexi  37927  cnvtrcl0  37933  ovolval5lem2  40867  ovnovollem1  40870  ovnovollem2  40871