Theorem imaeq2i 6062

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

This proof depends on syntax axioms:   = wceq 1570   “ cima 5666

This proof depends on axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1828  ax-4 1842  ax-5 1943  ax-6 2000  ax-7 2041  ax-8 2148  ax-9 2156  ax-ext 2737

This proof depends on definitions:  df-bi 210  df-an 402  df-or 862  df-3an 1105  df-tru 1573  df-fal 1583  df-ex 1813  df-sb 2100  df-clab 2744  df-cleq 2757  df-clel 2840  df-rab 3419  df-v 3459  df-dif 3909  df-un 3911  df-in 3913  df-ss 3923  df-nul 4287  df-if 4490  df-sn 4592  df-pr 4594  df-op 4598  df-br 5112  df-opab 5176  df-xp 5669  df-cnv 5671  df-dm 5673  df-rn 5674  df-res 5675  df-ima 5676

This theorem is used by:  cnvimarndm  6087  dmco  6258  imain  6625  fnimapr  6968  fnimatpd  6969  ssimaex  6970  intpreima  7069  resfunexg  7220  imauni  7249  isoini2  7346  fsuppeq  8177  fsuppeqg  8178  naddasslem1  8687  naddasslem2  8688  uniqs  8777  pwfilem  9284  fiint  9293  jech9.3  9793  infxpenlem  10013  hsmexlem4  10428  fcdmnn0supp  12576  fcdmnn0fsupp  12577  fcdmnn0suppg  12578  hashkf  14386  ghmeqker  19357  gsumval3lem1  20019  gsumval3lem2  20020  islinds2  22013  lindsind2  22019  mhpmulcl  22362  snclseqg  24324  retopbas  24968  ismbf3d  25864  i1fima  25888  i1fd  25891  itg1addlem5  25910  limciun  26104  plyeq0  26419  bday0  28055  bday1  28058  madeval2  28077  old1  28109  madeoldsuc  28129  bdayiun  28159  neg0s  28270  neg1s  28271  negbdaylem  28300  oncutlt  28508  oniso  28515  bdayons  28520  n0bday  28596  bdayn0p1  28613  spthispth  30136  0pth  30543  1pthdlem2  30554  eupth2lemb  30659  htth  31341  fcoinver  33020  ffs2  33142  ffsrn  33143  tocyccntz  33528  elrspunidl  33800  sibfof  34795  eulerpartgbij  34827  eulerpartlemmf  34830  eulerpartlemgh  34833  eulerpart  34837  fiblem  34853  orrvcval4  34920  cvmsss2  35803  opelco3  36304  poimirlem3  38331  poimirlem30  38358  mbfposadd  38375  itg2addnclem2  38380  ftc1anclem5  38405  ftc1anclem6  38406  pwfi2f1o  43881  brtrclfv2  44511  binomcxp  45125  fcoreslem1  47858  isubgr3stgrlem6  48794