Theorem imaeq2i 5977

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

Syntax hints:   = wceq 1539   “ cima 5603

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 1911  ax-6 1969  ax-7 2009  ax-8 2106  ax-9 2114  ax-ext 2707

This theorem depends on definitions:  df-bi 206  df-an 398  df-or 846  df-3an 1089  df-tru 1542  df-fal 1552  df-ex 1780  df-sb 2066  df-clab 2714  df-cleq 2728  df-clel 2814  df-rab 3287  df-v 3439  df-dif 3895  df-un 3897  df-in 3899  df-ss 3909  df-nul 4263  df-if 4466  df-sn 4566  df-pr 4568  df-op 4572  df-br 5082  df-opab 5144  df-xp 5606  df-cnv 5608  df-dm 5610  df-rn 5611  df-res 5612  df-ima 5613

This theorem is referenced by:  cnvimarndm  6000  dmco  6172  imain  6548  fnimapr  6884  ssimaex  6885  intpreima  6979  resfunexg  7123  imauni  7151  isoini2  7242  fsuppeq  8022  fsuppeqg  8023  uniqs  8597  pwfilem  8998  fiint  9135  jech9.3  9616  infxpenlem  9815  hsmexlem4  10231  fcdmnn0supp  12335  fcdmnn0fsupp  12336  fcdmnn0suppg  12337  hashkf  14092  ghmeqker  18906  gsumval3lem1  19551  gsumval3lem2  19552  islinds2  21065  lindsind2  21071  mhpmulcl  21384  snclseqg  23312  retopbas  23969  ismbf3d  24863  i1fima  24887  i1fd  24890  itg1addlem5  24910  limciun  25103  plyeq0  25417  spthispth  28139  0pth  28534  1pthdlem2  28545  eupth2lemb  28646  htth  29325  fcoinver  30991  fnimatp  31059  ffs2  31108  ffsrn  31109  tocyccntz  31456  elrspunidl  31651  sibfof  32352  eulerpartgbij  32384  eulerpartlemmf  32387  eulerpartlemgh  32390  eulerpart  32394  fiblem  32410  orrvcval4  32476  cvmsss2  33281  opelco3  33794  bday0s  34067  bday1s  34070  madeval2  34082  madeoldsuc  34112  negs0s  34169  poimirlem3  35824  poimirlem30  35851  mbfposadd  35868  itg2addnclem2  35873  ftc1anclem5  35898  ftc1anclem6  35899  uniqsALTV  36506  pwfi2f1o  40959  brtrclfv2  41373  binomcxp  42013  fcoreslem1  44615