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

Theorem resima2 5876
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 4178 . . . 4 (𝐵𝐶 ↔ (𝐶𝐵) = 𝐵)
2 reseq2 5836 . . . 4 ((𝐶𝐵) = 𝐵 → (𝐴 ↾ (𝐶𝐵)) = (𝐴𝐵))
31, 2sylbi 220 . . 3 (𝐵𝐶 → (𝐴 ↾ (𝐶𝐵)) = (𝐴𝐵))
43rneqd 5796 . 2 (𝐵𝐶 → ran (𝐴 ↾ (𝐶𝐵)) = ran (𝐴𝐵))
5 df-ima 5556 . . 3 ((𝐴𝐶) “ 𝐵) = ran ((𝐴𝐶) ↾ 𝐵)
6 resres 5854 . . . 4 ((𝐴𝐶) ↾ 𝐵) = (𝐴 ↾ (𝐶𝐵))
76rneqi 5795 . . 3 ran ((𝐴𝐶) ↾ 𝐵) = ran (𝐴 ↾ (𝐶𝐵))
85, 7eqtri 2847 . 2 ((𝐴𝐶) “ 𝐵) = ran (𝐴 ↾ (𝐶𝐵))
9 df-ima 5556 . 2 (𝐴𝐵) = ran (𝐴𝐵)
104, 8, 93eqtr4g 2884 1 (𝐵𝐶 → ((𝐴𝐶) “ 𝐵) = (𝐴𝐵))
Colors of variables: wff setvar class
Syntax hints:  wi 4   = wceq 1538  cin 3919  wss 3920  ran crn 5544  cres 5545  cima 5546
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1797  ax-4 1811  ax-5 1912  ax-6 1971  ax-7 2016  ax-8 2117  ax-9 2125  ax-10 2146  ax-11 2162  ax-12 2179  ax-ext 2796  ax-sep 5190  ax-nul 5197  ax-pr 5318
This theorem depends on definitions:  df-bi 210  df-an 400  df-or 845  df-3an 1086  df-tru 1541  df-ex 1782  df-nf 1786  df-sb 2071  df-clab 2803  df-cleq 2817  df-clel 2896  df-nfc 2964  df-rab 3142  df-v 3483  df-dif 3923  df-un 3925  df-in 3927  df-ss 3937  df-nul 4278  df-if 4452  df-sn 4552  df-pr 4554  df-op 4558  df-br 5054  df-opab 5116  df-xp 5549  df-rel 5550  df-cnv 5551  df-dm 5553  df-rn 5554  df-res 5555  df-ima 5556
This theorem is referenced by:  ressuppss  7846  ressuppssdif  7848  marypha1lem  8895  ackbij2lem3  9662  dmdprdsplit2lem  19170  cnpresti  21899  cnprest  21900  limcflf  24490  limcresi  24494  limciun  24503  efopnlem2  25254  pthhashvtx  32434  cvmopnlem  32585  cvmlift2lem9a  32610  poimirlem4  35007  limsupresre  42265  limsupresico  42269  liminfresico  42340
  Copyright terms: Public domain W3C validator