Theorem imaeq2i 6076

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

Syntax hints:   = wceq 1540   “ cima 5688

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1795  ax-4 1809  ax-5 1910  ax-6 1967  ax-7 2007  ax-8 2110  ax-9 2118  ax-ext 2708

This theorem depends on definitions:  df-bi 207  df-an 396  df-or 849  df-3an 1089  df-tru 1543  df-fal 1553  df-ex 1780  df-sb 2065  df-clab 2715  df-cleq 2729  df-clel 2816  df-rab 3437  df-v 3482  df-dif 3954  df-un 3956  df-in 3958  df-ss 3968  df-nul 4334  df-if 4526  df-sn 4627  df-pr 4629  df-op 4633  df-br 5144  df-opab 5206  df-xp 5691  df-cnv 5693  df-dm 5695  df-rn 5696  df-res 5697  df-ima 5698

This theorem is referenced by:  cnvimarndm  6101  dmco  6274  imain  6651  fnimapr  6992  fnimatpd  6993  ssimaex  6994  intpreima  7090  resfunexg  7235  imauni  7266  isoini2  7359  fsuppeq  8200  fsuppeqg  8201  naddasslem1  8732  naddasslem2  8733  uniqs  8817  pwfilem  9356  fiint  9366  fiintOLD  9367  jech9.3  9854  infxpenlem  10053  hsmexlem4  10469  fcdmnn0supp  12583  fcdmnn0fsupp  12584  fcdmnn0suppg  12585  hashkf  14371  ghmeqker  19261  gsumval3lem1  19923  gsumval3lem2  19924  islinds2  21833  lindsind2  21839  mhpmulcl  22153  snclseqg  24124  retopbas  24781  ismbf3d  25689  i1fima  25713  i1fd  25716  itg1addlem5  25735  limciun  25929  plyeq0  26250  bday0s  27873  bday1s  27876  madeval2  27892  old1  27914  madeoldsuc  27923  negs0s  28058  negs1s  28059  negsbdaylem  28088  n0sbday  28354  spthispth  29744  0pth  30144  1pthdlem2  30155  eupth2lemb  30256  htth  30937  fcoinver  32617  ffs2  32739  ffsrn  32740  tocyccntz  33164  elrspunidl  33456  sibfof  34342  eulerpartgbij  34374  eulerpartlemmf  34377  eulerpartlemgh  34380  eulerpart  34384  fiblem  34400  orrvcval4  34467  cvmsss2  35279  opelco3  35775  poimirlem3  37630  poimirlem30  37657  mbfposadd  37674  itg2addnclem2  37679  ftc1anclem5  37704  ftc1anclem6  37705  uniqsALTV  38330  pwfi2f1o  43108  brtrclfv2  43740  binomcxp  44376  fcoreslem1  47075  isubgr3stgrlem6  47938