Theorem imaeq2i 5143

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 5141	. 2 |- ( A = B -> ( C " A ) = ( C " B ) )
3	1, 2	ax-mp 5	1 |- ( C " A ) = ( C " B )

Syntax hints:   = wceq 1447   "cima 4814

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1672  ax-4 1685  ax-5 1761  ax-6 1808  ax-7 1854  ax-10 1918  ax-11 1923  ax-12 1936  ax-13 2091  ax-ext 2431

This theorem depends on definitions:  df-bi 190  df-or 376  df-an 377  df-3an 988  df-tru 1450  df-ex 1667  df-nf 1671  df-sb 1801  df-clab 2438  df-cleq 2444  df-clel 2447  df-nfc 2581  df-rab 2745  df-v 3014  df-dif 3374  df-un 3376  df-in 3378  df-ss 3385  df-nul 3699  df-if 3849  df-sn 3936  df-pr 3938  df-op 3942  df-br 4374  df-opab 4433  df-xp 4817  df-cnv 4819  df-dm 4821  df-rn 4822  df-res 4823  df-ima 4824

This theorem is referenced by:  cnvimarndm  5166  dmco  5321  imain  5640  fnimapr  5912  ssimaex  5913  intpreima  5994  resfunexg  6115  imauni  6136  isoini2  6215  frnsuppeq  6913  imacosupp  6942  uniqs  7409  fiint  7834  jech9.3  8271  infxpenlem  8430  hsmexlem4  8845  frnnn0supp  10912  hashkf  12510  ghmeqker  16919  gsumval3lem1  17549  gsumval3lem2  17550  islinds2  19381  lindsind2  19387  snclseqg  21140  retopbas  21791  ismbf3d  22621  i1fima  22647  i1fd  22650  itg1addlem5  22669  limciun  22860  plyeq0  23176  0pth  25311  2pthlem2  25337  constr3pthlem3  25396  htth  26582  fcoinver  28222  ffs2  28320  ffsrn  28321  sibfof  29178  eulerpartgbij  29210  eulerpartlemmf  29213  eulerpartlemgh  29216  eulerpart  29220  fiblem  29236  orrvcval4  29302  cvmsss2  30002  opelco3  30425  poimirlem3  31944  poimirlem30  31971  mbfposadd  31989  itg2addnclem2  31995  ftc1anclem5  32022  ftc1anclem6  32023  pwfi2f1o  35955  brtrclfv2  36320  binomcxp  36706  sPthisPth  39811  0pth-av  39892  1pthdlem2  39902