Theorem xpss2 5672

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

Syntax hints:   → wi 4   ⊆ wss 3907   × cxp 5650

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1818  ax-4 1832  ax-5 1933  ax-6 1990  ax-7 2031  ax-8 2147  ax-9 2155  ax-ext 2737

This theorem depends on definitions:  df-bi 210  df-an 401  df-ex 1803  df-sb 2094  df-clab 2744  df-cleq 2757  df-clel 2840  df-ss 3924  df-opab 5168  df-xp 5658

This theorem is referenced by:  xpdom3  9051  marypha1lem  9381  canthp1lem2  10626  axresscn  11121  imasvscafn  17581  imasvscaf  17583  gass  19362  gsum2d  20033  pzriprnglem4  21594  pzriprnglem10  21600  tx2cn  23728  txtube  23758  txcmplem1  23759  hausdiag  23763  xkoinjcn  23805  caussi  25417  dvfval  26017  issh2  31470  elrgspnsubrunlem2  33481  qtophaus  34143  2ndmbfm  34568  sxbrsigalem0  34578  cvmlift2lem9  35674  cvmlift2lem11  35676  filnetlem3  36753  bj-idres  37664  idresssidinxp  38825  trclexi  44208  cnvtrcl0  44214  ovolval5lem2  47225  ovnovollem1  47228  ovnovollem2  47229