Theorem imaeq1i 6032

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

Hypothesis

Ref	Expression
imaeq1i.1	⊢ 𝐴 = 𝐵

Assertion

Ref	Expression
imaeq1i	⊢ (𝐴 “ 𝐶) = (𝐵 “ 𝐶)

Proof of Theorem imaeq1i

Step	Hyp	Ref	Expression
1		imaeq1i.1	. 2 ⊢ 𝐴 = 𝐵
2		imaeq1 6030	. 2 ⊢ (𝐴 = 𝐵 → (𝐴 “ 𝐶) = (𝐵 “ 𝐶))
3	1, 2	ax-mp 5	1 ⊢ (𝐴 “ 𝐶) = (𝐵 “ 𝐶)

Syntax hints:   = wceq 1550   “ cima 5639

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1805  ax-4 1819  ax-5 1920  ax-6 1977  ax-7 2018  ax-8 2134  ax-9 2142  ax-ext 2724

This theorem depends on definitions:  df-bi 209  df-an 399  df-or 857  df-3an 1097  df-tru 1553  df-fal 1563  df-ex 1790  df-sb 2081  df-clab 2731  df-cleq 2744  df-clel 2827  df-rab 3405  df-v 3446  df-dif 3898  df-un 3900  df-in 3902  df-ss 3912  df-nul 4277  df-if 4471  df-sn 4573  df-pr 4575  df-op 4579  df-br 5091  df-opab 5153  df-cnv 5644  df-dm 5646  df-rn 5647  df-res 5648  df-ima 5649

This theorem is referenced by:  mptpreima  6210  csbpredg  6279  isarep2  6596  suppun  8148  suppco  8170  fsuppun  9319  fsuppcolem  9333  marypha2lem4  9370  dfoi  9445  r1limg  9715  isf34lem3  10318  compss  10319  fpwwe2lem12  10586  infrenegsup  12161  gsumzf1o  19924  ssidcn  23284  cnco  23295  qtopres  23727  idqtop  23735  qtopcn  23743  mbfid  25666  mbfres  25675  cncombf  25689  dvlog  26682  efopnlem2  26688  seqsval  28347  seqsfn  28368  seqsp1  28370  eucrct2eupth  30382  disjpreima  32722  imadifxp  32739  rinvf1o  32771  suppun2  32825  cyc3genpm  33282  elrgspnsubrunlem2  33378  esplysply  33812  vieta  33821  isconstr  33977  mbfmcst  34500  mbfmco  34505  sitmcl  34592  eulerpartlemt  34612  eulerpartlemmf  34616  eulerpart  34623  0rrv  34692  mclsppslem  35871  bj-iminvid  37625  mptsnun  37771  poimirlem3  38060  ftc1anclem3  38132  areacirclem5  38149  cytpval  43717  arearect  43730  brtrclfv2  44241  0cnf  46389  fourierdlem62  46680  smfco  47314