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

Theorem xpss2 5705
Description: Subset relation for Cartesian product. (Contributed by Jeff Hankins, 30-Aug-2009.)
Assertion
Ref Expression
xpss2 (𝐴𝐵 → (𝐶 × 𝐴) ⊆ (𝐶 × 𝐵))

Proof of Theorem xpss2
StepHypRef Expression
1 ssid 4006 . 2 𝐶𝐶
2 xpss12 5700 . 2 ((𝐶𝐶𝐴𝐵) → (𝐶 × 𝐴) ⊆ (𝐶 × 𝐵))
31, 2mpan 690 1 (𝐴𝐵 → (𝐶 × 𝐴) ⊆ (𝐶 × 𝐵))
Colors of variables: wff setvar class
Syntax hints:  wi 4  wss 3951   × cxp 5683
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1795  ax-4 1809  ax-5 1910  ax-6 1967  ax-7 2007  ax-8 2110  ax-9 2118  ax-ext 2708
This theorem depends on definitions:  df-bi 207  df-an 396  df-ex 1780  df-sb 2065  df-clab 2715  df-cleq 2729  df-clel 2816  df-ss 3968  df-opab 5206  df-xp 5691
This theorem is referenced by:  xpdom3  9110  marypha1lem  9473  canthp1lem2  10693  axresscn  11188  imasvscafn  17582  imasvscaf  17584  gass  19319  gsum2d  19990  pzriprnglem4  21495  pzriprnglem10  21501  tx2cn  23618  txtube  23648  txcmplem1  23649  hausdiag  23653  xkoinjcn  23695  caussi  25331  dvfval  25932  issh2  31228  elrgspnsubrunlem2  33252  qtophaus  33835  2ndmbfm  34263  sxbrsigalem0  34273  cvmlift2lem9  35316  cvmlift2lem11  35318  filnetlem3  36381  bj-idres  37161  idresssidinxp  38309  trclexi  43633  cnvtrcl0  43639  ovolval5lem2  46668  ovnovollem1  46671  ovnovollem2  46672
  Copyright terms: Public domain W3C validator