Theorem imaeq1d 6018

Description: Equality theorem for image. (Contributed by FL, 15-Dec-2006.)

Hypothesis

Ref	Expression
imaeq1d.1	⊢ (𝜑 → 𝐴 = 𝐵)

Assertion

Ref	Expression
imaeq1d	⊢ (𝜑 → (𝐴 “ 𝐶) = (𝐵 “ 𝐶))

Proof of Theorem imaeq1d

Step	Hyp	Ref	Expression
1		imaeq1d.1	. 2 ⊢ (𝜑 → 𝐴 = 𝐵)
2		imaeq1 6014	. 2 ⊢ (𝐴 = 𝐵 → (𝐴 “ 𝐶) = (𝐵 “ 𝐶))
3	1, 2	syl 17	1 ⊢ (𝜑 → (𝐴 “ 𝐶) = (𝐵 “ 𝐶))

Syntax hints:   → wi 4   = 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:  imaeq12d  6020  nfimad  6028  csbrn  6161  f1imacnv  6790  foimacnv  6791  fimacnvinrn  7016  seqomeq12  8385  ssenen  9079  fipreima  9258  oieq1  9417  oieq2  9418  dfac12lem1  10054  dfac12r  10057  fpwwe2cbv  10541  fpwwe2lem2  10543  fpwwecbv  10555  fpwwelem  10556  seqeq1  13927  seqeq2  13928  seqeq3  13929  1arith  16855  vdwmc  16906  vdwnnlem1  16923  ramub2  16942  rami  16943  imasless  17461  gsumvalx  18601  eqglact  19108  eqg0subgecsn  19126  psgnunilem1  19422  evpmss  21541  psgnevpmb  21542  frlmup3  21755  psrbag  21873  psrbaglefi  21882  iscn  23179  ptbasfi  23525  ptval2  23545  ptrescn  23583  xkoptsub  23598  qtopval  23639  cmphaushmeo  23744  ptcmpg  24001  restutopopn  24182  prdsxmslem2  24473  metuval  24493  nghmfval  24666  isnghm  24667  ismbf1  25581  ismbf  25585  mbfconst  25590  mbfres2  25602  cncombf  25615  isi1f  25631  itg1val  25640  deg1val  26057  fta1glem2  26130  fta1g  26131  fta1b  26133  dgrval  26189  dgrlem  26190  coeidlem  26198  coe11  26214  fta1lem  26271  fta1  26272  vieta1lem2  26275  vieta1  26276  taylthlem2  26338  taylthlem2OLD  26339  areaval  26930  sqff1o  27148  seqseq123d  28282  nlfnval  31956  xppreima2  32729  ofpreima  32743  mptiffisupp  32772  fpwrelmapffslem  32811  indf1ofs  32948  evpmval  33227  altgnsg  33231  ply1dg3rt0irred  33665  vieta  33736  xrhval  34175  ismbfm  34408  mbfmcst  34416  issibf  34490  sitgfval  34498  eulerpartlemelr  34514  eulerpartleme  34520  eulerpartlemo  34522  eulerpartlemt0  34526  eulerpartlemt  34528  eulerpartlemr  34531  eulerpartlemgf  34536  eulerpartlemgs2  34537  eulerpartlemn  34538  eulerpart  34539  ballotlemscr  34676  ballotlemrv  34677  ballotlemrinv0  34690  iscvm  35453  cvmliftmolem1  35475  cvmlift2lem9a  35497  cvmlift2lem9  35505  msrfval  35731  ismfs  35743  mthmval  35769  bj-imdirval2  37388  bj-iminvval2  37399  poimirlem4  37825  poimirlem5  37826  poimirlem6  37827  poimirlem7  37828  poimirlem8  37829  poimirlem10  37831  poimirlem11  37832  poimirlem12  37833  poimirlem13  37834  poimirlem14  37835  poimirlem15  37836  poimirlem16  37837  poimirlem17  37838  poimirlem18  37839  poimirlem19  37840  poimirlem20  37841  poimirlem21  37842  poimirlem22  37843  poimirlem26  37847  poimirlem27  37848  poimirlem32  37853  cnambfre  37869  itg2addnclem2  37873  ftc1anclem1  37894  ftc1anclem6  37899  lkrval  39348  aks6d1c6lem4  42427  aks6d1c6lem5  42431  aks6d1c7lem3  42436  prjcrvfval  42874  prjcrvval  42875  prjcrv0  42876  pw2f1o2val  43281  aomclem8  43303  pwfi2f1o  43338  trclimalb2  43967  frege131d  44005  colleq12d  44494  dirkercncflem2  46348  issmflem  46971  smfpimioo  47031  smfpimcc  47052  smfsuplem2  47056  3f1oss1  47321  imaidfu2lem  49354  imaidfu  49355  imaidfu2  49356