Theorem imaeq1 6012

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 5930	. . 3 ⊢ (𝐴 = 𝐵 → (𝐴 ↾ 𝐶) = (𝐵 ↾ 𝐶))
2	1	rneqd 5885	. 2 ⊢ (𝐴 = 𝐵 → ran (𝐴 ↾ 𝐶) = ran (𝐵 ↾ 𝐶))
3		df-ima 5635	. 2 ⊢ (𝐴 “ 𝐶) = ran (𝐴 ↾ 𝐶)
4		df-ima 5635	. 2 ⊢ (𝐵 “ 𝐶) = ran (𝐵 ↾ 𝐶)
5	2, 3, 4	3eqtr4g 2794	1 ⊢ (𝐴 = 𝐵 → (𝐴 “ 𝐶) = (𝐵 “ 𝐶))

Syntax hints:   → wi 4   = wceq 1541  ran crn 5623   ↾ cres 5624   “ cima 5625

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1796  ax-4 1810  ax-5 1911  ax-6 1968  ax-7 2009  ax-8 2115  ax-9 2123  ax-ext 2706

This theorem depends on definitions:  df-bi 207  df-an 396  df-or 848  df-3an 1088  df-tru 1544  df-fal 1554  df-ex 1781  df-sb 2068  df-clab 2713  df-cleq 2726  df-clel 2809  df-rab 3398  df-v 3440  df-dif 3902  df-un 3904  df-in 3906  df-ss 3916  df-nul 4284  df-if 4478  df-sn 4579  df-pr 4581  df-op 4585  df-br 5097  df-opab 5159  df-cnv 5630  df-dm 5632  df-rn 5633  df-res 5634  df-ima 5635

This theorem is referenced by:  imaeq1i  6014  imaeq1d  6016  suppval  8102  naddcllem  8602  eceq2  8674  marypha1lem  9334  marypha1  9335  ackbij2lem2  10147  ackbij2lem3  10148  r1om  10151  limsupval  15395  isacs1i  17578  mreacs  17579  islindf  21765  iscnp  23179  xkoccn  23561  xkohaus  23595  xkoco1cn  23599  xkoco2cn  23600  xkococnlem  23601  xkococn  23602  xkoinjcn  23629  fmval  23885  fmf  23887  utoptop  24176  restutop  24179  restutopopn  24180  ustuqtoplem  24181  ustuqtop1  24183  ustuqtop2  24184  ustuqtop4  24186  ustuqtop5  24187  utopsnneiplem  24189  utopsnnei  24191  neipcfilu  24237  psmetutop  24509  cfilfval  25218  elply2  26155  coeeu  26184  coelem  26185  coeeq  26186  dmarea  26921  negsval  27994  mclsax  35712  tailfval  36515  bj-cleq  37106  bj-funun  37396  poimirlem15  37775  poimirlem24  37784  brtrclfv2  43910  liminfval  45945  ushggricedg  48115  uhgrimisgrgric  48119