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

Theorem xpss1 5048
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
StepHypRef Expression
1 ssid 3475 . 2  |-  C  C_  C
2 xpss12 5045 . 2  |-  ( ( A  C_  B  /\  C  C_  C )  -> 
( A  X.  C
)  C_  ( B  X.  C ) )
31, 2mpan2 671 1  |-  ( A 
C_  B  ->  ( A  X.  C )  C_  ( B  X.  C
) )
Colors of variables: wff setvar class
Syntax hints:    -> wi 4    C_ wss 3428    X. cxp 4938
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1592  ax-4 1603  ax-5 1671  ax-6 1710  ax-7 1730  ax-10 1777  ax-11 1782  ax-12 1794  ax-13 1952  ax-ext 2430
This theorem depends on definitions:  df-bi 185  df-or 370  df-an 371  df-tru 1373  df-ex 1588  df-nf 1591  df-sb 1703  df-clab 2437  df-cleq 2443  df-clel 2446  df-nfc 2601  df-in 3435  df-ss 3442  df-opab 4451  df-xp 4946
This theorem is referenced by:  ssres2  5237  funssxp  5671  tposssxp  6851  tpostpos2  6868  unxpwdom2  7906  dfac12lem2  8416  axdc3lem  8722  fpwwe2  8913  canthp1lem2  8923  pwfseqlem5  8933  wrdexg  12348  imasvscafn  14579  imasvscaf  14581  gasubg  15924  mamures  18401  mdetrlin  18526  mdetrsca  18527  mdetunilem9  18544  mdetmul  18547  tx1cn  19300  cxpcn3  22304  imadifxp  26075  1stmbfm  26811  sxbrsigalem0  26822  cvmlift2lem1  27327  cvmlift2lem9  27336
  Copyright terms: Public domain W3C validator