Theorem imaeq2i 6047

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

Syntax hints:   = wceq 1560   “ cima 5650

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1815  ax-4 1829  ax-5 1930  ax-6 1987  ax-7 2028  ax-8 2144  ax-9 2152  ax-ext 2734

This theorem depends on definitions:  df-bi 209  df-an 400  df-or 859  df-3an 1100  df-tru 1563  df-fal 1573  df-ex 1800  df-sb 2091  df-clab 2741  df-cleq 2754  df-clel 2837  df-rab 3415  df-v 3456  df-dif 3907  df-un 3909  df-in 3911  df-ss 3921  df-nul 4286  df-if 4481  df-sn 4583  df-pr 4585  df-op 4589  df-br 5101  df-opab 5163  df-xp 5653  df-cnv 5655  df-dm 5657  df-rn 5658  df-res 5659  df-ima 5660

This theorem is referenced by:  cnvimarndm  6072  dmco  6242  imain  6606  fnimapr  6950  fnimatpd  6951  ssimaex  6952  intpreima  7051  resfunexg  7199  imauni  7230  isoini2  7323  fsuppeq  8155  fsuppeqg  8156  naddasslem1  8665  naddasslem2  8666  uniqs  8755  pwfilem  9262  fiint  9271  jech9.3  9772  infxpenlem  9969  hsmexlem4  10386  fcdmnn0supp  12538  fcdmnn0fsupp  12539  fcdmnn0suppg  12540  hashkf  14345  ghmeqker  19283  gsumval3lem1  19945  gsumval3lem2  19946  islinds2  21865  lindsind2  21871  mhpmulcl  22214  snclseqg  24176  retopbas  24820  ismbf3d  25716  i1fima  25740  i1fd  25743  itg1addlem5  25762  limciun  25956  plyeq0  26271  bday0  27904  bday1  27907  madeval2  27926  old1  27958  madeoldsuc  27978  bdayiun  28008  neg0s  28119  neg1s  28120  negbdaylem  28149  oncutlt  28357  oniso  28364  bdayons  28369  n0bday  28445  bdayn0p1  28462  spthispth  29924  0pth  30327  1pthdlem2  30338  eupth2lemb  30439  htth  31121  fcoinver  32804  ffs2  32929  ffsrn  32930  tocyccntz  33324  elrspunidl  33614  sibfof  34637  eulerpartgbij  34669  eulerpartlemmf  34672  eulerpartlemgh  34675  eulerpart  34679  fiblem  34695  orrvcval4  34762  cvmsss2  35624  opelco3  36125  poimirlem3  38122  poimirlem30  38149  mbfposadd  38166  itg2addnclem2  38171  ftc1anclem5  38196  ftc1anclem6  38197  pwfi2f1o  43673  brtrclfv2  44303  binomcxp  44933  fcoreslem1  47657  isubgr3stgrlem6  48593