![]() |
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 3964 | . 2 ⊢ 𝐶 ⊆ 𝐶 | |
2 | xpss12 5646 | . 2 ⊢ ((𝐴 ⊆ 𝐵 ∧ 𝐶 ⊆ 𝐶) → (𝐴 × 𝐶) ⊆ (𝐵 × 𝐶)) | |
3 | 1, 2 | mpan2 689 | 1 ⊢ (𝐴 ⊆ 𝐵 → (𝐴 × 𝐶) ⊆ (𝐵 × 𝐶)) |
Colors of variables: wff setvar class |
Syntax hints: → wi 4 ⊆ wss 3908 × cxp 5629 |
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 1913 ax-6 1971 ax-7 2011 ax-8 2108 ax-9 2116 ax-ext 2708 |
This theorem depends on definitions: df-bi 206 df-an 397 df-tru 1544 df-ex 1782 df-sb 2068 df-clab 2715 df-cleq 2729 df-clel 2815 df-v 3445 df-in 3915 df-ss 3925 df-opab 5166 df-xp 5637 |
This theorem is referenced by: ssres2 5963 funssxp 6694 tposssxp 8153 tpostpos2 8170 unxpwdom2 9482 dfac12lem2 10038 unctb 10099 axdc3lem 10344 fpwwe2 10537 pwfseqlem5 10557 imasvscafn 17379 imasvscaf 17381 gasubg 19041 mamures 21691 mdetrlin 21903 mdetrsca 21904 mdetunilem9 21921 mdetmul 21924 tx1cn 22912 cxpcn3 26053 imadifxp 31348 1stmbfm 32672 sxbrsigalem0 32683 cvmlift2lem1 33708 cvmlift2lem9 33717 poimirlem32 36048 dfno2 41611 trclexi 41803 cnvtrcl0 41809 volicoff 44137 volicofmpt 44139 issmflem 44869 |
Copyright terms: Public domain | W3C validator |