MPE Home Metamath Proof Explorer < Previous   Next >
Nearby theorems
Mirrors  >  Home  >  MPE Home  >  Th. List  >  xpss2 Structured version   Unicode version

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
StepHypRef 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 ) )
31, 2mpan 670 1  |-  ( A 
C_  B  ->  ( C  X.  A )  C_  ( C  X.  B
) )
Colors of variables: wff setvar class
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
  Copyright terms: Public domain W3C validator