Theorem imaeq2i 5899

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

Syntax hints:   = wceq 1538   “ cima 5527

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1797  ax-4 1811  ax-5 1911  ax-6 1970  ax-7 2015  ax-8 2113  ax-9 2121  ax-ext 2729

This theorem depends on definitions:  df-bi 210  df-an 400  df-or 845  df-3an 1086  df-tru 1541  df-ex 1782  df-sb 2070  df-clab 2736  df-cleq 2750  df-clel 2830  df-rab 3079  df-v 3411  df-un 3863  df-in 3865  df-ss 3875  df-sn 4523  df-pr 4525  df-op 4529  df-br 5033  df-opab 5095  df-xp 5530  df-cnv 5532  df-dm 5534  df-rn 5535  df-res 5536  df-ima 5537

This theorem is referenced by:  cnvimarndm  5922  dmco  6084  imain  6420  fnimapr  6736  ssimaex  6737  intpreima  6829  resfunexg  6969  imauni  6997  isoini2  7086  frnsuppeq  7849  frnsuppeqg  7850  imacosuppOLD  7885  uniqs  8367  pwfilem  8745  fiint  8828  jech9.3  9276  infxpenlem  9473  hsmexlem4  9889  frnnn0supp  11990  frnnn0fsupp  11991  frnnn0suppg  11992  hashkf  13742  ghmeqker  18452  gsumval3lem1  19093  gsumval3lem2  19094  islinds2  20578  lindsind2  20584  mhpmulcl  20892  snclseqg  22816  retopbas  23462  ismbf3d  24354  i1fima  24378  i1fd  24381  itg1addlem5  24400  limciun  24593  plyeq0  24907  spthispth  27614  0pth  28009  1pthdlem2  28020  eupth2lemb  28121  htth  28800  fcoinver  30468  fnimatp  30538  ffs2  30587  ffsrn  30588  tocyccntz  30937  elrspunidl  31127  sibfof  31826  eulerpartgbij  31858  eulerpartlemmf  31861  eulerpartlemgh  31864  eulerpart  31868  fiblem  31884  orrvcval4  31950  cvmsss2  32752  opelco3  33265  bday0s  33582  bday1s  33585  madeval2  33597  madeoldsuc  33624  negs0s  33672  poimirlem3  35340  poimirlem30  35367  mbfposadd  35384  itg2addnclem2  35389  ftc1anclem5  35414  ftc1anclem6  35415  uniqsALTV  36026  pwfi2f1o  40413  brtrclfv2  40801  binomcxp  41434