Theorem xpss1 5228

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

Assertion

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

Proof of Theorem xpss1

Step	Hyp	Ref	Expression
1		ssid 3624	. 2 |- C C_ C
2		xpss12 5225	. 2 |- ( ( A C_ B /\ C C_ C ) -> ( A X. C ) C_ ( B X. C ) )
3	1, 2	mpan2 707	1 |- ( A C_ B -> ( A X. C ) C_ ( B X. C ) )

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:  ssres2  5425  funssxp  6061  tposssxp  7356  tpostpos2  7373  unxpwdom2  8493  dfac12lem2  8966  axdc3lem  9272  fpwwe2  9465  canthp1lem2  9475  pwfseqlem5  9485  wrdexg  13315  imasvscafn  16197  imasvscaf  16199  gasubg  17735  mamures  20196  mdetrlin  20408  mdetrsca  20409  mdetunilem9  20426  mdetmul  20429  tx1cn  21412  cxpcn3  24489  imadifxp  29414  1stmbfm  30322  sxbrsigalem0  30333  cvmlift2lem1  31284  cvmlift2lem9  31293  poimirlem32  33441  trclexi  37927  cnvtrcl0  37933  volicoff  40212  volicofmpt  40214  issmflem  40936