Theorem imaeq2i 6057

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

Syntax hints:   = wceq 1540   “ cima 5679

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1796  ax-4 1810  ax-5 1912  ax-6 1970  ax-7 2010  ax-8 2107  ax-9 2115  ax-ext 2702

This theorem depends on definitions:  df-bi 206  df-an 396  df-or 845  df-3an 1088  df-tru 1543  df-fal 1553  df-ex 1781  df-sb 2067  df-clab 2709  df-cleq 2723  df-clel 2809  df-rab 3432  df-v 3475  df-dif 3951  df-un 3953  df-in 3955  df-ss 3965  df-nul 4323  df-if 4529  df-sn 4629  df-pr 4631  df-op 4635  df-br 5149  df-opab 5211  df-xp 5682  df-cnv 5684  df-dm 5686  df-rn 5687  df-res 5688  df-ima 5689

This theorem is referenced by:  cnvimarndm  6081  dmco  6253  imain  6633  fnimapr  6975  ssimaex  6976  intpreima  7071  resfunexg  7219  imauni  7248  isoini2  7339  fsuppeq  8165  fsuppeqg  8166  naddasslem1  8699  naddasslem2  8700  uniqs  8777  pwfilem  9183  fiint  9330  jech9.3  9815  infxpenlem  10014  hsmexlem4  10430  fcdmnn0supp  12535  fcdmnn0fsupp  12536  fcdmnn0suppg  12537  hashkf  14299  ghmeqker  19164  gsumval3lem1  19821  gsumval3lem2  19822  islinds2  21679  lindsind2  21685  mhpmulcl  22002  snclseqg  23941  retopbas  24598  ismbf3d  25504  i1fima  25528  i1fd  25531  itg1addlem5  25551  limciun  25744  plyeq0  26064  bday0s  27676  bday1s  27679  madeval2  27695  old1  27717  madeoldsuc  27726  negs0s  27854  negsbdaylem  27883  spthispth  29418  0pth  29813  1pthdlem2  29824  eupth2lemb  29925  htth  30606  fcoinver  32270  fnimatp  32337  ffs2  32388  ffsrn  32389  tocyccntz  32741  elrspunidl  32988  sibfof  33805  eulerpartgbij  33837  eulerpartlemmf  33840  eulerpartlemgh  33843  eulerpart  33847  fiblem  33863  orrvcval4  33929  cvmsss2  34731  opelco3  35218  poimirlem3  36958  poimirlem30  36985  mbfposadd  37002  itg2addnclem2  37007  ftc1anclem5  37032  ftc1anclem6  37033  uniqsALTV  37665  pwfi2f1o  42304  brtrclfv2  42944  binomcxp  43582  fcoreslem1  46235