Theorem imaeq2i 6018

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

Syntax hints:   = wceq 1542   “ cima 5628

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 3391  df-v 3432  df-dif 3893  df-un 3895  df-in 3897  df-ss 3907  df-nul 4275  df-if 4468  df-sn 4569  df-pr 4571  df-op 4575  df-br 5087  df-opab 5149  df-xp 5631  df-cnv 5633  df-dm 5635  df-rn 5636  df-res 5637  df-ima 5638

This theorem is referenced by:  cnvimarndm  6043  dmco  6214  imain  6578  fnimapr  6918  fnimatpd  6919  ssimaex  6920  intpreima  7017  resfunexg  7164  imauni  7195  isoini2  7288  fsuppeq  8119  fsuppeqg  8120  naddasslem1  8624  naddasslem2  8625  uniqs  8714  pwfilem  9222  fiint  9231  jech9.3  9732  infxpenlem  9929  hsmexlem4  10345  fcdmnn0supp  12488  fcdmnn0fsupp  12489  fcdmnn0suppg  12490  hashkf  14288  ghmeqker  19212  gsumval3lem1  19874  gsumval3lem2  19875  islinds2  21806  lindsind2  21812  mhpmulcl  22128  snclseqg  24094  retopbas  24738  ismbf3d  25634  i1fima  25658  i1fd  25661  itg1addlem5  25680  limciun  25874  plyeq0  26189  bday0  27820  bday1  27823  madeval2  27842  old1  27874  madeoldsuc  27894  bdayiun  27924  neg0s  28035  neg1s  28036  negbdaylem  28065  oncutlt  28273  oniso  28280  bdayons  28285  n0bday  28361  bdayn0p1  28378  spthispth  29810  0pth  30213  1pthdlem2  30224  eupth2lemb  30325  htth  31007  fcoinver  32692  ffs2  32818  ffsrn  32819  tocyccntz  33223  elrspunidl  33506  sibfof  34503  eulerpartgbij  34535  eulerpartlemmf  34538  eulerpartlemgh  34541  eulerpart  34545  fiblem  34561  orrvcval4  34628  cvmsss2  35475  opelco3  35976  poimirlem3  37961  poimirlem30  37988  mbfposadd  38005  itg2addnclem2  38010  ftc1anclem5  38035  ftc1anclem6  38036  pwfi2f1o  43545  brtrclfv2  44175  binomcxp  44805  fcoreslem1  47526  isubgr3stgrlem6  48462