Theorem xpss1 5674

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

This proof depends on syntax axioms:   → wi 4   ⊆ wss 3899   × cxp 5653

This proof depends on axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1828  ax-4 1842  ax-5 1943  ax-6 2000  ax-7 2041  ax-8 2147  ax-9 2155  ax-ext 2732

This proof depends on definitions:  df-bi 210  df-an 402  df-ex 1813  df-sb 2100  df-clab 2739  df-cleq 2752  df-clel 2835  df-ss 3916  df-opab 5168  df-xp 5661

This theorem is used by:  ssres2  5997  funssxp  6731  tposssxp  8228  tpostpos2  8245  unxpwdom2  9560  dfac12lem2  10147  unctb  10206  axdc3lem  10452  fpwwe2  10652  pwfseqlem5  10672  imasvscafn  17623  imasvscaf  17625  gasubg  19429  mamures  22619  mdetrlin  22824  mdetrsca  22825  mdetunilem9  22842  mdetmul  22845  tx1cn  23835  cxpcn3  26985  imadifxp  33074  1stmbfm  34771  sxbrsigalem0  34782  cvmlift2lem1  35881  cvmlift2lem9  35890  poimirlem32  38401  dfno2  44268  trclexi  44460  cnvtrcl0  44466  volicoff  46823  volicofmpt  46825  issmflem  47555