Theorem xpss1 5662

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

Syntax hints:   → wi 4   ⊆ wss 3902   × cxp 5641

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1814  ax-4 1828  ax-5 1929  ax-6 1986  ax-7 2027  ax-8 2143  ax-9 2151  ax-ext 2733

This theorem depends on definitions:  df-bi 209  df-an 400  df-ex 1799  df-sb 2090  df-clab 2740  df-cleq 2753  df-clel 2836  df-ss 3919  df-opab 5160  df-xp 5649

This theorem is referenced by:  ssres2  5986  funssxp  6715  tposssxp  8204  tpostpos2  8221  unxpwdom2  9530  dfac12lem2  10095  unctb  10154  axdc3lem  10401  fpwwe2  10595  pwfseqlem5  10615  imasvscafn  17558  imasvscaf  17560  gasubg  19333  mamures  22445  mdetrlin  22650  mdetrsca  22651  mdetunilem9  22668  mdetmul  22671  tx1cn  23657  cxpcn3  26801  imadifxp  32761  1stmbfm  34518  sxbrsigalem0  34529  cvmlift2lem1  35613  cvmlift2lem9  35622  poimirlem32  38112  dfno2  43965  trclexi  44157  cnvtrcl0  44163  volicoff  46530  volicofmpt  46532  issmflem  47262