Theorem xpss1 5538

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

Syntax hints:   → wi 4   ⊆ wss 3881   × cxp 5517

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1797  ax-4 1811  ax-5 1911  ax-6 1970  ax-7 2015  ax-8 2113  ax-9 2121  ax-ext 2770

This theorem depends on definitions:  df-bi 210  df-an 400  df-ex 1782  df-sb 2070  df-clab 2777  df-cleq 2791  df-clel 2870  df-v 3443  df-in 3888  df-ss 3898  df-opab 5093  df-xp 5525

This theorem is referenced by:  ssres2  5846  funssxp  6509  tposssxp  7879  tpostpos2  7896  unxpwdom2  9036  dfac12lem2  9555  unctb  9616  axdc3lem  9861  fpwwe2  10054  pwfseqlem5  10074  imasvscafn  16802  imasvscaf  16804  gasubg  18424  mamures  20997  mdetrlin  21207  mdetrsca  21208  mdetunilem9  21225  mdetmul  21228  tx1cn  22214  cxpcn3  25337  imadifxp  30364  1stmbfm  31628  sxbrsigalem0  31639  cvmlift2lem1  32662  cvmlift2lem9  32671  poimirlem32  35089  trclexi  40320  cnvtrcl0  40326  volicoff  42637  volicofmpt  42639  issmflem  43361