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

Theorem xpss2 5332
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 3819 . 2 𝐶𝐶
2 xpss12 5327 . 2 ((𝐶𝐶𝐴𝐵) → (𝐶 × 𝐴) ⊆ (𝐶 × 𝐵))
31, 2mpan 682 1 (𝐴𝐵 → (𝐶 × 𝐴) ⊆ (𝐶 × 𝐵))
Colors of variables: wff setvar class
Syntax hints:  wi 4  wss 3769   × cxp 5310
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1891  ax-4 1905  ax-5 2006  ax-6 2072  ax-7 2107  ax-9 2166  ax-10 2185  ax-11 2200  ax-12 2213  ax-13 2377  ax-ext 2777
This theorem depends on definitions:  df-bi 199  df-an 386  df-or 875  df-tru 1657  df-ex 1876  df-nf 1880  df-sb 2065  df-clab 2786  df-cleq 2792  df-clel 2795  df-nfc 2930  df-in 3776  df-ss 3783  df-opab 4906  df-xp 5318
This theorem is referenced by:  xpdom3  8300  marypha1lem  8581  unctb  9315  axresscn  10257  imasvscafn  16512  imasvscaf  16514  xpsc0  16535  xpsc1  16536  gass  18046  gsum2d  18686  tx2cn  21742  txtube  21772  txcmplem1  21773  hausdiag  21777  xkoinjcn  21819  caussi  23423  dvfval  24002  issh2  28591  qtophaus  30419  2ndmbfm  30839  sxbrsigalem0  30849  cvmlift2lem9  31810  cvmlift2lem11  31812  filnetlem3  32887  idresssidinxp  34574  trclexi  38710  cnvtrcl0  38716  ovolval5lem2  41613  ovnovollem1  41616  ovnovollem2  41617
  Copyright terms: Public domain W3C validator