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

Theorem xpss2 5136
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 3581 . 2 𝐶𝐶
2 xpss12 5132 . 2 ((𝐶𝐶𝐴𝐵) → (𝐶 × 𝐴) ⊆ (𝐶 × 𝐵))
31, 2mpan 701 1 (𝐴𝐵 → (𝐶 × 𝐴) ⊆ (𝐶 × 𝐵))
Colors of variables: wff setvar class
Syntax hints:  wi 4  wss 3534   × cxp 5021
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1711  ax-4 1726  ax-5 1825  ax-6 1873  ax-7 1920  ax-10 2004  ax-11 2019  ax-12 2031  ax-13 2227  ax-ext 2584
This theorem depends on definitions:  df-bi 195  df-or 383  df-an 384  df-tru 1477  df-ex 1695  df-nf 1700  df-sb 1866  df-clab 2591  df-cleq 2597  df-clel 2600  df-nfc 2734  df-in 3541  df-ss 3548  df-opab 4633  df-xp 5029
This theorem is referenced by:  xpdom3  7915  marypha1lem  8194  unctb  8882  axresscn  9820  imasvscafn  15961  imasvscaf  15963  xpsc0  15984  xpsc1  15985  gass  17498  gsum2d  18135  tx2cn  21160  txtube  21190  txcmplem1  21191  hausdiag  21195  xkoinjcn  21237  caussi  22816  dvfval  23379  issh2  27251  qtophaus  29032  2ndmbfm  29451  sxbrsigalem0  29461  cvmlift2lem9  30348  cvmlift2lem11  30350  filnetlem3  31346  trclexi  36744  cnvtrcl0  36750  ovolval5lem2  39342  ovnovollem1  39345  ovnovollem2  39346
  Copyright terms: Public domain W3C validator