Theorem xpss2 5671

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

This proof depends on syntax axioms:   → wi 4   ⊆ wss 3899   × cxp 5649

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 1943  ax-6 2000  ax-7 2041  ax-8 2147  ax-9 2155  ax-ext 2733

This proof depends on definitions:  df-bi 210  df-an 402  df-ex 1813  df-sb 2100  df-clab 2740  df-cleq 2753  df-clel 2836  df-ss 3916  df-opab 5168  df-xp 5657

This theorem is used by:  xpdom3  9078  marypha1lem  9409  canthp1lem2  10719  axresscn  11214  imasvscafn  17689  imasvscaf  17691  gass  19495  gsum2d  20166  pzriprnglem4  21770  pzriprnglem10  21776  tx2cn  23909  txtube  23939  txcmplem1  23940  hausdiag  23944  xkoinjcn  23986  caussi  25598  dvfval  26197  issh2  31793  elrgspnsubrunlem2  33791  qtophaus  34450  2ndmbfm  34876  sxbrsigalem0  34886  cvmlift2lem9  36045  cvmlift2lem11  36047  filnetlem3  37138  bj-idres  38049  idresssidinxp  39214  trclexi  44579  cnvtrcl0  44585  ovolval5lem2  47607  ovnovollem1  47610  ovnovollem2  47611