Theorem imaeq2i 6045

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

Syntax hints:   = wceq 1540   “ cima 5657

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 2707

This theorem depends on definitions:  df-bi 207  df-an 396  df-or 848  df-3an 1088  df-tru 1543  df-fal 1553  df-ex 1780  df-sb 2065  df-clab 2714  df-cleq 2727  df-clel 2809  df-rab 3416  df-v 3461  df-dif 3929  df-un 3931  df-in 3933  df-ss 3943  df-nul 4309  df-if 4501  df-sn 4602  df-pr 4604  df-op 4608  df-br 5120  df-opab 5182  df-xp 5660  df-cnv 5662  df-dm 5664  df-rn 5665  df-res 5666  df-ima 5667

This theorem is referenced by:  cnvimarndm  6070  dmco  6243  imain  6620  fnimapr  6961  fnimatpd  6962  ssimaex  6963  intpreima  7059  resfunexg  7206  imauni  7237  isoini2  7331  fsuppeq  8172  fsuppeqg  8173  naddasslem1  8704  naddasslem2  8705  uniqs  8789  pwfilem  9326  fiint  9336  fiintOLD  9337  jech9.3  9826  infxpenlem  10025  hsmexlem4  10441  fcdmnn0supp  12556  fcdmnn0fsupp  12557  fcdmnn0suppg  12558  hashkf  14348  ghmeqker  19224  gsumval3lem1  19884  gsumval3lem2  19885  islinds2  21771  lindsind2  21777  mhpmulcl  22085  snclseqg  24052  retopbas  24697  ismbf3d  25605  i1fima  25629  i1fd  25632  itg1addlem5  25651  limciun  25845  plyeq0  26166  bday0s  27790  bday1s  27793  madeval2  27809  old1  27831  madeoldsuc  27840  negs0s  27975  negs1s  27976  negsbdaylem  28005  n0sbday  28271  spthispth  29652  0pth  30052  1pthdlem2  30063  eupth2lemb  30164  htth  30845  fcoinver  32531  ffs2  32651  ffsrn  32652  tocyccntz  33101  elrspunidl  33389  sibfof  34318  eulerpartgbij  34350  eulerpartlemmf  34353  eulerpartlemgh  34356  eulerpart  34360  fiblem  34376  orrvcval4  34443  cvmsss2  35242  opelco3  35738  poimirlem3  37593  poimirlem30  37620  mbfposadd  37637  itg2addnclem2  37642  ftc1anclem5  37667  ftc1anclem6  37668  uniqsALTV  38293  pwfi2f1o  43067  brtrclfv2  43698  binomcxp  44329  fcoreslem1  47040  isubgr3stgrlem6  47931