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

Theorem xpss2 5285
 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 3765 . 2 𝐶𝐶
2 xpss12 5281 . 2 ((𝐶𝐶𝐴𝐵) → (𝐶 × 𝐴) ⊆ (𝐶 × 𝐵))
31, 2mpan 708 1 (𝐴𝐵 → (𝐶 × 𝐴) ⊆ (𝐶 × 𝐵))
 Colors of variables: wff setvar class Syntax hints:   → wi 4   ⊆ wss 3715   × cxp 5264 This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1871  ax-4 1886  ax-5 1988  ax-6 2054  ax-7 2090  ax-9 2148  ax-10 2168  ax-11 2183  ax-12 2196  ax-13 2391  ax-ext 2740 This theorem depends on definitions:  df-bi 197  df-or 384  df-an 385  df-tru 1635  df-ex 1854  df-nf 1859  df-sb 2047  df-clab 2747  df-cleq 2753  df-clel 2756  df-nfc 2891  df-in 3722  df-ss 3729  df-opab 4865  df-xp 5272 This theorem is referenced by:  xpdom3  8223  marypha1lem  8504  unctb  9219  axresscn  10161  imasvscafn  16399  imasvscaf  16401  xpsc0  16422  xpsc1  16423  gass  17934  gsum2d  18571  tx2cn  21615  txtube  21645  txcmplem1  21646  hausdiag  21650  xkoinjcn  21692  caussi  23295  dvfval  23860  issh2  28375  qtophaus  30212  2ndmbfm  30632  sxbrsigalem0  30642  cvmlift2lem9  31600  cvmlift2lem11  31602  filnetlem3  32681  idresssidinxp  34403  trclexi  38429  cnvtrcl0  38435  ovolval5lem2  41373  ovnovollem1  41376  ovnovollem2  41377
 Copyright terms: Public domain W3C validator