Theorem xpss1 5669

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

This proof depends on syntax axioms:   → wi 4   ⊆ wss 3896   × cxp 5648

This proof depends on axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1827  ax-4 1841  ax-5 1942  ax-6 1999  ax-7 2040  ax-8 2146  ax-9 2154  ax-ext 2732

This proof depends on definitions:  df-bi 210  df-an 402  df-ex 1812  df-sb 2099  df-clab 2739  df-cleq 2752  df-clel 2835  df-ss 3897  df-opab 5167  df-xp 5656

This theorem is used by:  ssres2  5995  funssxp  6741  tposssxp  8252  tpostpos2  8269  unxpwdom2  9587  dfac12lem2  10228  unctb  10287  axdc3lem  10533  fpwwe2  10733  pwfseqlem5  10753  imasvscafn  17716  imasvscaf  17718  gasubg  19523  mamures  22719  mdetrlin  22924  mdetrsca  22925  mdetunilem9  22942  mdetmul  22945  tx1cn  23935  cxpcn3  27083  imadifxp  33244  1stmbfm  34940  sxbrsigalem0  34951  cvmlift2lem1  36155  cvmlift2lem9  36164  poimirlem32  38677  dfno2  44536  trclexi  44727  cnvtrcl0  44733  volicoff  47112  volicofmpt  47114  issmflem  47844