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 3923 | . 2 ⊢ 𝐶 ⊆ 𝐶 | |
2 | xpss12 5566 | . 2 ⊢ ((𝐴 ⊆ 𝐵 ∧ 𝐶 ⊆ 𝐶) → (𝐴 × 𝐶) ⊆ (𝐵 × 𝐶)) | |
3 | 1, 2 | mpan2 691 | 1 ⊢ (𝐴 ⊆ 𝐵 → (𝐴 × 𝐶) ⊆ (𝐵 × 𝐶)) |
Colors of variables: wff setvar class |
Syntax hints: → wi 4 ⊆ wss 3866 × cxp 5549 |
This theorem was proved from axioms: ax-mp 5 ax-1 6 ax-2 7 ax-3 8 ax-gen 1803 ax-4 1817 ax-5 1918 ax-6 1976 ax-7 2016 ax-8 2112 ax-9 2120 ax-ext 2708 |
This theorem depends on definitions: df-bi 210 df-an 400 df-tru 1546 df-ex 1788 df-sb 2071 df-clab 2715 df-cleq 2729 df-clel 2816 df-v 3410 df-in 3873 df-ss 3883 df-opab 5116 df-xp 5557 |
This theorem is referenced by: ssres2 5879 funssxp 6574 tposssxp 7972 tpostpos2 7989 unxpwdom2 9204 dfac12lem2 9758 unctb 9819 axdc3lem 10064 fpwwe2 10257 pwfseqlem5 10277 imasvscafn 17042 imasvscaf 17044 gasubg 18696 mamures 21289 mdetrlin 21499 mdetrsca 21500 mdetunilem9 21517 mdetmul 21520 tx1cn 22506 cxpcn3 25634 imadifxp 30659 1stmbfm 31939 sxbrsigalem0 31950 cvmlift2lem1 32977 cvmlift2lem9 32986 poimirlem32 35546 trclexi 40904 cnvtrcl0 40910 volicoff 43211 volicofmpt 43213 issmflem 43935 |
Copyright terms: Public domain | W3C validator |