Theorem imaeq1 6055

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 5976	. . 3 ⊢ (𝐴 = 𝐵 → (𝐴 ↾ 𝐶) = (𝐵 ↾ 𝐶))
2	1	rneqd 5938	. 2 ⊢ (𝐴 = 𝐵 → ran (𝐴 ↾ 𝐶) = ran (𝐵 ↾ 𝐶))
3		df-ima 5690	. 2 ⊢ (𝐴 “ 𝐶) = ran (𝐴 ↾ 𝐶)
4		df-ima 5690	. 2 ⊢ (𝐵 “ 𝐶) = ran (𝐵 ↾ 𝐶)
5	2, 3, 4	3eqtr4g 2798	1 ⊢ (𝐴 = 𝐵 → (𝐴 “ 𝐶) = (𝐵 “ 𝐶))

Syntax hints:   → wi 4   = wceq 1542  ran crn 5678   ↾ cres 5679   “ cima 5680

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1798  ax-4 1812  ax-5 1914  ax-6 1972  ax-7 2012  ax-8 2109  ax-9 2117  ax-ext 2704

This theorem depends on definitions:  df-bi 206  df-an 398  df-or 847  df-3an 1090  df-tru 1545  df-fal 1555  df-ex 1783  df-sb 2069  df-clab 2711  df-cleq 2725  df-clel 2811  df-rab 3434  df-v 3477  df-dif 3952  df-un 3954  df-in 3956  df-ss 3966  df-nul 4324  df-if 4530  df-sn 4630  df-pr 4632  df-op 4636  df-br 5150  df-opab 5212  df-cnv 5685  df-dm 5687  df-rn 5688  df-res 5689  df-ima 5690

This theorem is referenced by:  imaeq1i  6057  imaeq1d  6059  suppval  8148  naddcllem  8675  eceq2  8743  marypha1lem  9428  marypha1  9429  ackbij2lem2  10235  ackbij2lem3  10236  r1om  10239  limsupval  15418  isacs1i  17601  mreacs  17602  islindf  21367  iscnp  22741  xkoccn  23123  xkohaus  23157  xkoco1cn  23161  xkoco2cn  23162  xkococnlem  23163  xkococn  23164  xkoinjcn  23191  fmval  23447  fmf  23449  utoptop  23739  restutop  23742  restutopopn  23743  ustuqtoplem  23744  ustuqtop1  23746  ustuqtop2  23747  ustuqtop4  23749  ustuqtop5  23750  utopsnneiplem  23752  utopsnnei  23754  neipcfilu  23801  psmetutop  24076  cfilfval  24781  elply2  25710  coeeu  25739  coelem  25740  coeeq  25741  dmarea  26462  negsval  27503  mclsax  34591  tailfval  35305  bj-cleq  35891  bj-funun  36181  poimirlem15  36551  poimirlem24  36560  brtrclfv2  42526  liminfval  44523  isomgreqve  46541  isomgrsym  46552  isomgrtr  46555  ushrisomgr  46557