Theorem xpss2 5708

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

Syntax hints:   → wi 4   ⊆ wss 3962   × cxp 5686

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1791  ax-4 1805  ax-5 1907  ax-6 1964  ax-7 2004  ax-8 2107  ax-9 2115  ax-ext 2705

This theorem depends on definitions:  df-bi 207  df-an 396  df-ex 1776  df-sb 2062  df-clab 2712  df-cleq 2726  df-clel 2813  df-ss 3979  df-opab 5210  df-xp 5694

This theorem is referenced by:  xpdom3  9108  marypha1lem  9470  canthp1lem2  10690  axresscn  11185  imasvscafn  17583  imasvscaf  17585  gass  19331  gsum2d  20004  pzriprnglem4  21512  pzriprnglem10  21518  tx2cn  23633  txtube  23663  txcmplem1  23664  hausdiag  23668  xkoinjcn  23710  caussi  25344  dvfval  25946  issh2  31237  qtophaus  33796  2ndmbfm  34242  sxbrsigalem0  34252  cvmlift2lem9  35295  cvmlift2lem11  35297  filnetlem3  36362  bj-idres  37142  idresssidinxp  38289  trclexi  43609  cnvtrcl0  43615  ovolval5lem2  46608  ovnovollem1  46611  ovnovollem2  46612