Theorem imaeq2i 5172

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

Syntax hints:   = wceq 1369   "cima 4848

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1591  ax-4 1602  ax-5 1670  ax-6 1708  ax-7 1728  ax-10 1775  ax-11 1780  ax-12 1792  ax-13 1943  ax-ext 2423

This theorem depends on definitions:  df-bi 185  df-or 370  df-an 371  df-3an 967  df-tru 1372  df-ex 1587  df-nf 1590  df-sb 1701  df-clab 2430  df-cleq 2436  df-clel 2439  df-nfc 2573  df-rab 2729  df-v 2979  df-dif 3336  df-un 3338  df-in 3340  df-ss 3347  df-nul 3643  df-if 3797  df-sn 3883  df-pr 3885  df-op 3889  df-br 4298  df-opab 4356  df-xp 4851  df-cnv 4853  df-dm 4855  df-rn 4856  df-res 4857  df-ima 4858

This theorem is referenced by:  cnvimarndm  5195  dmco  5351  imain  5499  fnimapr  5760  ssimaex  5761  intpreima  5839  resfunexg  5948  imauni  5968  isoini2  6035  frnsuppeq  6707  imacosupp  6734  uniqs  7165  fiint  7593  cantnffvalOLD  7876  cantnfp1lem1OLD  7917  cantnfp1lem3OLD  7919  cantnflem1dOLD  7924  cantnflem1OLD  7925  mapfienOLD  7932  oef1oOLD  7936  cnfcom2lemOLD  7947  jech9.3  8026  infxpenlem  8185  hsmexlem4  8603  frnnn0supp  10638  nn0suppOLD  10639  hashkf  12110  ghmeqker  15778  gsumval3OLD  16387  gsumval3lem1  16388  gsumval3lem2  16389  islinds2  18247  lindsind2  18253  snclseqg  19691  retopbas  20344  ismbf3d  21137  i1fima  21161  i1fd  21164  itg1addlem5  21183  limciun  21374  plyeq0  21684  0pth  23474  2pthlem2  23500  constr3pthlem3  23548  htth  24325  ffs2  26033  ffsrn  26034  sibfof  26731  eulerpartgbij  26760  eulerpartlemmf  26763  eulerpartlemgh  26766  eulerpart  26770  fiblem  26786  orrvcval4  26852  cvmsss2  27168  opelco3  27594  mbfposadd  28444  itg2addnclem2  28449  ftc1anclem5  28476  ftc1anclem6  28477  fsuppeq  29455  pwfi2f1o  29456