Theorem imaeq2i 6009

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

Syntax hints:   = wceq 1540   “ cima 5622

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 2008  ax-8 2111  ax-9 2119  ax-ext 2701

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 2066  df-clab 2708  df-cleq 2721  df-clel 2803  df-rab 3395  df-v 3438  df-dif 3906  df-un 3908  df-in 3910  df-ss 3920  df-nul 4285  df-if 4477  df-sn 4578  df-pr 4580  df-op 4584  df-br 5093  df-opab 5155  df-xp 5625  df-cnv 5627  df-dm 5629  df-rn 5630  df-res 5631  df-ima 5632

This theorem is referenced by:  cnvimarndm  6034  dmco  6203  imain  6567  fnimapr  6906  fnimatpd  6907  ssimaex  6908  intpreima  7004  resfunexg  7151  imauni  7182  isoini2  7276  fsuppeq  8108  fsuppeqg  8109  naddasslem1  8612  naddasslem2  8613  uniqs  8701  pwfilem  9207  fiint  9216  fiintOLD  9217  jech9.3  9710  infxpenlem  9907  hsmexlem4  10323  fcdmnn0supp  12441  fcdmnn0fsupp  12442  fcdmnn0suppg  12443  hashkf  14239  ghmeqker  19122  gsumval3lem1  19784  gsumval3lem2  19785  islinds2  21720  lindsind2  21726  mhpmulcl  22034  snclseqg  24001  retopbas  24646  ismbf3d  25553  i1fima  25577  i1fd  25580  itg1addlem5  25599  limciun  25793  plyeq0  26114  bday0s  27742  bday1s  27745  madeval2  27763  old1  27789  madeoldsuc  27799  bdayiun  27829  negs0s  27937  negs1s  27938  negsbdaylem  27967  onscutlt  28170  onsiso  28174  bdayon  28178  n0sbday  28249  bdayn0p1  28263  spthispth  29669  0pth  30069  1pthdlem2  30080  eupth2lemb  30181  htth  30862  fcoinver  32548  ffs2  32671  ffsrn  32672  tocyccntz  33086  elrspunidl  33365  sibfof  34308  eulerpartgbij  34340  eulerpartlemmf  34343  eulerpartlemgh  34346  eulerpart  34350  fiblem  34366  orrvcval4  34433  cvmsss2  35247  opelco3  35748  poimirlem3  37603  poimirlem30  37630  mbfposadd  37647  itg2addnclem2  37652  ftc1anclem5  37677  ftc1anclem6  37678  pwfi2f1o  43069  brtrclfv2  43700  binomcxp  44330  fcoreslem1  47047  isubgr3stgrlem6  47955