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

Theorem xpss1 5102
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 3516 . 2  |-  C  C_  C
2 xpss12 5099 . 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 3469    X. cxp 4990
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1596  ax-4 1607  ax-5 1675  ax-6 1714  ax-7 1734  ax-10 1781  ax-11 1786  ax-12 1798  ax-13 1961  ax-ext 2438
This theorem depends on definitions:  df-bi 185  df-or 370  df-an 371  df-tru 1377  df-ex 1592  df-nf 1595  df-sb 1707  df-clab 2446  df-cleq 2452  df-clel 2455  df-nfc 2610  df-in 3476  df-ss 3483  df-opab 4499  df-xp 4998
This theorem is referenced by:  ssres2  5291  funssxp  5735  tposssxp  6949  tpostpos2  6966  unxpwdom2  8003  dfac12lem2  8513  axdc3lem  8819  fpwwe2  9010  canthp1lem2  9020  pwfseqlem5  9030  wrdexg  12510  imasvscafn  14781  imasvscaf  14783  gasubg  16128  mamures  18652  mdetrlin  18864  mdetrsca  18865  mdetunilem9  18882  mdetmul  18885  tx1cn  19838  cxpcn3  22843  imadifxp  27117  1stmbfm  27857  sxbrsigalem0  27868  cvmlift2lem1  28373  cvmlift2lem9  28382
  Copyright terms: Public domain W3C validator