Theorem imaeq2i 5964

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

Syntax hints:   = wceq 1541   “ cima 5591

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1801  ax-4 1815  ax-5 1916  ax-6 1974  ax-7 2014  ax-8 2111  ax-9 2119  ax-ext 2710

This theorem depends on definitions:  df-bi 206  df-an 396  df-or 844  df-3an 1087  df-tru 1544  df-fal 1554  df-ex 1786  df-sb 2071  df-clab 2717  df-cleq 2731  df-clel 2817  df-rab 3074  df-v 3432  df-dif 3894  df-un 3896  df-in 3898  df-ss 3908  df-nul 4262  df-if 4465  df-sn 4567  df-pr 4569  df-op 4573  df-br 5079  df-opab 5141  df-xp 5594  df-cnv 5596  df-dm 5598  df-rn 5599  df-res 5600  df-ima 5601

This theorem is referenced by:  cnvimarndm  5987  dmco  6155  imain  6515  fnimapr  6846  ssimaex  6847  intpreima  6941  resfunexg  7085  imauni  7113  isoini2  7203  frnsuppeq  7975  frnsuppeqg  7976  uniqs  8540  pwfilem  8925  fiint  9052  jech9.3  9556  infxpenlem  9753  hsmexlem4  10169  frnnn0supp  12272  frnnn0fsupp  12273  frnnn0suppg  12274  hashkf  14027  ghmeqker  18842  gsumval3lem1  19487  gsumval3lem2  19488  islinds2  21001  lindsind2  21007  mhpmulcl  21320  snclseqg  23248  retopbas  23905  ismbf3d  24799  i1fima  24823  i1fd  24826  itg1addlem5  24846  limciun  25039  plyeq0  25353  spthispth  28073  0pth  28468  1pthdlem2  28479  eupth2lemb  28580  htth  29259  fcoinver  30925  fnimatp  30993  ffs2  31042  ffsrn  31043  tocyccntz  31390  elrspunidl  31585  sibfof  32286  eulerpartgbij  32318  eulerpartlemmf  32321  eulerpartlemgh  32324  eulerpart  32328  fiblem  32344  orrvcval4  32410  cvmsss2  33215  opelco3  33728  bday0s  34001  bday1s  34004  madeval2  34016  madeoldsuc  34046  negs0s  34103  poimirlem3  35759  poimirlem30  35786  mbfposadd  35803  itg2addnclem2  35808  ftc1anclem5  35833  ftc1anclem6  35834  uniqsALTV  36443  pwfi2f1o  40901  brtrclfv2  41288  binomcxp  41928  fcoreslem1  44508