Theorem xpss1 5682

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

This proof depends on syntax axioms:   → wi 4   ⊆ wss 3906   × cxp 5661

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 2148  ax-9 2156  ax-ext 2737

This proof depends on definitions:  df-bi 210  df-an 402  df-ex 1813  df-sb 2100  df-clab 2744  df-cleq 2757  df-clel 2840  df-ss 3923  df-opab 5176  df-xp 5669

This theorem is used by:  ssres2  6005  funssxp  6738  tposssxp  8228  tpostpos2  8245  unxpwdom2  9553  dfac12lem2  10140  unctb  10199  axdc3lem  10445  fpwwe2  10639  pwfseqlem5  10659  imasvscafn  17609  imasvscaf  17611  gasubg  19396  mamures  22584  mdetrlin  22789  mdetrsca  22790  mdetunilem9  22807  mdetmul  22810  tx1cn  23797  cxpcn3  26944  imadifxp  32993  1stmbfm  34691  sxbrsigalem0  34702  cvmlift2lem1  35807  cvmlift2lem9  35816  poimirlem32  38336  dfno2  44187  trclexi  44379  cnvtrcl0  44385  volicoff  46742  volicofmpt  46744  issmflem  47474