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

Theorem resima2 6036
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 4231 . . . 4 (𝐵𝐶 ↔ (𝐶𝐵) = 𝐵)
2 reseq2 5995 . . . 4 ((𝐶𝐵) = 𝐵 → (𝐴 ↾ (𝐶𝐵)) = (𝐴𝐵))
31, 2sylbi 217 . . 3 (𝐵𝐶 → (𝐴 ↾ (𝐶𝐵)) = (𝐴𝐵))
43rneqd 5952 . 2 (𝐵𝐶 → ran (𝐴 ↾ (𝐶𝐵)) = ran (𝐴𝐵))
5 df-ima 5702 . . 3 ((𝐴𝐶) “ 𝐵) = ran ((𝐴𝐶) ↾ 𝐵)
6 resres 6013 . . . 4 ((𝐴𝐶) ↾ 𝐵) = (𝐴 ↾ (𝐶𝐵))
76rneqi 5951 . . 3 ran ((𝐴𝐶) ↾ 𝐵) = ran (𝐴 ↾ (𝐶𝐵))
85, 7eqtri 2763 . 2 ((𝐴𝐶) “ 𝐵) = ran (𝐴 ↾ (𝐶𝐵))
9 df-ima 5702 . 2 (𝐴𝐵) = ran (𝐴𝐵)
104, 8, 93eqtr4g 2800 1 (𝐵𝐶 → ((𝐴𝐶) “ 𝐵) = (𝐴𝐵))
Colors of variables: wff setvar class
Syntax hints:  wi 4   = wceq 1537  cin 3962  wss 3963  ran crn 5690  cres 5691  cima 5692
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1792  ax-4 1806  ax-5 1908  ax-6 1965  ax-7 2005  ax-8 2108  ax-9 2116  ax-ext 2706  ax-sep 5302  ax-nul 5312  ax-pr 5438
This theorem depends on definitions:  df-bi 207  df-an 396  df-or 848  df-3an 1088  df-tru 1540  df-fal 1550  df-ex 1777  df-sb 2063  df-clab 2713  df-cleq 2727  df-clel 2814  df-ral 3060  df-rex 3069  df-rab 3434  df-v 3480  df-dif 3966  df-un 3968  df-in 3970  df-ss 3980  df-nul 4340  df-if 4532  df-sn 4632  df-pr 4634  df-op 4638  df-br 5149  df-opab 5211  df-xp 5695  df-rel 5696  df-cnv 5697  df-dm 5699  df-rn 5700  df-res 5701  df-ima 5702
This theorem is referenced by:  ressuppss  8207  ressuppssdif  8209  naddcllem  8713  marypha1lem  9471  ackbij2lem3  10278  eqg0subgecsn  19228  dmdprdsplit2lem  20080  cnpresti  23312  cnprest  23313  limcflf  25931  limcresi  25935  limciun  25944  efopnlem2  26714  negsval  28072  pthhashvtx  35112  cvmopnlem  35263  cvmlift2lem9a  35288  poimirlem4  37611  limsupresre  45652  limsupresico  45656  liminfresico  45727  uhgrimisgrgric  47837
  Copyright terms: Public domain W3C validator