Theorem imaeq2i 5383

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

Syntax hints:   = wceq 1475   “ cima 5041

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1713  ax-4 1728  ax-5 1827  ax-6 1875  ax-7 1922  ax-10 2006  ax-11 2021  ax-12 2034  ax-13 2234  ax-ext 2590

This theorem depends on definitions:  df-bi 196  df-or 384  df-an 385  df-3an 1033  df-tru 1478  df-ex 1696  df-nf 1701  df-sb 1868  df-clab 2597  df-cleq 2603  df-clel 2606  df-nfc 2740  df-rab 2905  df-v 3175  df-dif 3543  df-un 3545  df-in 3547  df-ss 3554  df-nul 3875  df-if 4037  df-sn 4126  df-pr 4128  df-op 4132  df-br 4584  df-opab 4644  df-xp 5044  df-cnv 5046  df-dm 5048  df-rn 5049  df-res 5050  df-ima 5051

This theorem is referenced by:  cnvimarndm  5405  dmco  5560  imain  5888  fnimapr  6172  ssimaex  6173  intpreima  6254  resfunexg  6384  imauni  6408  isoini2  6489  frnsuppeq  7194  imacosupp  7222  uniqs  7694  fiint  8122  jech9.3  8560  infxpenlem  8719  hsmexlem4  9134  frnnn0supp  11226  hashkf  12981  ghmeqker  17510  gsumval3lem1  18129  gsumval3lem2  18130  islinds2  19971  lindsind2  19977  snclseqg  21729  retopbas  22374  ismbf3d  23227  i1fima  23251  i1fd  23254  itg1addlem5  23273  limciun  23464  plyeq0  23771  0pth  26100  2pthlem2  26126  constr3pthlem3  26185  htth  27159  fcoinver  28798  ffs2  28891  ffsrn  28892  sibfof  29729  eulerpartgbij  29761  eulerpartlemmf  29764  eulerpartlemgh  29767  eulerpart  29771  fiblem  29787  orrvcval4  29853  cvmsss2  30510  opelco3  30923  poimirlem3  32582  poimirlem30  32609  mbfposadd  32627  itg2addnclem2  32632  ftc1anclem5  32659  ftc1anclem6  32660  pwfi2f1o  36684  brtrclfv2  37038  binomcxp  37578  sPthisPth  40932  0pth-av  41293  1pthdlem2  41303  eupth2lemb  41405