Theorem imaeq1 6014

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 5932	. . 3 ⊢ (𝐴 = 𝐵 → (𝐴 ↾ 𝐶) = (𝐵 ↾ 𝐶))
2	1	rneqd 5887	. 2 ⊢ (𝐴 = 𝐵 → ran (𝐴 ↾ 𝐶) = ran (𝐵 ↾ 𝐶))
3		df-ima 5637	. 2 ⊢ (𝐴 “ 𝐶) = ran (𝐴 ↾ 𝐶)
4		df-ima 5637	. 2 ⊢ (𝐵 “ 𝐶) = ran (𝐵 ↾ 𝐶)
5	2, 3, 4	3eqtr4g 2797	1 ⊢ (𝐴 = 𝐵 → (𝐴 “ 𝐶) = (𝐵 “ 𝐶))

Syntax hints:   → wi 4   = wceq 1542  ran crn 5625   ↾ cres 5626   “ cima 5627

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 1969  ax-7 2010  ax-8 2116  ax-9 2124  ax-ext 2709

This theorem depends on definitions:  df-bi 207  df-an 396  df-or 849  df-3an 1089  df-tru 1545  df-fal 1555  df-ex 1782  df-sb 2069  df-clab 2716  df-cleq 2729  df-clel 2812  df-rab 3391  df-v 3432  df-dif 3893  df-un 3895  df-in 3897  df-ss 3907  df-nul 4275  df-if 4468  df-sn 4569  df-pr 4571  df-op 4575  df-br 5087  df-opab 5149  df-cnv 5632  df-dm 5634  df-rn 5635  df-res 5636  df-ima 5637

This theorem is referenced by:  imaeq1i  6016  imaeq1d  6018  suppval  8105  naddcllem  8605  eceq2  8678  marypha1lem  9339  marypha1  9340  ackbij2lem2  10152  ackbij2lem3  10153  r1om  10156  limsupval  15427  isacs1i  17614  mreacs  17615  islindf  21802  iscnp  23212  xkoccn  23594  xkohaus  23628  xkoco1cn  23632  xkoco2cn  23633  xkococnlem  23634  xkococn  23635  xkoinjcn  23662  fmval  23918  fmf  23920  utoptop  24209  restutop  24212  restutopopn  24213  ustuqtoplem  24214  ustuqtop1  24216  ustuqtop2  24217  ustuqtop4  24219  ustuqtop5  24220  utopsnneiplem  24222  utopsnnei  24224  neipcfilu  24270  psmetutop  24542  cfilfval  25241  elply2  26171  coeeu  26200  coelem  26201  coeeq  26202  dmarea  26934  negsval  28031  mclsax  35767  tailfval  36570  bj-cleq  37285  bj-funun  37582  poimirlem15  37970  poimirlem24  37979  brtrclfv2  44172  liminfval  46205  ushggricedg  48415  uhgrimisgrgric  48419