Theorem imaeq2i 6077

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

Syntax hints:   = wceq 1536   “ cima 5691

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1791  ax-4 1805  ax-5 1907  ax-6 1964  ax-7 2004  ax-8 2107  ax-9 2115  ax-ext 2705

This theorem depends on definitions:  df-bi 207  df-an 396  df-or 848  df-3an 1088  df-tru 1539  df-fal 1549  df-ex 1776  df-sb 2062  df-clab 2712  df-cleq 2726  df-clel 2813  df-rab 3433  df-v 3479  df-dif 3965  df-un 3967  df-in 3969  df-ss 3979  df-nul 4339  df-if 4531  df-sn 4631  df-pr 4633  df-op 4637  df-br 5148  df-opab 5210  df-xp 5694  df-cnv 5696  df-dm 5698  df-rn 5699  df-res 5700  df-ima 5701

This theorem is referenced by:  cnvimarndm  6102  dmco  6275  imain  6652  fnimapr  6991  fnimatpd  6992  ssimaex  6993  intpreima  7089  resfunexg  7234  imauni  7265  isoini2  7358  fsuppeq  8198  fsuppeqg  8199  naddasslem1  8730  naddasslem2  8731  uniqs  8815  pwfilem  9353  fiint  9363  fiintOLD  9364  jech9.3  9851  infxpenlem  10050  hsmexlem4  10466  fcdmnn0supp  12580  fcdmnn0fsupp  12581  fcdmnn0suppg  12582  hashkf  14367  ghmeqker  19273  gsumval3lem1  19937  gsumval3lem2  19938  islinds2  21850  lindsind2  21856  mhpmulcl  22170  snclseqg  24139  retopbas  24796  ismbf3d  25702  i1fima  25726  i1fd  25729  itg1addlem5  25749  limciun  25943  plyeq0  26264  bday0s  27887  bday1s  27890  madeval2  27906  old1  27928  madeoldsuc  27937  negs0s  28072  negs1s  28073  negsbdaylem  28102  n0sbday  28368  spthispth  29758  0pth  30153  1pthdlem2  30164  eupth2lemb  30265  htth  30946  fcoinver  32623  ffs2  32745  ffsrn  32746  tocyccntz  33146  elrspunidl  33435  sibfof  34321  eulerpartgbij  34353  eulerpartlemmf  34356  eulerpartlemgh  34359  eulerpart  34363  fiblem  34379  orrvcval4  34445  cvmsss2  35258  opelco3  35755  poimirlem3  37609  poimirlem30  37636  mbfposadd  37653  itg2addnclem2  37658  ftc1anclem5  37683  ftc1anclem6  37684  uniqsALTV  38310  pwfi2f1o  43084  brtrclfv2  43716  binomcxp  44352  fcoreslem1  47012  isubgr3stgrlem6  47873