Metamath Proof Explorer |
< Previous
Next >
Nearby theorems |
||
Mirrors > Home > MPE Home > Th. List > xpss2 | Structured version Visualization version GIF version |
Description: Subset relation for Cartesian product. (Contributed by Jeff Hankins, 30-Aug-2009.) |
Ref | Expression |
---|---|
xpss2 | ⊢ (𝐴 ⊆ 𝐵 → (𝐶 × 𝐴) ⊆ (𝐶 × 𝐵)) |
Step | Hyp | Ref | Expression |
---|---|---|---|
1 | ssid 3587 | . 2 ⊢ 𝐶 ⊆ 𝐶 | |
2 | xpss12 5148 | . 2 ⊢ ((𝐶 ⊆ 𝐶 ∧ 𝐴 ⊆ 𝐵) → (𝐶 × 𝐴) ⊆ (𝐶 × 𝐵)) | |
3 | 1, 2 | mpan 702 | 1 ⊢ (𝐴 ⊆ 𝐵 → (𝐶 × 𝐴) ⊆ (𝐶 × 𝐵)) |
Colors of variables: wff setvar class |
Syntax hints: → wi 4 ⊆ wss 3540 × cxp 5036 |
This theorem was proved from axioms: ax-mp 5 ax-1 6 ax-2 7 ax-3 8 ax-gen 1713 ax-4 1728 ax-5 1827 ax-6 1875 ax-7 1922 ax-10 2006 ax-11 2021 ax-12 2034 ax-13 2234 ax-ext 2590 |
This theorem depends on definitions: df-bi 196 df-or 384 df-an 385 df-tru 1478 df-ex 1696 df-nf 1701 df-sb 1868 df-clab 2597 df-cleq 2603 df-clel 2606 df-nfc 2740 df-in 3547 df-ss 3554 df-opab 4644 df-xp 5044 |
This theorem is referenced by: xpdom3 7943 marypha1lem 8222 unctb 8910 axresscn 9848 imasvscafn 16020 imasvscaf 16022 xpsc0 16043 xpsc1 16044 gass 17557 gsum2d 18194 tx2cn 21223 txtube 21253 txcmplem1 21254 hausdiag 21258 xkoinjcn 21300 caussi 22903 dvfval 23467 issh2 27450 qtophaus 29231 2ndmbfm 29650 sxbrsigalem0 29660 cvmlift2lem9 30547 cvmlift2lem11 30549 filnetlem3 31545 trclexi 36946 cnvtrcl0 36952 ovolval5lem2 39543 ovnovollem1 39546 ovnovollem2 39547 |
Copyright terms: Public domain | W3C validator |