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

Theorem xpss2 5152
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 3587 . 2 𝐶𝐶
2 xpss12 5148 . 2 ((𝐶𝐶𝐴𝐵) → (𝐶 × 𝐴) ⊆ (𝐶 × 𝐵))
31, 2mpan 702 1 (𝐴𝐵 → (𝐶 × 𝐴) ⊆ (𝐶 × 𝐵))
Colors of variables: wff setvar class
Syntax hints:  wi 4  wss 3540   × cxp 5036
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1713  ax-4 1728  ax-5 1827  ax-6 1875  ax-7 1922  ax-10 2006  ax-11 2021  ax-12 2034  ax-13 2234  ax-ext 2590
This theorem depends on definitions:  df-bi 196  df-or 384  df-an 385  df-tru 1478  df-ex 1696  df-nf 1701  df-sb 1868  df-clab 2597  df-cleq 2603  df-clel 2606  df-nfc 2740  df-in 3547  df-ss 3554  df-opab 4644  df-xp 5044
This theorem is referenced by:  xpdom3  7943  marypha1lem  8222  unctb  8910  axresscn  9848  imasvscafn  16020  imasvscaf  16022  xpsc0  16043  xpsc1  16044  gass  17557  gsum2d  18194  tx2cn  21223  txtube  21253  txcmplem1  21254  hausdiag  21258  xkoinjcn  21300  caussi  22903  dvfval  23467  issh2  27450  qtophaus  29231  2ndmbfm  29650  sxbrsigalem0  29660  cvmlift2lem9  30547  cvmlift2lem11  30549  filnetlem3  31545  trclexi  36946  cnvtrcl0  36952  ovolval5lem2  39543  ovnovollem1  39546  ovnovollem2  39547
  Copyright terms: Public domain W3C validator