Metamath Proof Explorer < Previous   Next > Nearby theorems Mirrors  >  Home  >  MPE Home  >  Th. List  >  resima2 Structured version   Visualization version   GIF version

Theorem resima2 5578
 Description: Image under a restricted class. (Contributed by FL, 31-Aug-2009.) (Proof shortened by JJ, 25-Aug-2021.)
Assertion
Ref Expression
resima2 (𝐵𝐶 → ((𝐴𝐶) “ 𝐵) = (𝐴𝐵))

Proof of Theorem resima2
StepHypRef Expression
1 sseqin2 3948 . . . 4 (𝐵𝐶 ↔ (𝐶𝐵) = 𝐵)
2 reseq2 5534 . . . 4 ((𝐶𝐵) = 𝐵 → (𝐴 ↾ (𝐶𝐵)) = (𝐴𝐵))
31, 2sylbi 207 . . 3 (𝐵𝐶 → (𝐴 ↾ (𝐶𝐵)) = (𝐴𝐵))
43rneqd 5496 . 2 (𝐵𝐶 → ran (𝐴 ↾ (𝐶𝐵)) = ran (𝐴𝐵))
5 df-ima 5267 . . 3 ((𝐴𝐶) “ 𝐵) = ran ((𝐴𝐶) ↾ 𝐵)
6 resres 5555 . . . 4 ((𝐴𝐶) ↾ 𝐵) = (𝐴 ↾ (𝐶𝐵))
76rneqi 5495 . . 3 ran ((𝐴𝐶) ↾ 𝐵) = ran (𝐴 ↾ (𝐶𝐵))
85, 7eqtri 2770 . 2 ((𝐴𝐶) “ 𝐵) = ran (𝐴 ↾ (𝐶𝐵))
9 df-ima 5267 . 2 (𝐴𝐵) = ran (𝐴𝐵)
104, 8, 93eqtr4g 2807 1 (𝐵𝐶 → ((𝐴𝐶) “ 𝐵) = (𝐴𝐵))
 Colors of variables: wff setvar class Syntax hints:   → wi 4   = wceq 1620   ∩ cin 3702   ⊆ wss 3703  ran crn 5255   ↾ cres 5256   “ cima 5257 This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1859  ax-4 1874  ax-5 1976  ax-6 2042  ax-7 2078  ax-9 2136  ax-10 2156  ax-11 2171  ax-12 2184  ax-13 2379  ax-ext 2728  ax-sep 4921  ax-nul 4929  ax-pr 5043 This theorem depends on definitions:  df-bi 197  df-or 384  df-an 385  df-3an 1074  df-tru 1623  df-ex 1842  df-nf 1847  df-sb 2035  df-clab 2735  df-cleq 2741  df-clel 2744  df-nfc 2879  df-rab 3047  df-v 3330  df-dif 3706  df-un 3708  df-in 3710  df-ss 3717  df-nul 4047  df-if 4219  df-sn 4310  df-pr 4312  df-op 4316  df-br 4793  df-opab 4853  df-xp 5260  df-rel 5261  df-cnv 5262  df-dm 5264  df-rn 5265  df-res 5266  df-ima 5267 This theorem is referenced by:  ressuppss  7470  ressuppssdif  7472  marypha1lem  8492  ackbij2lem3  9226  dmdprdsplit2lem  18615  cnpresti  21265  cnprest  21266  limcflf  23815  limcresi  23819  limciun  23828  efopnlem2  24573  cvmopnlem  31538  cvmlift2lem9a  31563  poimirlem4  33695  limsupresre  40400  limsupresico  40404  liminfresico  40475
 Copyright terms: Public domain W3C validator