Theorem xpss1 5637

Description: Subset relation for Cartesian product. (Contributed by Jeff Hankins, 30-Aug-2009.)

Assertion

Ref	Expression
xpss1	⊢ (𝐴 ⊆ 𝐵 → (𝐴 × 𝐶) ⊆ (𝐵 × 𝐶))

Proof of Theorem xpss1

Step	Hyp	Ref	Expression
1		ssid 3937	. 2 ⊢ 𝐶 ⊆ 𝐶
2		xpss12 5633	. 2 ⊢ ((𝐴 ⊆ 𝐵 ∧ 𝐶 ⊆ 𝐶) → (𝐴 × 𝐶) ⊆ (𝐵 × 𝐶))
3	1, 2	mpan2 697	1 ⊢ (𝐴 ⊆ 𝐵 → (𝐴 × 𝐶) ⊆ (𝐵 × 𝐶))

Syntax hints:   → wi 4   ⊆ wss 3883   × cxp 5616

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 2711

This theorem depends on definitions:  df-bi 208  df-an 397  df-ex 1787  df-sb 2074  df-clab 2718  df-cleq 2731  df-clel 2814  df-ss 3900  df-opab 5135  df-xp 5624

This theorem is referenced by:  ssres2  5956  funssxp  6683  tposssxp  8170  tpostpos2  8187  unxpwdom2  9493  dfac12lem2  10058  unctb  10117  axdc3lem  10363  fpwwe2  10557  pwfseqlem5  10577  imasvscafn  17492  imasvscaf  17494  gasubg  19268  mamures  22380  mdetrlin  22585  mdetrsca  22586  mdetunilem9  22603  mdetmul  22606  tx1cn  23592  cxpcn3  26730  imadifxp  32690  1stmbfm  34444  sxbrsigalem0  34455  cvmlift2lem1  35530  cvmlift2lem9  35539  poimirlem32  38019  dfno2  43872  trclexi  44064  cnvtrcl0  44070  volicoff  46438  volicofmpt  46440  issmflem  47170