Theorem resima2 5998

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

Step	Hyp	Ref	Expression
1		sseqin2 4173	. . . 4 ⊢ (𝐵 ⊆ 𝐶 ↔ (𝐶 ∩ 𝐵) = 𝐵)
2		reseq2 5956	. . . 4 ⊢ ((𝐶 ∩ 𝐵) = 𝐵 → (𝐴 ↾ (𝐶 ∩ 𝐵)) = (𝐴 ↾ 𝐵))
3	1, 2	sylbi 219	. . 3 ⊢ (𝐵 ⊆ 𝐶 → (𝐴 ↾ (𝐶 ∩ 𝐵)) = (𝐴 ↾ 𝐵))
4	3	rneqd 5910	. 2 ⊢ (𝐵 ⊆ 𝐶 → ran (𝐴 ↾ (𝐶 ∩ 𝐵)) = ran (𝐴 ↾ 𝐵))
5		df-ima 5656	. . 3 ⊢ ((𝐴 ↾ 𝐶) “ 𝐵) = ran ((𝐴 ↾ 𝐶) ↾ 𝐵)
6		resres 5974	. . . 4 ⊢ ((𝐴 ↾ 𝐶) ↾ 𝐵) = (𝐴 ↾ (𝐶 ∩ 𝐵))
7	6	rneqi 5909	. . 3 ⊢ ran ((𝐴 ↾ 𝐶) ↾ 𝐵) = ran (𝐴 ↾ (𝐶 ∩ 𝐵))
8	5, 7	eqtri 2784	. 2 ⊢ ((𝐴 ↾ 𝐶) “ 𝐵) = ran (𝐴 ↾ (𝐶 ∩ 𝐵))
9		df-ima 5656	. 2 ⊢ (𝐴 “ 𝐵) = ran (𝐴 ↾ 𝐵)
10	4, 8, 9	3eqtr4g 2821	1 ⊢ (𝐵 ⊆ 𝐶 → ((𝐴 ↾ 𝐶) “ 𝐵) = (𝐴 “ 𝐵))

Syntax hints:   → wi 4   = wceq 1559   ∩ cin 3901   ⊆ wss 3902  ran crn 5644   ↾ cres 5645   “ cima 5646

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1814  ax-4 1828  ax-5 1929  ax-6 1986  ax-7 2027  ax-8 2143  ax-9 2151  ax-ext 2733  ax-sep 5243  ax-pr 5387

This theorem depends on definitions:  df-bi 209  df-an 400  df-or 859  df-3an 1099  df-tru 1562  df-fal 1572  df-ex 1799  df-sb 2090  df-clab 2740  df-cleq 2753  df-clel 2836  df-ral 3076  df-rex 3086  df-rab 3414  df-v 3455  df-dif 3905  df-un 3907  df-in 3909  df-ss 3919  df-nul 4284  df-if 4478  df-sn 4580  df-pr 4582  df-op 4586  df-br 5098  df-opab 5160  df-xp 5649  df-rel 5650  df-cnv 5651  df-dm 5653  df-rn 5654  df-res 5655  df-ima 5656

This theorem is referenced by:  ressuppss  8156  ressuppssdif  8158  naddcllem  8639  marypha1lem  9372  ackbij2lem3  10189  eqg0subgecsn  19228  dmdprdsplit2lem  20077  cnpresti  23335  cnprest  23336  limcflf  25930  limcresi  25934  limciun  25943  efopnlem2  26709  negsval  28105  pthhashvtx  35438  cvmopnlem  35588  cvmlift2lem9a  35613  poimirlem4  38083  limsupresre  46230  limsupresico  46234  liminfresico  46305  uhgrimisgrgric  48513