Theorem imaeq2i 6006

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 6004	. 2 ⊢ (𝐴 = 𝐵 → (𝐶 “ 𝐴) = (𝐶 “ 𝐵))
3	1, 2	ax-mp 5	1 ⊢ (𝐶 “ 𝐴) = (𝐶 “ 𝐵)

Syntax hints:   = wceq 1541   “ cima 5617

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 2113  ax-9 2121  ax-ext 2703

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 2710  df-cleq 2723  df-clel 2806  df-rab 3396  df-v 3438  df-dif 3900  df-un 3902  df-in 3904  df-ss 3914  df-nul 4281  df-if 4473  df-sn 4574  df-pr 4576  df-op 4580  df-br 5090  df-opab 5152  df-xp 5620  df-cnv 5622  df-dm 5624  df-rn 5625  df-res 5626  df-ima 5627

This theorem is referenced by:  cnvimarndm  6031  dmco  6202  imain  6566  fnimapr  6905  fnimatpd  6906  ssimaex  6907  intpreima  7003  resfunexg  7149  imauni  7180  isoini2  7273  fsuppeq  8105  fsuppeqg  8106  naddasslem1  8609  naddasslem2  8610  uniqs  8698  pwfilem  9202  fiint  9211  jech9.3  9707  infxpenlem  9904  hsmexlem4  10320  fcdmnn0supp  12438  fcdmnn0fsupp  12439  fcdmnn0suppg  12440  hashkf  14239  ghmeqker  19155  gsumval3lem1  19817  gsumval3lem2  19818  islinds2  21750  lindsind2  21756  mhpmulcl  22064  snclseqg  24031  retopbas  24675  ismbf3d  25582  i1fima  25606  i1fd  25609  itg1addlem5  25628  limciun  25822  plyeq0  26143  bday0s  27772  bday1s  27775  madeval2  27794  old1  27820  madeoldsuc  27830  bdayiun  27860  negs0s  27968  negs1s  27969  negsbdaylem  27998  onscutlt  28201  onsiso  28205  bdayon  28209  n0sbday  28280  bdayn0p1  28294  spthispth  29702  0pth  30105  1pthdlem2  30116  eupth2lemb  30217  htth  30898  fcoinver  32584  ffs2  32710  ffsrn  32711  tocyccntz  33113  elrspunidl  33393  sibfof  34353  eulerpartgbij  34385  eulerpartlemmf  34388  eulerpartlemgh  34391  eulerpart  34395  fiblem  34411  orrvcval4  34478  cvmsss2  35318  opelco3  35819  poimirlem3  37671  poimirlem30  37698  mbfposadd  37715  itg2addnclem2  37720  ftc1anclem5  37745  ftc1anclem6  37746  pwfi2f1o  43137  brtrclfv2  43768  binomcxp  44398  fcoreslem1  47102  isubgr3stgrlem6  48010