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

Theorem xpss2 5573
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 3992 . 2 𝐶𝐶
2 xpss12 5568 . 2 ((𝐶𝐶𝐴𝐵) → (𝐶 × 𝐴) ⊆ (𝐶 × 𝐵))
31, 2mpan 686 1 (𝐴𝐵 → (𝐶 × 𝐴) ⊆ (𝐶 × 𝐵))
Colors of variables: wff setvar class
Syntax hints:  wi 4  wss 3939   × cxp 5551
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1789  ax-4 1803  ax-5 1904  ax-6 1963  ax-7 2008  ax-8 2109  ax-9 2117  ax-10 2138  ax-11 2153  ax-12 2169  ax-ext 2797
This theorem depends on definitions:  df-bi 208  df-an 397  df-or 844  df-tru 1533  df-ex 1774  df-nf 1778  df-sb 2063  df-clab 2804  df-cleq 2818  df-clel 2897  df-nfc 2967  df-in 3946  df-ss 3955  df-opab 5125  df-xp 5559
This theorem is referenced by:  xpdom3  8607  marypha1lem  8889  canthp1lem2  10067  axresscn  10562  imasvscafn  16802  imasvscaf  16804  gass  18363  gsum2d  19014  tx2cn  22134  txtube  22164  txcmplem1  22165  hausdiag  22169  xkoinjcn  22211  caussi  23815  dvfval  24410  issh2  28900  qtophaus  30986  2ndmbfm  31405  sxbrsigalem0  31415  cvmlift2lem9  32442  cvmlift2lem11  32444  filnetlem3  33612  bj-idres  34331  idresssidinxp  35434  trclexi  39841  cnvtrcl0  39847  ovolval5lem2  42797  ovnovollem1  42800  ovnovollem2  42801
  Copyright terms: Public domain W3C validator