![]() |
Metamath Proof Explorer |
< Previous
Next >
Nearby theorems |
|
Mirrors > Home > MPE Home > Th. List > resima2 | Structured version Visualization version GIF version |
Description: Image under a restricted class. (Contributed by FL, 31-Aug-2009.) (Proof shortened by JJ, 25-Aug-2021.) |
Ref | Expression |
---|---|
resima2 | ⊢ (𝐵 ⊆ 𝐶 → ((𝐴 ↾ 𝐶) “ 𝐵) = (𝐴 “ 𝐵)) |
Step | Hyp | Ref | Expression |
---|---|---|---|
1 | sseqin2 4214 | . . . 4 ⊢ (𝐵 ⊆ 𝐶 ↔ (𝐶 ∩ 𝐵) = 𝐵) | |
2 | reseq2 5975 | . . . 4 ⊢ ((𝐶 ∩ 𝐵) = 𝐵 → (𝐴 ↾ (𝐶 ∩ 𝐵)) = (𝐴 ↾ 𝐵)) | |
3 | 1, 2 | sylbi 216 | . . 3 ⊢ (𝐵 ⊆ 𝐶 → (𝐴 ↾ (𝐶 ∩ 𝐵)) = (𝐴 ↾ 𝐵)) |
4 | 3 | rneqd 5936 | . 2 ⊢ (𝐵 ⊆ 𝐶 → ran (𝐴 ↾ (𝐶 ∩ 𝐵)) = ran (𝐴 ↾ 𝐵)) |
5 | df-ima 5688 | . . 3 ⊢ ((𝐴 ↾ 𝐶) “ 𝐵) = ran ((𝐴 ↾ 𝐶) ↾ 𝐵) | |
6 | resres 5993 | . . . 4 ⊢ ((𝐴 ↾ 𝐶) ↾ 𝐵) = (𝐴 ↾ (𝐶 ∩ 𝐵)) | |
7 | 6 | rneqi 5935 | . . 3 ⊢ ran ((𝐴 ↾ 𝐶) ↾ 𝐵) = ran (𝐴 ↾ (𝐶 ∩ 𝐵)) |
8 | 5, 7 | eqtri 2758 | . 2 ⊢ ((𝐴 ↾ 𝐶) “ 𝐵) = ran (𝐴 ↾ (𝐶 ∩ 𝐵)) |
9 | df-ima 5688 | . 2 ⊢ (𝐴 “ 𝐵) = ran (𝐴 ↾ 𝐵) | |
10 | 4, 8, 9 | 3eqtr4g 2795 | 1 ⊢ (𝐵 ⊆ 𝐶 → ((𝐴 ↾ 𝐶) “ 𝐵) = (𝐴 “ 𝐵)) |
Colors of variables: wff setvar class |
Syntax hints: → wi 4 = wceq 1539 ∩ cin 3946 ⊆ wss 3947 ran crn 5676 ↾ cres 5677 “ cima 5678 |
This theorem was proved from axioms: ax-mp 5 ax-1 6 ax-2 7 ax-3 8 ax-gen 1795 ax-4 1809 ax-5 1911 ax-6 1969 ax-7 2009 ax-8 2106 ax-9 2114 ax-10 2135 ax-12 2169 ax-ext 2701 ax-sep 5298 ax-nul 5305 ax-pr 5426 |
This theorem depends on definitions: df-bi 206 df-an 395 df-or 844 df-3an 1087 df-tru 1542 df-fal 1552 df-ex 1780 df-nf 1784 df-sb 2066 df-clab 2708 df-cleq 2722 df-clel 2808 df-rab 3431 df-v 3474 df-dif 3950 df-un 3952 df-in 3954 df-ss 3964 df-nul 4322 df-if 4528 df-sn 4628 df-pr 4630 df-op 4634 df-br 5148 df-opab 5210 df-xp 5681 df-rel 5682 df-cnv 5683 df-dm 5685 df-rn 5686 df-res 5687 df-ima 5688 |
This theorem is referenced by: ressuppss 8170 ressuppssdif 8172 naddcllem 8677 marypha1lem 9430 ackbij2lem3 10238 eqg0subgecsn 19112 dmdprdsplit2lem 19956 cnpresti 23012 cnprest 23013 limcflf 25630 limcresi 25634 limciun 25643 efopnlem2 26401 negsval 27739 pthhashvtx 34416 cvmopnlem 34567 cvmlift2lem9a 34592 poimirlem4 36795 limsupresre 44710 limsupresico 44714 liminfresico 44785 |
Copyright terms: Public domain | W3C validator |