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

Theorem xpss1 5101
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 3508 . 2  |-  C  C_  C
2 xpss12 5098 . 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 3461    X. cxp 4987
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1605  ax-4 1618  ax-5 1691  ax-6 1734  ax-7 1776  ax-10 1823  ax-11 1828  ax-12 1840  ax-13 1985  ax-ext 2421
This theorem depends on definitions:  df-bi 185  df-or 370  df-an 371  df-tru 1386  df-ex 1600  df-nf 1604  df-sb 1727  df-clab 2429  df-cleq 2435  df-clel 2438  df-nfc 2593  df-in 3468  df-ss 3475  df-opab 4496  df-xp 4995
This theorem is referenced by:  ssres2  5290  funssxp  5734  tposssxp  6961  tpostpos2  6978  unxpwdom2  8017  dfac12lem2  8527  axdc3lem  8833  fpwwe2  9024  canthp1lem2  9034  pwfseqlem5  9044  wrdexg  12536  imasvscafn  14811  imasvscaf  14813  gasubg  16214  mamures  18765  mdetrlin  18977  mdetrsca  18978  mdetunilem9  18995  mdetmul  18998  tx1cn  19983  cxpcn3  22994  imadifxp  27330  1stmbfm  28104  sxbrsigalem0  28115  cvmlift2lem1  28620  cvmlift2lem9  28629  xphe  37491
  Copyright terms: Public domain W3C validator