Theorem xpss2 5675

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 3935	. 2 ⊢ 𝐶 ⊆ 𝐶
2		xpss12 5670	. 2 ⊢ ((𝐶 ⊆ 𝐶 ∧ 𝐴 ⊆ 𝐵) → (𝐶 × 𝐴) ⊆ (𝐶 × 𝐵))
3	1, 2	mpan 703	1 ⊢ (𝐴 ⊆ 𝐵 → (𝐶 × 𝐴) ⊆ (𝐶 × 𝐵))

This proof depends on syntax axioms:   → wi 4   ⊆ wss 3900   × cxp 5653

This proof depends on axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1828  ax-4 1842  ax-5 1945  ax-6 2002  ax-7 2043  ax-8 2149  ax-9 2157  ax-ext 2735

This proof depends on definitions:  df-bi 210  df-an 402  df-ex 1813  df-sb 2102  df-clab 2742  df-cleq 2755  df-clel 2839  df-ss 3901  df-opab 5171  df-xp 5661

This theorem is used by:  xpdom3  9122  marypha1lem  9452  canthp1lem2  10765  axresscn  11260  imasvscafn  17738  imasvscaf  17740  gass  19545  gsum2d  20216  pzriprnglem4  21820  pzriprnglem10  21826  tx2cn  23959  txtube  23989  txcmplem1  23990  hausdiag  23994  xkoinjcn  24036  caussi  25648  dvfval  26247  issh2  31841  elrgspnsubrunlem2  33879  qtophaus  34538  2ndmbfm  34963  sxbrsigalem0  34973  cvmlift2lem9  36243  cvmlift2lem11  36245  filnetlem3  37346  bj-idres  38273  idresssidinxp  39438  trclexi  44812  cnvtrcl0  44818  ovolval5lem2  47868  ovnovollem1  47871  ovnovollem2  47872