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

Theorem xpss2 5568
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 3986 . 2 𝐶𝐶
2 xpss12 5563 . 2 ((𝐶𝐶𝐴𝐵) → (𝐶 × 𝐴) ⊆ (𝐶 × 𝐵))
31, 2mpan 686 1 (𝐴𝐵 → (𝐶 × 𝐴) ⊆ (𝐶 × 𝐵))
Colors of variables: wff setvar class
Syntax hints:  wi 4  wss 3933   × cxp 5546
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1787  ax-4 1801  ax-5 1902  ax-6 1961  ax-7 2006  ax-8 2107  ax-9 2115  ax-10 2136  ax-11 2151  ax-12 2167  ax-ext 2790
This theorem depends on definitions:  df-bi 208  df-an 397  df-or 842  df-tru 1531  df-ex 1772  df-nf 1776  df-sb 2061  df-clab 2797  df-cleq 2811  df-clel 2890  df-nfc 2960  df-in 3940  df-ss 3949  df-opab 5120  df-xp 5554
This theorem is referenced by:  xpdom3  8603  marypha1lem  8885  canthp1lem2  10063  axresscn  10558  imasvscafn  16798  imasvscaf  16800  gass  18369  gsum2d  19021  tx2cn  22146  txtube  22176  txcmplem1  22177  hausdiag  22181  xkoinjcn  22223  caussi  23827  dvfval  24422  issh2  28913  qtophaus  30999  2ndmbfm  31418  sxbrsigalem0  31428  cvmlift2lem9  32455  cvmlift2lem11  32457  filnetlem3  33625  bj-idres  34344  idresssidinxp  35447  trclexi  39858  cnvtrcl0  39864  ovolval5lem2  42812  ovnovollem1  42815  ovnovollem2  42816
  Copyright terms: Public domain W3C validator