Theorem imaeq2i 6060

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

Syntax hints:   = wceq 1570   “ cima 5664

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1825  ax-4 1839  ax-5 1940  ax-6 1997  ax-7 2038  ax-8 2145  ax-9 2153  ax-ext 2735

This theorem depends on definitions:  df-bi 210  df-an 401  df-or 861  df-3an 1105  df-tru 1573  df-fal 1583  df-ex 1810  df-sb 2097  df-clab 2742  df-cleq 2755  df-clel 2838  df-rab 3417  df-v 3457  df-dif 3908  df-un 3910  df-in 3912  df-ss 3922  df-nul 4287  df-if 4488  df-sn 4590  df-pr 4592  df-op 4596  df-br 5110  df-opab 5174  df-xp 5667  df-cnv 5669  df-dm 5671  df-rn 5672  df-res 5673  df-ima 5674

This theorem is referenced by:  cnvimarndm  6085  dmco  6256  imain  6621  fnimapr  6964  fnimatpd  6965  ssimaex  6966  intpreima  7065  resfunexg  7213  imauni  7244  isoini2  7337  fsuppeq  8167  fsuppeqg  8168  naddasslem1  8677  naddasslem2  8678  uniqs  8767  pwfilem  9273  fiint  9282  jech9.3  9782  infxpenlem  9993  hsmexlem4  10408  fcdmnn0supp  12556  fcdmnn0fsupp  12557  fcdmnn0suppg  12558  hashkf  14364  ghmeqker  19308  gsumval3lem1  19970  gsumval3lem2  19971  islinds2  21963  lindsind2  21969  mhpmulcl  22312  snclseqg  24273  retopbas  24917  ismbf3d  25813  i1fima  25837  i1fd  25840  itg1addlem5  25859  limciun  26053  plyeq0  26368  bday0  28004  bday1  28007  madeval2  28026  old1  28058  madeoldsuc  28078  bdayiun  28108  neg0s  28219  neg1s  28220  negbdaylem  28249  oncutlt  28457  oniso  28464  bdayons  28469  n0bday  28545  bdayn0p1  28562  spthispth  30073  0pth  30476  1pthdlem2  30487  eupth2lemb  30588  htth  31270  fcoinver  32949  ffs2  33072  ffsrn  33073  tocyccntz  33464  elrspunidl  33736  sibfof  34730  eulerpartgbij  34762  eulerpartlemmf  34765  eulerpartlemgh  34768  eulerpart  34772  fiblem  34788  orrvcval4  34855  cvmsss2  35766  opelco3  36267  poimirlem3  38274  poimirlem30  38301  mbfposadd  38318  itg2addnclem2  38323  ftc1anclem5  38348  ftc1anclem6  38349  pwfi2f1o  43823  brtrclfv2  44453  binomcxp  45067  fcoreslem1  47800  isubgr3stgrlem6  48736