Theorem imaeq2i 6025

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

Syntax hints:   = wceq 1542   “ cima 5635

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 3402  df-v 3444  df-dif 3906  df-un 3908  df-in 3910  df-ss 3920  df-nul 4288  df-if 4482  df-sn 4583  df-pr 4585  df-op 4589  df-br 5101  df-opab 5163  df-xp 5638  df-cnv 5640  df-dm 5642  df-rn 5643  df-res 5644  df-ima 5645

This theorem is referenced by:  cnvimarndm  6050  dmco  6221  imain  6585  fnimapr  6925  fnimatpd  6926  ssimaex  6927  intpreima  7024  resfunexg  7171  imauni  7202  isoini2  7295  fsuppeq  8127  fsuppeqg  8128  naddasslem1  8632  naddasslem2  8633  uniqs  8722  pwfilem  9230  fiint  9239  jech9.3  9738  infxpenlem  9935  hsmexlem4  10351  fcdmnn0supp  12470  fcdmnn0fsupp  12471  fcdmnn0suppg  12472  hashkf  14267  ghmeqker  19184  gsumval3lem1  19846  gsumval3lem2  19847  islinds2  21780  lindsind2  21786  mhpmulcl  22104  snclseqg  24072  retopbas  24716  ismbf3d  25623  i1fima  25647  i1fd  25650  itg1addlem5  25669  limciun  25863  plyeq0  26184  bday0  27819  bday1  27822  madeval2  27841  old1  27873  madeoldsuc  27893  bdayiun  27923  neg0s  28034  neg1s  28035  negbdaylem  28064  oncutlt  28272  oniso  28279  bdayons  28284  n0bday  28360  bdayn0p1  28377  spthispth  29809  0pth  30212  1pthdlem2  30223  eupth2lemb  30324  htth  31006  fcoinver  32691  ffs2  32817  ffsrn  32818  tocyccntz  33238  elrspunidl  33521  sibfof  34518  eulerpartgbij  34550  eulerpartlemmf  34553  eulerpartlemgh  34556  eulerpart  34560  fiblem  34576  orrvcval4  34643  cvmsss2  35490  opelco3  35991  poimirlem3  37874  poimirlem30  37901  mbfposadd  37918  itg2addnclem2  37923  ftc1anclem5  37948  ftc1anclem6  37949  pwfi2f1o  43453  brtrclfv2  44083  binomcxp  44713  fcoreslem1  47423  isubgr3stgrlem6  48331