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 1542   “ cima 5627

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1797  ax-4 1811  ax-5 1912  ax-6 1969  ax-7 2010  ax-8 2116  ax-9 2124  ax-ext 2709

This theorem depends on definitions:  df-bi 207  df-an 396  df-or 849  df-3an 1089  df-tru 1545  df-fal 1555  df-ex 1782  df-sb 2069  df-clab 2716  df-cleq 2729  df-clel 2812  df-rab 3391  df-v 3432  df-dif 3893  df-un 3895  df-in 3897  df-ss 3907  df-nul 4275  df-if 4468  df-sn 4569  df-pr 4571  df-op 4575  df-br 5087  df-opab 5149  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  7017  seqomeq12  8386  ssenen  9082  fipreima  9261  oieq1  9420  oieq2  9421  dfac12lem1  10057  dfac12r  10060  fpwwe2cbv  10544  fpwwe2lem2  10546  fpwwecbv  10558  fpwwelem  10559  seqeq1  13957  seqeq2  13958  seqeq3  13959  1arith  16889  vdwmc  16940  vdwnnlem1  16957  ramub2  16976  rami  16977  imasless  17495  gsumvalx  18635  eqglact  19145  eqg0subgecsn  19163  psgnunilem1  19459  evpmss  21576  psgnevpmb  21577  frlmup3  21790  psrbag  21907  psrbaglefi  21916  iscn  23210  ptbasfi  23556  ptval2  23576  ptrescn  23614  xkoptsub  23629  qtopval  23670  cmphaushmeo  23775  ptcmpg  24032  restutopopn  24213  prdsxmslem2  24504  metuval  24524  nghmfval  24697  isnghm  24698  ismbf1  25601  ismbf  25605  mbfconst  25610  mbfres2  25622  cncombf  25635  isi1f  25651  itg1val  25660  deg1val  26071  fta1glem2  26144  fta1g  26145  fta1b  26147  dgrval  26203  dgrlem  26204  coeidlem  26212  coe11  26228  fta1lem  26284  fta1  26285  vieta1lem2  26288  vieta1  26289  taylthlem2  26351  taylthlem2OLD  26352  areaval  26941  sqff1o  27159  seqseq123d  28292  nlfnval  31967  xppreima2  32739  ofpreima  32753  mptiffisupp  32781  fpwrelmapffslem  32820  indf1ofs  32941  evpmval  33221  altgnsg  33225  ply1dg3rt0irred  33659  vieta  33739  xrhval  34178  ismbfm  34411  mbfmcst  34419  issibf  34493  sitgfval  34501  eulerpartlemelr  34517  eulerpartleme  34523  eulerpartlemo  34525  eulerpartlemt0  34529  eulerpartlemt  34531  eulerpartlemr  34534  eulerpartlemgf  34539  eulerpartlemgs2  34540  eulerpartlemn  34541  eulerpart  34542  ballotlemscr  34679  ballotlemrv  34680  ballotlemrinv0  34693  iscvm  35457  cvmliftmolem1  35479  cvmlift2lem9a  35501  cvmlift2lem9  35509  msrfval  35735  ismfs  35747  mthmval  35773  ttcid  36690  bj-imdirval2  37513  bj-iminvval2  37524  poimirlem4  37959  poimirlem5  37960  poimirlem6  37961  poimirlem7  37962  poimirlem8  37963  poimirlem10  37965  poimirlem11  37966  poimirlem12  37967  poimirlem13  37968  poimirlem14  37969  poimirlem15  37970  poimirlem16  37971  poimirlem17  37972  poimirlem18  37973  poimirlem19  37974  poimirlem20  37975  poimirlem21  37976  poimirlem22  37977  poimirlem26  37981  poimirlem27  37982  poimirlem32  37987  cnambfre  38003  itg2addnclem2  38007  ftc1anclem1  38028  ftc1anclem6  38033  lkrval  39548  aks6d1c6lem4  42626  aks6d1c6lem5  42630  aks6d1c7lem3  42635  prjcrvfval  43078  prjcrvval  43079  prjcrv0  43080  pw2f1o2val  43485  aomclem8  43507  pwfi2f1o  43542  trclimalb2  44171  frege131d  44209  colleq12d  44698  dirkercncflem2  46550  issmflem  47173  smfpimioo  47233  smfpimcc  47254  smfsuplem2  47258  3f1oss1  47535  imaidfu2lem  49596  imaidfu  49597  imaidfu2  49598