Metamath Proof Explorer < Previous   Next > Nearby theorems Mirrors  >  Home  >  MPE Home  >  Th. List  >  xpss1 Structured version   Visualization version   GIF version

Theorem xpss1 5539
 Description: Subset relation for Cartesian product. (Contributed by Jeff Hankins, 30-Aug-2009.)
Assertion
Ref Expression
xpss1 (𝐴𝐵 → (𝐴 × 𝐶) ⊆ (𝐵 × 𝐶))

Proof of Theorem xpss1
StepHypRef Expression
1 ssid 3937 . 2 𝐶𝐶
2 xpss12 5535 . 2 ((𝐴𝐵𝐶𝐶) → (𝐴 × 𝐶) ⊆ (𝐵 × 𝐶))
31, 2mpan2 690 1 (𝐴𝐵 → (𝐴 × 𝐶) ⊆ (𝐵 × 𝐶))
 Colors of variables: wff setvar class Syntax hints:   → wi 4   ⊆ wss 3881   × cxp 5518 This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1797  ax-4 1811  ax-5 1911  ax-6 1970  ax-7 2015  ax-8 2113  ax-9 2121  ax-ext 2770 This theorem depends on definitions:  df-bi 210  df-an 400  df-ex 1782  df-sb 2070  df-clab 2777  df-cleq 2791  df-clel 2870  df-v 3443  df-in 3888  df-ss 3898  df-opab 5094  df-xp 5526 This theorem is referenced by:  ssres2  5847  funssxp  6510  tposssxp  7882  tpostpos2  7899  unxpwdom2  9039  dfac12lem2  9558  unctb  9619  axdc3lem  9864  fpwwe2  10057  pwfseqlem5  10077  imasvscafn  16805  imasvscaf  16807  gasubg  18428  mamures  21007  mdetrlin  21217  mdetrsca  21218  mdetunilem9  21235  mdetmul  21238  tx1cn  22224  cxpcn3  25347  imadifxp  30374  1stmbfm  31643  sxbrsigalem0  31654  cvmlift2lem1  32677  cvmlift2lem9  32686  poimirlem32  35108  trclexi  40363  cnvtrcl0  40369  volicoff  42680  volicofmpt  42682  issmflem  43404
 Copyright terms: Public domain W3C validator