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 3988 | . 2 ⊢ 𝐶 ⊆ 𝐶 | |
2 | xpss12 5569 | . 2 ⊢ ((𝐴 ⊆ 𝐵 ∧ 𝐶 ⊆ 𝐶) → (𝐴 × 𝐶) ⊆ (𝐵 × 𝐶)) | |
3 | 1, 2 | mpan2 689 | 1 ⊢ (𝐴 ⊆ 𝐵 → (𝐴 × 𝐶) ⊆ (𝐵 × 𝐶)) |
Colors of variables: wff setvar class |
Syntax hints: → wi 4 ⊆ wss 3935 × cxp 5552 |
This theorem was proved from axioms: ax-mp 5 ax-1 6 ax-2 7 ax-3 8 ax-gen 1792 ax-4 1806 ax-5 1907 ax-6 1966 ax-7 2011 ax-8 2112 ax-9 2120 ax-10 2141 ax-11 2157 ax-12 2173 ax-ext 2793 |
This theorem depends on definitions: df-bi 209 df-an 399 df-or 844 df-tru 1536 df-ex 1777 df-nf 1781 df-sb 2066 df-clab 2800 df-cleq 2814 df-clel 2893 df-nfc 2963 df-in 3942 df-ss 3951 df-opab 5128 df-xp 5560 |
This theorem is referenced by: ssres2 5880 funssxp 6534 tposssxp 7895 tpostpos2 7912 unxpwdom2 9051 dfac12lem2 9569 unctb 9626 axdc3lem 9871 fpwwe2 10064 pwfseqlem5 10084 wrdexgOLD 13871 imasvscafn 16809 imasvscaf 16811 gasubg 18431 mamures 21000 mdetrlin 21210 mdetrsca 21211 mdetunilem9 21228 mdetmul 21231 tx1cn 22216 cxpcn3 25328 imadifxp 30350 1stmbfm 31518 sxbrsigalem0 31529 cvmlift2lem1 32549 cvmlift2lem9 32558 poimirlem32 34923 trclexi 39978 cnvtrcl0 39984 volicoff 42279 volicofmpt 42281 issmflem 43003 |
Copyright terms: Public domain | W3C validator |