Theorem imaeq1i 6016

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

Syntax hints:   = wceq 1541   “ cima 5627

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1796  ax-4 1810  ax-5 1911  ax-6 1968  ax-7 2009  ax-8 2115  ax-9 2123  ax-ext 2708

This theorem depends on definitions:  df-bi 207  df-an 396  df-or 848  df-3an 1088  df-tru 1544  df-fal 1554  df-ex 1781  df-sb 2068  df-clab 2715  df-cleq 2728  df-clel 2811  df-rab 3400  df-v 3442  df-dif 3904  df-un 3906  df-in 3908  df-ss 3918  df-nul 4286  df-if 4480  df-sn 4581  df-pr 4583  df-op 4587  df-br 5099  df-opab 5161  df-cnv 5632  df-dm 5634  df-rn 5635  df-res 5636  df-ima 5637

This theorem is referenced by:  mptpreima  6196  csbpredg  6265  isarep2  6582  suppun  8126  suppco  8148  fsuppun  9290  fsuppcolem  9304  marypha2lem4  9341  dfoi  9416  r1limg  9683  isf34lem3  10285  compss  10286  fpwwe2lem12  10553  infrenegsup  12125  gsumzf1o  19841  ssidcn  23199  cnco  23210  qtopres  23642  idqtop  23650  qtopcn  23658  mbfid  25592  mbfres  25601  cncombf  25615  dvlog  26616  efopnlem2  26622  seqsval  28284  seqsfn  28305  seqsp1  28307  eucrct2eupth  30320  disjpreima  32659  imadifxp  32676  rinvf1o  32708  suppun2  32763  cyc3genpm  33234  elrgspnsubrunlem2  33330  esplysply  33729  vieta  33736  isconstr  33893  mbfmcst  34416  mbfmco  34421  sitmcl  34508  eulerpartlemt  34528  eulerpartlemmf  34532  eulerpart  34539  0rrv  34608  mclsppslem  35777  bj-iminvid  37400  mptsnun  37544  poimirlem3  37824  ftc1anclem3  37896  areacirclem5  37913  cytpval  43444  arearect  43457  brtrclfv2  43968  0cnf  46121  fourierdlem62  46412  smfco  47046