Theorem imaeq1i 5463

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

Hypothesis

Ref	Expression
imaeq1i.1	|- A = B

Assertion

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

Proof of Theorem imaeq1i

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

Syntax hints:   = wceq 1483   "cima 5117

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1722  ax-4 1737  ax-5 1839  ax-6 1888  ax-7 1935  ax-9 1999  ax-10 2019  ax-11 2034  ax-12 2047  ax-13 2246  ax-ext 2602

This theorem depends on definitions:  df-bi 197  df-or 385  df-an 386  df-3an 1039  df-tru 1486  df-ex 1705  df-nf 1710  df-sb 1881  df-clab 2609  df-cleq 2615  df-clel 2618  df-nfc 2753  df-rab 2921  df-v 3202  df-dif 3577  df-un 3579  df-in 3581  df-ss 3588  df-nul 3916  df-if 4087  df-sn 4178  df-pr 4180  df-op 4184  df-br 4654  df-opab 4713  df-cnv 5122  df-dm 5124  df-rn 5125  df-res 5126  df-ima 5127

This theorem is referenced by:  mptpreima  5628  isarep2  5978  suppun  7315  supp0cosupp0  7334  imacosupp  7335  fsuppun  8294  fsuppcolem  8306  marypha2lem4  8344  dfoi  8416  r1limg  8634  isf34lem3  9197  compss  9198  fpwwe2lem13  9464  infrenegsup  11006  gsumzf1o  18313  ssidcn  21059  cnco  21070  qtopres  21501  idqtop  21509  qtopcn  21517  mbfid  23403  mbfres  23411  cncombf  23425  dvlog  24397  efopnlem2  24403  eucrct2eupth  27105  disjpreima  29397  imadifxp  29414  rinvf1o  29432  mbfmcst  30321  mbfmco  30326  sitmcl  30413  eulerpartlemt  30433  eulerpartlemmf  30437  eulerpart  30444  0rrv  30513  mclsppslem  31480  csbpredg  33172  mptsnun  33186  poimirlem3  33412  ftc1anclem3  33487  areacirclem5  33504  cytpval  37787  arearect  37801  brtrclfv2  38019  0cnf  40090  mbf0  40173  fourierdlem62  40385  smfco  41009