Theorem xpss2 5670

Description: Subset relation for Cartesian product. (Contributed by Jeff Hankins, 30-Aug-2009.)

Assertion

Ref	Expression
xpss2	⊢ (𝐴 ⊆ 𝐵 → (𝐶 × 𝐴) ⊆ (𝐶 × 𝐵))

Proof of Theorem xpss2

Step	Hyp	Ref	Expression
1		ssid 3930	. 2 ⊢ 𝐶 ⊆ 𝐶
2		xpss12 5665	. 2 ⊢ ((𝐶 ⊆ 𝐶 ∧ 𝐴 ⊆ 𝐵) → (𝐶 × 𝐴) ⊆ (𝐶 × 𝐵))
3	1, 2	mpan 703	1 ⊢ (𝐴 ⊆ 𝐵 → (𝐶 × 𝐴) ⊆ (𝐶 × 𝐵))

This proof depends on syntax axioms:   → wi 4   ⊆ wss 3895   × cxp 5648

This proof depends on axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1827  ax-4 1841  ax-5 1942  ax-6 1999  ax-7 2040  ax-8 2146  ax-9 2154  ax-ext 2732

This proof depends on definitions:  df-bi 210  df-an 402  df-ex 1812  df-sb 2099  df-clab 2739  df-cleq 2752  df-clel 2835  df-ss 3896  df-opab 5167  df-xp 5656

This theorem is used by:  xpdom3  9097  marypha1lem  9428  canthp1lem2  10741  axresscn  11236  imasvscafn  17714  imasvscaf  17716  gass  19520  gsum2d  20191  pzriprnglem4  21795  pzriprnglem10  21801  tx2cn  23934  txtube  23964  txcmplem1  23965  hausdiag  23969  xkoinjcn  24011  caussi  25623  dvfval  26222  issh2  31816  elrgspnsubrunlem2  33855  qtophaus  34514  2ndmbfm  34939  sxbrsigalem0  34949  cvmlift2lem9  36162  cvmlift2lem11  36164  filnetlem3  37260  bj-idres  38174  idresssidinxp  39339  trclexi  44713  cnvtrcl0  44719  ovolval5lem2  47756  ovnovollem1  47759  ovnovollem2  47760