![]() |
Metamath Proof Explorer |
< Previous
Next >
Nearby theorems |
|
Mirrors > Home > MPE Home > Th. List > imass1 | Structured version Visualization version GIF version |
Description: Subset theorem for image. (Contributed by NM, 16-Mar-2004.) |
Ref | Expression |
---|---|
imass1 | ⊢ (𝐴 ⊆ 𝐵 → (𝐴 “ 𝐶) ⊆ (𝐵 “ 𝐶)) |
Step | Hyp | Ref | Expression |
---|---|---|---|
1 | ssres 5761 | . . 3 ⊢ (𝐴 ⊆ 𝐵 → (𝐴 ↾ 𝐶) ⊆ (𝐵 ↾ 𝐶)) | |
2 | rnss 5691 | . . 3 ⊢ ((𝐴 ↾ 𝐶) ⊆ (𝐵 ↾ 𝐶) → ran (𝐴 ↾ 𝐶) ⊆ ran (𝐵 ↾ 𝐶)) | |
3 | 1, 2 | syl 17 | . 2 ⊢ (𝐴 ⊆ 𝐵 → ran (𝐴 ↾ 𝐶) ⊆ ran (𝐵 ↾ 𝐶)) |
4 | df-ima 5456 | . 2 ⊢ (𝐴 “ 𝐶) = ran (𝐴 ↾ 𝐶) | |
5 | df-ima 5456 | . 2 ⊢ (𝐵 “ 𝐶) = ran (𝐵 ↾ 𝐶) | |
6 | 3, 4, 5 | 3sstr4g 3933 | 1 ⊢ (𝐴 ⊆ 𝐵 → (𝐴 “ 𝐶) ⊆ (𝐵 “ 𝐶)) |
Colors of variables: wff setvar class |
Syntax hints: → wi 4 ⊆ wss 3859 ran crn 5444 ↾ cres 5445 “ cima 5446 |
This theorem was proved from axioms: ax-mp 5 ax-1 6 ax-2 7 ax-3 8 ax-gen 1777 ax-4 1791 ax-5 1888 ax-6 1947 ax-7 1992 ax-8 2083 ax-9 2091 ax-10 2112 ax-11 2126 ax-12 2141 ax-ext 2769 |
This theorem depends on definitions: df-bi 208 df-an 397 df-or 843 df-3an 1082 df-tru 1525 df-ex 1762 df-nf 1766 df-sb 2043 df-clab 2776 df-cleq 2788 df-clel 2863 df-nfc 2935 df-rab 3114 df-v 3439 df-dif 3862 df-un 3864 df-in 3866 df-ss 3874 df-nul 4212 df-if 4382 df-sn 4473 df-pr 4475 df-op 4479 df-br 4963 df-opab 5025 df-cnv 5451 df-dm 5453 df-rn 5454 df-res 5455 df-ima 5456 |
This theorem is referenced by: vdwnnlem1 16160 dprdres 18867 imasnopn 21982 imasncld 21983 imasncls 21984 utoptop 22526 restutop 22529 ustuqtop3 22535 utopreg 22544 metustbl 22859 imadifxp 30041 esum2d 30969 eulerpartlemmf 31250 brtrclfv2 39576 frege97d 39601 frege109d 39606 frege131d 39613 hess 39630 resimass 41070 setrecsss 44303 |
Copyright terms: Public domain | W3C validator |