Theorem xpss1 5703

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 4012	. 2 ⊢ 𝐶 ⊆ 𝐶
2		xpss12 5699	. 2 ⊢ ((𝐴 ⊆ 𝐵 ∧ 𝐶 ⊆ 𝐶) → (𝐴 × 𝐶) ⊆ (𝐵 × 𝐶))
3	1, 2	mpan2 689	1 ⊢ (𝐴 ⊆ 𝐵 → (𝐴 × 𝐶) ⊆ (𝐵 × 𝐶))

Syntax hints:   → wi 4   ⊆ wss 3957   × cxp 5682

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1790  ax-4 1804  ax-5 1906  ax-6 1964  ax-7 2004  ax-8 2102  ax-9 2110  ax-ext 2700

This theorem depends on definitions:  df-bi 206  df-an 395  df-ex 1775  df-sb 2062  df-clab 2707  df-cleq 2721  df-clel 2806  df-ss 3974  df-opab 5217  df-xp 5690

This theorem is referenced by:  ssres2  6017  funssxp  6759  tposssxp  8251  tpostpos2  8268  unxpwdom2  9638  dfac12lem2  10195  unctb  10254  axdc3lem  10500  fpwwe2  10693  pwfseqlem5  10713  imasvscafn  17573  imasvscaf  17575  gasubg  19318  mamures  22411  mdetrlin  22618  mdetrsca  22619  mdetunilem9  22636  mdetmul  22639  tx1cn  23627  cxpcn3  26799  imadifxp  32547  1stmbfm  34132  sxbrsigalem0  34143  cvmlift2lem1  35168  cvmlift2lem9  35177  poimirlem32  37390  dfno2  43156  trclexi  43348  cnvtrcl0  43354  volicoff  45676  volicofmpt  45678  issmflem  46408