Theorem imaeq2i 6087

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

Syntax hints:   = wceq 1537   “ cima 5703

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1793  ax-4 1807  ax-5 1909  ax-6 1967  ax-7 2007  ax-8 2110  ax-9 2118  ax-ext 2711

This theorem depends on definitions:  df-bi 207  df-an 396  df-or 847  df-3an 1089  df-tru 1540  df-fal 1550  df-ex 1778  df-sb 2065  df-clab 2718  df-cleq 2732  df-clel 2819  df-rab 3444  df-v 3490  df-dif 3979  df-un 3981  df-in 3983  df-ss 3993  df-nul 4353  df-if 4549  df-sn 4649  df-pr 4651  df-op 4655  df-br 5167  df-opab 5229  df-xp 5706  df-cnv 5708  df-dm 5710  df-rn 5711  df-res 5712  df-ima 5713

This theorem is referenced by:  cnvimarndm  6112  dmco  6285  imain  6663  fnimapr  7005  fnimatpd  7006  ssimaex  7007  intpreima  7103  resfunexg  7252  imauni  7283  isoini2  7375  fsuppeq  8216  fsuppeqg  8217  naddasslem1  8750  naddasslem2  8751  uniqs  8835  pwfilem  9384  fiint  9394  fiintOLD  9395  jech9.3  9883  infxpenlem  10082  hsmexlem4  10498  fcdmnn0supp  12609  fcdmnn0fsupp  12610  fcdmnn0suppg  12611  hashkf  14381  ghmeqker  19283  gsumval3lem1  19947  gsumval3lem2  19948  islinds2  21856  lindsind2  21862  mhpmulcl  22176  snclseqg  24145  retopbas  24802  ismbf3d  25708  i1fima  25732  i1fd  25735  itg1addlem5  25755  limciun  25949  plyeq0  26270  bday0s  27891  bday1s  27894  madeval2  27910  old1  27932  madeoldsuc  27941  negs0s  28076  negs1s  28077  negsbdaylem  28106  n0sbday  28372  spthispth  29762  0pth  30157  1pthdlem2  30168  eupth2lemb  30269  htth  30950  fcoinver  32626  ffs2  32742  ffsrn  32743  tocyccntz  33137  elrspunidl  33421  sibfof  34305  eulerpartgbij  34337  eulerpartlemmf  34340  eulerpartlemgh  34343  eulerpart  34347  fiblem  34363  orrvcval4  34429  cvmsss2  35242  opelco3  35738  poimirlem3  37583  poimirlem30  37610  mbfposadd  37627  itg2addnclem2  37632  ftc1anclem5  37657  ftc1anclem6  37658  uniqsALTV  38285  pwfi2f1o  43053  brtrclfv2  43689  binomcxp  44326  fcoreslem1  46978