Theorem imaeq2i 6032

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

Syntax hints:   = wceq 1540   “ cima 5644

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 2702

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 2709  df-cleq 2722  df-clel 2804  df-rab 3409  df-v 3452  df-dif 3920  df-un 3922  df-in 3924  df-ss 3934  df-nul 4300  df-if 4492  df-sn 4593  df-pr 4595  df-op 4599  df-br 5111  df-opab 5173  df-xp 5647  df-cnv 5649  df-dm 5651  df-rn 5652  df-res 5653  df-ima 5654

This theorem is referenced by:  cnvimarndm  6057  dmco  6230  imain  6604  fnimapr  6947  fnimatpd  6948  ssimaex  6949  intpreima  7045  resfunexg  7192  imauni  7223  isoini2  7317  fsuppeq  8157  fsuppeqg  8158  naddasslem1  8661  naddasslem2  8662  uniqs  8750  pwfilem  9274  fiint  9284  fiintOLD  9285  jech9.3  9774  infxpenlem  9973  hsmexlem4  10389  fcdmnn0supp  12506  fcdmnn0fsupp  12507  fcdmnn0suppg  12508  hashkf  14304  ghmeqker  19182  gsumval3lem1  19842  gsumval3lem2  19843  islinds2  21729  lindsind2  21735  mhpmulcl  22043  snclseqg  24010  retopbas  24655  ismbf3d  25562  i1fima  25586  i1fd  25589  itg1addlem5  25608  limciun  25802  plyeq0  26123  bday0s  27747  bday1s  27750  madeval2  27768  old1  27794  madeoldsuc  27803  negs0s  27939  negs1s  27940  negsbdaylem  27969  onscutlt  28172  onsiso  28176  bdayon  28180  n0sbday  28251  bdayn0p1  28265  spthispth  29661  0pth  30061  1pthdlem2  30072  eupth2lemb  30173  htth  30854  fcoinver  32540  ffs2  32658  ffsrn  32659  tocyccntz  33108  elrspunidl  33406  sibfof  34338  eulerpartgbij  34370  eulerpartlemmf  34373  eulerpartlemgh  34376  eulerpart  34380  fiblem  34396  orrvcval4  34463  cvmsss2  35268  opelco3  35769  poimirlem3  37624  poimirlem30  37651  mbfposadd  37668  itg2addnclem2  37673  ftc1anclem5  37698  ftc1anclem6  37699  pwfi2f1o  43092  brtrclfv2  43723  binomcxp  44353  fcoreslem1  47068  isubgr3stgrlem6  47974