Theorem imaeq1 6026

Description: Equality theorem for image. (Contributed by NM, 14-Aug-1994.)

Assertion

Ref	Expression
imaeq1	⊢ (𝐴 = 𝐵 → (𝐴 “ 𝐶) = (𝐵 “ 𝐶))

Proof of Theorem imaeq1

Step	Hyp	Ref	Expression
1		reseq1 5944	. . 3 ⊢ (𝐴 = 𝐵 → (𝐴 ↾ 𝐶) = (𝐵 ↾ 𝐶))
2	1	rneqd 5902	. 2 ⊢ (𝐴 = 𝐵 → ran (𝐴 ↾ 𝐶) = ran (𝐵 ↾ 𝐶))
3		df-ima 5651	. 2 ⊢ (𝐴 “ 𝐶) = ran (𝐴 ↾ 𝐶)
4		df-ima 5651	. 2 ⊢ (𝐵 “ 𝐶) = ran (𝐵 ↾ 𝐶)
5	2, 3, 4	3eqtr4g 2789	1 ⊢ (𝐴 = 𝐵 → (𝐴 “ 𝐶) = (𝐵 “ 𝐶))

Syntax hints:   → wi 4   = wceq 1540  ran crn 5639   ↾ cres 5640   “ cima 5641

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 1910  ax-6 1967  ax-7 2008  ax-8 2111  ax-9 2119  ax-ext 2701

This theorem depends on definitions:  df-bi 207  df-an 396  df-or 848  df-3an 1088  df-tru 1543  df-fal 1553  df-ex 1780  df-sb 2066  df-clab 2708  df-cleq 2721  df-clel 2803  df-rab 3406  df-v 3449  df-dif 3917  df-un 3919  df-in 3921  df-ss 3931  df-nul 4297  df-if 4489  df-sn 4590  df-pr 4592  df-op 4596  df-br 5108  df-opab 5170  df-cnv 5646  df-dm 5648  df-rn 5649  df-res 5650  df-ima 5651

This theorem is referenced by:  imaeq1i  6028  imaeq1d  6030  suppval  8141  naddcllem  8640  eceq2  8712  marypha1lem  9384  marypha1  9385  ackbij2lem2  10192  ackbij2lem3  10193  r1om  10196  limsupval  15440  isacs1i  17618  mreacs  17619  islindf  21721  iscnp  23124  xkoccn  23506  xkohaus  23540  xkoco1cn  23544  xkoco2cn  23545  xkococnlem  23546  xkococn  23547  xkoinjcn  23574  fmval  23830  fmf  23832  utoptop  24122  restutop  24125  restutopopn  24126  ustuqtoplem  24127  ustuqtop1  24129  ustuqtop2  24130  ustuqtop4  24132  ustuqtop5  24133  utopsnneiplem  24135  utopsnnei  24137  neipcfilu  24183  psmetutop  24455  cfilfval  25164  elply2  26101  coeeu  26130  coelem  26131  coeeq  26132  dmarea  26867  negsval  27931  mclsax  35556  tailfval  36360  bj-cleq  36950  bj-funun  37240  poimirlem15  37629  poimirlem24  37638  brtrclfv2  43716  liminfval  45757  ushggricedg  47927  uhgrimisgrgric  47931