Theorem imaeq1i 6031

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

Syntax hints:   = wceq 1540   “ cima 5644

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1795  ax-4 1809  ax-5 1910  ax-6 1967  ax-7 2008  ax-8 2111  ax-9 2119  ax-ext 2702

This theorem depends on definitions:  df-bi 207  df-an 396  df-or 848  df-3an 1088  df-tru 1543  df-fal 1553  df-ex 1780  df-sb 2066  df-clab 2709  df-cleq 2722  df-clel 2804  df-rab 3409  df-v 3452  df-dif 3920  df-un 3922  df-in 3924  df-ss 3934  df-nul 4300  df-if 4492  df-sn 4593  df-pr 4595  df-op 4599  df-br 5111  df-opab 5173  df-cnv 5649  df-dm 5651  df-rn 5652  df-res 5653  df-ima 5654

This theorem is referenced by:  mptpreima  6214  csbpredg  6283  isarep2  6611  suppun  8166  suppco  8188  fsuppun  9345  fsuppcolem  9359  marypha2lem4  9396  dfoi  9471  r1limg  9731  isf34lem3  10335  compss  10336  fpwwe2lem12  10602  infrenegsup  12173  gsumzf1o  19849  ssidcn  23149  cnco  23160  qtopres  23592  idqtop  23600  qtopcn  23608  mbfid  25543  mbfres  25552  cncombf  25566  dvlog  26567  efopnlem2  26573  seqsval  28189  seqsfn  28210  seqsp1  28212  eucrct2eupth  30181  disjpreima  32520  imadifxp  32537  rinvf1o  32561  suppun2  32614  cyc3genpm  33116  elrgspnsubrunlem2  33206  isconstr  33733  mbfmcst  34257  mbfmco  34262  sitmcl  34349  eulerpartlemt  34369  eulerpartlemmf  34373  eulerpart  34380  0rrv  34449  mclsppslem  35577  bj-iminvid  37190  mptsnun  37334  poimirlem3  37624  ftc1anclem3  37696  areacirclem5  37713  cytpval  43198  arearect  43211  brtrclfv2  43723  0cnf  45882  fourierdlem62  46173  smfco  46807