Theorem xpss2 5285

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

Syntax hints:   → wi 4   ⊆ wss 3715   × cxp 5264

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1871  ax-4 1886  ax-5 1988  ax-6 2054  ax-7 2090  ax-9 2148  ax-10 2168  ax-11 2183  ax-12 2196  ax-13 2391  ax-ext 2740

This theorem depends on definitions:  df-bi 197  df-or 384  df-an 385  df-tru 1635  df-ex 1854  df-nf 1859  df-sb 2047  df-clab 2747  df-cleq 2753  df-clel 2756  df-nfc 2891  df-in 3722  df-ss 3729  df-opab 4865  df-xp 5272

This theorem is referenced by:  xpdom3  8223  marypha1lem  8504  unctb  9219  axresscn  10161  imasvscafn  16399  imasvscaf  16401  xpsc0  16422  xpsc1  16423  gass  17934  gsum2d  18571  tx2cn  21615  txtube  21645  txcmplem1  21646  hausdiag  21650  xkoinjcn  21692  caussi  23295  dvfval  23860  issh2  28375  qtophaus  30212  2ndmbfm  30632  sxbrsigalem0  30642  cvmlift2lem9  31600  cvmlift2lem11  31602  filnetlem3  32681  idresssidinxp  34403  trclexi  38429  cnvtrcl0  38435  ovolval5lem2  41373  ovnovollem1  41376  ovnovollem2  41377