Theorem xpss2 5645

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

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

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1802  ax-4 1816  ax-5 1917  ax-6 1974  ax-7 2015  ax-8 2121  ax-9 2129  ax-ext 2712

This theorem depends on definitions:  df-bi 208  df-an 397  df-ex 1787  df-sb 2074  df-clab 2719  df-cleq 2732  df-clel 2815  df-ss 3907  df-opab 5142  df-xp 5631

This theorem is referenced by:  xpdom3  9010  marypha1lem  9343  canthp1lem2  10574  axresscn  11069  imasvscafn  17499  imasvscaf  17501  gass  19274  gsum2d  19945  pzriprnglem4  21466  pzriprnglem10  21472  tx2cn  23600  txtube  23630  txcmplem1  23631  hausdiag  23635  xkoinjcn  23677  caussi  25289  dvfval  25889  issh2  31305  elrgspnsubrunlem2  33336  qtophaus  34027  2ndmbfm  34452  sxbrsigalem0  34462  cvmlift2lem9  35546  cvmlift2lem11  35548  filnetlem3  36615  bj-idres  37527  idresssidinxp  38688  trclexi  44071  cnvtrcl0  44077  ovolval5lem2  47103  ovnovollem1  47106  ovnovollem2  47107