Theorem xpss2 5644

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

Syntax hints:   → wi 4   ⊆ wss 3890   × cxp 5622

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1797  ax-4 1811  ax-5 1912  ax-6 1969  ax-7 2010  ax-8 2116  ax-9 2124  ax-ext 2709

This theorem depends on definitions:  df-bi 207  df-an 396  df-ex 1782  df-sb 2069  df-clab 2716  df-cleq 2729  df-clel 2812  df-ss 3907  df-opab 5149  df-xp 5630

This theorem is referenced by:  xpdom3  9006  marypha1lem  9339  canthp1lem2  10567  axresscn  11062  imasvscafn  17492  imasvscaf  17494  gass  19267  gsum2d  19938  pzriprnglem4  21474  pzriprnglem10  21480  tx2cn  23585  txtube  23615  txcmplem1  23616  hausdiag  23620  xkoinjcn  23662  caussi  25274  dvfval  25874  issh2  31295  elrgspnsubrunlem2  33324  qtophaus  33996  2ndmbfm  34421  sxbrsigalem0  34431  cvmlift2lem9  35509  cvmlift2lem11  35511  filnetlem3  36578  bj-idres  37490  idresssidinxp  38649  trclexi  44065  cnvtrcl0  44071  ovolval5lem2  47099  ovnovollem1  47102  ovnovollem2  47103