Theorem xpss1 5607

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

Syntax hints:   → wi 4   ⊆ wss 3891   × cxp 5586

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1801  ax-4 1815  ax-5 1916  ax-6 1974  ax-7 2014  ax-8 2111  ax-9 2119  ax-ext 2710

This theorem depends on definitions:  df-bi 206  df-an 396  df-tru 1544  df-ex 1786  df-sb 2071  df-clab 2717  df-cleq 2731  df-clel 2817  df-v 3432  df-in 3898  df-ss 3908  df-opab 5141  df-xp 5594

This theorem is referenced by:  ssres2  5916  funssxp  6625  tposssxp  8030  tpostpos2  8047  unxpwdom2  9308  dfac12lem2  9884  unctb  9945  axdc3lem  10190  fpwwe2  10383  pwfseqlem5  10403  imasvscafn  17229  imasvscaf  17231  gasubg  18889  mamures  21520  mdetrlin  21732  mdetrsca  21733  mdetunilem9  21750  mdetmul  21753  tx1cn  22741  cxpcn3  25882  imadifxp  30919  1stmbfm  32206  sxbrsigalem0  32217  cvmlift2lem1  33243  cvmlift2lem9  33252  poimirlem32  35788  trclexi  41181  cnvtrcl0  41187  volicoff  43490  volicofmpt  43492  issmflem  44214