Theorem imaeq2i 6056

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

Syntax hints:   = wceq 1542   “ cima 5679

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1798  ax-4 1812  ax-5 1914  ax-6 1972  ax-7 2012  ax-8 2109  ax-9 2117  ax-ext 2704

This theorem depends on definitions:  df-bi 206  df-an 398  df-or 847  df-3an 1090  df-tru 1545  df-fal 1555  df-ex 1783  df-sb 2069  df-clab 2711  df-cleq 2725  df-clel 2811  df-rab 3434  df-v 3477  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  6079  dmco  6251  imain  6631  fnimapr  6973  ssimaex  6974  intpreima  7069  resfunexg  7214  imauni  7242  isoini2  7333  fsuppeq  8157  fsuppeqg  8158  naddasslem1  8690  naddasslem2  8691  uniqs  8768  pwfilem  9174  fiint  9321  jech9.3  9806  infxpenlem  10005  hsmexlem4  10421  fcdmnn0supp  12525  fcdmnn0fsupp  12526  fcdmnn0suppg  12527  hashkf  14289  ghmeqker  19114  gsumval3lem1  19768  gsumval3lem2  19769  islinds2  21360  lindsind2  21366  mhpmulcl  21684  snclseqg  23612  retopbas  24269  ismbf3d  25163  i1fima  25187  i1fd  25190  itg1addlem5  25210  limciun  25403  plyeq0  25717  bday0s  27319  bday1s  27322  madeval2  27338  old1  27360  madeoldsuc  27369  negs0s  27491  negsbdaylem  27520  spthispth  28973  0pth  29368  1pthdlem2  29379  eupth2lemb  29480  htth  30159  fcoinver  31823  fnimatp  31890  ffs2  31941  ffsrn  31942  tocyccntz  32291  elrspunidl  32535  sibfof  33328  eulerpartgbij  33360  eulerpartlemmf  33363  eulerpartlemgh  33366  eulerpart  33370  fiblem  33386  orrvcval4  33452  cvmsss2  34254  opelco3  34735  poimirlem3  36480  poimirlem30  36507  mbfposadd  36524  itg2addnclem2  36529  ftc1anclem5  36554  ftc1anclem6  36555  uniqsALTV  37187  pwfi2f1o  41824  brtrclfv2  42464  binomcxp  43102  fcoreslem1  45760