Theorem imaeq1i 6042

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 6040	. 2 ⊢ (𝐴 = 𝐵 → (𝐴 “ 𝐶) = (𝐵 “ 𝐶))
3	1, 2	ax-mp 5	1 ⊢ (𝐴 “ 𝐶) = (𝐵 “ 𝐶)

Syntax hints:   = wceq 1559   “ cima 5646

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1814  ax-4 1828  ax-5 1929  ax-6 1986  ax-7 2027  ax-8 2143  ax-9 2151  ax-ext 2733

This theorem depends on definitions:  df-bi 209  df-an 400  df-or 859  df-3an 1099  df-tru 1562  df-fal 1572  df-ex 1799  df-sb 2090  df-clab 2740  df-cleq 2753  df-clel 2836  df-rab 3414  df-v 3455  df-dif 3905  df-un 3907  df-in 3909  df-ss 3919  df-nul 4284  df-if 4478  df-sn 4580  df-pr 4582  df-op 4586  df-br 5098  df-opab 5160  df-cnv 5651  df-dm 5653  df-rn 5654  df-res 5655  df-ima 5656

This theorem is referenced by:  mptpreima  6220  csbpredg  6289  isarep2  6606  suppun  8158  suppco  8180  fsuppun  9327  fsuppcolem  9341  marypha2lem4  9378  dfoi  9453  r1limg  9723  isf34lem3  10326  compss  10327  fpwwe2lem12  10594  infrenegsup  12169  gsumzf1o  19943  ssidcn  23303  cnco  23314  qtopres  23746  idqtop  23754  qtopcn  23762  mbfid  25685  mbfres  25694  cncombf  25708  dvlog  26704  efopnlem2  26710  seqsval  28369  seqsfn  28390  seqsp1  28392  eucrct2eupth  30404  disjpreima  32744  imadifxp  32761  rinvf1o  32793  suppun2  32847  cyc3genpm  33293  elrgspnsubrunlem2  33390  esplysply  33829  vieta  33838  isconstr  33994  mbfmcst  34517  mbfmco  34522  sitmcl  34609  eulerpartlemt  34629  eulerpartlemmf  34633  eulerpart  34640  0rrv  34709  mclsppslem  35894  bj-iminvid  37648  mptsnun  37794  poimirlem3  38083  ftc1anclem3  38155  areacirclem5  38172  cytpval  43740  arearect  43753  brtrclfv2  44264  0cnf  46412  fourierdlem62  46703  smfco  47337