Theorem imaeq2i 6015

Description: Equality theorem for image. (Contributed by NM, 21-Dec-2008.)

Hypothesis

Ref	Expression
imaeq1i.1	⊢ 𝐴 = 𝐵

Assertion

Ref	Expression
imaeq2i	⊢ (𝐶 “ 𝐴) = (𝐶 “ 𝐵)

Proof of Theorem imaeq2i

Step	Hyp	Ref	Expression
1		imaeq1i.1	. 2 ⊢ 𝐴 = 𝐵
2		imaeq2 6013	. 2 ⊢ (𝐴 = 𝐵 → (𝐶 “ 𝐴) = (𝐶 “ 𝐵))
3	1, 2	ax-mp 5	1 ⊢ (𝐶 “ 𝐴) = (𝐶 “ 𝐵)

Syntax hints:   = wceq 1541   “ 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-xp 5628  df-cnv 5630  df-dm 5632  df-rn 5633  df-res 5634  df-ima 5635

This theorem is referenced by:  cnvimarndm  6040  dmco  6211  imain  6575  fnimapr  6915  fnimatpd  6916  ssimaex  6917  intpreima  7013  resfunexg  7159  imauni  7190  isoini2  7283  fsuppeq  8115  fsuppeqg  8116  naddasslem1  8620  naddasslem2  8621  uniqs  8709  pwfilem  9216  fiint  9225  jech9.3  9724  infxpenlem  9921  hsmexlem4  10337  fcdmnn0supp  12456  fcdmnn0fsupp  12457  fcdmnn0suppg  12458  hashkf  14253  ghmeqker  19170  gsumval3lem1  19832  gsumval3lem2  19833  islinds2  21766  lindsind2  21772  mhpmulcl  22090  snclseqg  24058  retopbas  24702  ismbf3d  25609  i1fima  25633  i1fd  25636  itg1addlem5  25655  limciun  25849  plyeq0  26170  bday0s  27799  bday1s  27802  madeval2  27821  old1  27847  madeoldsuc  27857  bdayiun  27887  negs0s  27995  negs1s  27996  negsbdaylem  28025  onscutlt  28232  onsiso  28236  bdayon  28240  n0sbday  28312  bdayn0p1  28327  spthispth  29746  0pth  30149  1pthdlem2  30160  eupth2lemb  30261  htth  30942  fcoinver  32628  ffs2  32755  ffsrn  32756  tocyccntz  33175  elrspunidl  33458  sibfof  34446  eulerpartgbij  34478  eulerpartlemmf  34481  eulerpartlemgh  34484  eulerpart  34488  fiblem  34504  orrvcval4  34571  cvmsss2  35417  opelco3  35918  poimirlem3  37763  poimirlem30  37790  mbfposadd  37807  itg2addnclem2  37812  ftc1anclem5  37837  ftc1anclem6  37838  pwfi2f1o  43280  brtrclfv2  43910  binomcxp  44540  fcoreslem1  47251  isubgr3stgrlem6  48159