Theorem imaeq2i 5335

Description: Equality theorem for image. (Contributed by NM, 21-Dec-2008.)

Hypothesis

Ref	Expression
imaeq1i.1	|- A = B

Assertion

Ref	Expression
imaeq2i	|- ( C " A ) = ( C " B )

Proof of Theorem imaeq2i

Step	Hyp	Ref	Expression
1		imaeq1i.1	. 2 |- A = B
2		imaeq2 5333	. 2 |- ( A = B -> ( C " A ) = ( C " B ) )
3	1, 2	ax-mp 5	1 |- ( C " A ) = ( C " B )

Syntax hints:   = wceq 1379   "cima 5002

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1601  ax-4 1612  ax-5 1680  ax-6 1719  ax-7 1739  ax-10 1786  ax-11 1791  ax-12 1803  ax-13 1968  ax-ext 2445

This theorem depends on definitions:  df-bi 185  df-or 370  df-an 371  df-3an 975  df-tru 1382  df-ex 1597  df-nf 1600  df-sb 1712  df-clab 2453  df-cleq 2459  df-clel 2462  df-nfc 2617  df-rab 2823  df-v 3115  df-dif 3479  df-un 3481  df-in 3483  df-ss 3490  df-nul 3786  df-if 3940  df-sn 4028  df-pr 4030  df-op 4034  df-br 4448  df-opab 4506  df-xp 5005  df-cnv 5007  df-dm 5009  df-rn 5010  df-res 5011  df-ima 5012

This theorem is referenced by:  cnvimarndm  5358  dmco  5515  imain  5664  fnimapr  5931  ssimaex  5932  intpreima  6012  resfunexg  6126  imauni  6146  isoini2  6223  frnsuppeq  6913  imacosupp  6940  uniqs  7371  fiint  7797  cantnffvalOLD  8082  cantnfp1lem1OLD  8123  cantnfp1lem3OLD  8125  cantnflem1dOLD  8130  cantnflem1OLD  8131  mapfienOLD  8138  oef1oOLD  8142  cnfcom2lemOLD  8153  jech9.3  8232  infxpenlem  8391  hsmexlem4  8809  frnnn0supp  10849  nn0suppOLD  10850  hashkf  12375  ghmeqker  16098  gsumval3OLD  16711  gsumval3lem1  16712  gsumval3lem2  16713  islinds2  18643  lindsind2  18649  snclseqg  20377  retopbas  21030  ismbf3d  21824  i1fima  21848  i1fd  21851  itg1addlem5  21870  limciun  22061  plyeq0  22371  0pth  24276  2pthlem2  24302  constr3pthlem3  24361  htth  25539  fcoinver  27161  ffs2  27251  ffsrn  27252  sibfof  27950  eulerpartgbij  27979  eulerpartlemmf  27982  eulerpartlemgh  27985  eulerpart  27989  fiblem  28005  orrvcval4  28071  cvmsss2  28387  opelco3  28813  mbfposadd  29667  itg2addnclem2  29672  ftc1anclem5  29699  ftc1anclem6  29700  fsuppeq  30675  pwfi2f1o  30676