Theorem imaeq2i 6061

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

Syntax hints:   = wceq 1567   “ cima 5665

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1822  ax-4 1836  ax-5 1937  ax-6 1994  ax-7 2035  ax-8 2151  ax-9 2159  ax-ext 2741

This theorem depends on definitions:  df-bi 210  df-an 401  df-or 861  df-3an 1103  df-tru 1570  df-fal 1580  df-ex 1807  df-sb 2098  df-clab 2748  df-cleq 2761  df-clel 2844  df-rab 3424  df-v 3465  df-dif 3916  df-un 3918  df-in 3920  df-ss 3930  df-nul 4295  df-if 4493  df-sn 4595  df-pr 4597  df-op 4601  df-br 5114  df-opab 5178  df-xp 5668  df-cnv 5670  df-dm 5672  df-rn 5673  df-res 5674  df-ima 5675

This theorem is referenced by:  cnvimarndm  6086  dmco  6257  imain  6622  fnimapr  6965  fnimatpd  6966  ssimaex  6967  intpreima  7066  resfunexg  7214  imauni  7245  isoini2  7338  fsuppeq  8170  fsuppeqg  8171  naddasslem1  8680  naddasslem2  8681  uniqs  8770  pwfilem  9276  fiint  9285  jech9.3  9785  infxpenlem  9996  hsmexlem4  10412  fcdmnn0supp  12560  fcdmnn0fsupp  12561  fcdmnn0suppg  12562  hashkf  14367  ghmeqker  19312  gsumval3lem1  19974  gsumval3lem2  19975  islinds2  21931  lindsind2  21937  mhpmulcl  22280  snclseqg  24241  retopbas  24885  ismbf3d  25781  i1fima  25805  i1fd  25808  itg1addlem5  25827  limciun  26021  plyeq0  26336  bday0  27969  bday1  27972  madeval2  27991  old1  28023  madeoldsuc  28043  bdayiun  28073  neg0s  28184  neg1s  28185  negbdaylem  28214  oncutlt  28422  oniso  28429  bdayons  28434  n0bday  28510  bdayn0p1  28527  spthispth  30013  0pth  30416  1pthdlem2  30427  eupth2lemb  30528  htth  31210  fcoinver  32889  ffs2  33012  ffsrn  33013  tocyccntz  33404  elrspunidl  33679  sibfof  34674  eulerpartgbij  34706  eulerpartlemmf  34709  eulerpartlemgh  34712  eulerpart  34716  fiblem  34732  orrvcval4  34799  cvmsss2  35664  opelco3  36165  poimirlem3  38161  poimirlem30  38188  mbfposadd  38205  itg2addnclem2  38210  ftc1anclem5  38235  ftc1anclem6  38236  pwfi2f1o  43714  brtrclfv2  44344  binomcxp  44958  fcoreslem1  47688  isubgr3stgrlem6  48624