|   | Metamath Proof Explorer | < Previous  
      Next > Nearby theorems | |
| Mirrors > Home > MPE Home > Th. List > xpss1 | Structured version Visualization version GIF version | ||
| Description: Subset relation for Cartesian product. (Contributed by Jeff Hankins, 30-Aug-2009.) | 
| Ref | Expression | 
|---|---|
| xpss1 | ⊢ (𝐴 ⊆ 𝐵 → (𝐴 × 𝐶) ⊆ (𝐵 × 𝐶)) | 
| Step | Hyp | Ref | Expression | 
|---|---|---|---|
| 1 | ssid 4005 | . 2 ⊢ 𝐶 ⊆ 𝐶 | |
| 2 | xpss12 5699 | . 2 ⊢ ((𝐴 ⊆ 𝐵 ∧ 𝐶 ⊆ 𝐶) → (𝐴 × 𝐶) ⊆ (𝐵 × 𝐶)) | |
| 3 | 1, 2 | mpan2 691 | 1 ⊢ (𝐴 ⊆ 𝐵 → (𝐴 × 𝐶) ⊆ (𝐵 × 𝐶)) | 
| Colors of variables: wff setvar class | 
| Syntax hints: → wi 4 ⊆ wss 3950 × cxp 5682 | 
| This theorem was proved from axioms: ax-mp 5 ax-1 6 ax-2 7 ax-3 8 ax-gen 1794 ax-4 1808 ax-5 1909 ax-6 1966 ax-7 2006 ax-8 2109 ax-9 2117 ax-ext 2707 | 
| This theorem depends on definitions: df-bi 207 df-an 396 df-ex 1779 df-sb 2064 df-clab 2714 df-cleq 2728 df-clel 2815 df-ss 3967 df-opab 5205 df-xp 5690 | 
| This theorem is referenced by: ssres2 6021 funssxp 6763 tposssxp 8256 tpostpos2 8273 unxpwdom2 9629 dfac12lem2 10186 unctb 10245 axdc3lem 10491 fpwwe2 10684 pwfseqlem5 10704 imasvscafn 17583 imasvscaf 17585 gasubg 19321 mamures 22402 mdetrlin 22609 mdetrsca 22610 mdetunilem9 22627 mdetmul 22630 tx1cn 23618 cxpcn3 26792 imadifxp 32615 1stmbfm 34263 sxbrsigalem0 34274 cvmlift2lem1 35308 cvmlift2lem9 35317 poimirlem32 37660 dfno2 43446 trclexi 43638 cnvtrcl0 43644 volicoff 46015 volicofmpt 46017 issmflem 46747 | 
| Copyright terms: Public domain | W3C validator |