Theorem imaeq1d 6013

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 6009	. 2 ⊢ (𝐴 = 𝐵 → (𝐴 “ 𝐶) = (𝐵 “ 𝐶))
3	1, 2	syl 17	1 ⊢ (𝜑 → (𝐴 “ 𝐶) = (𝐵 “ 𝐶))

Syntax hints:   → wi 4   = wceq 1541   “ cima 5622

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 2113  ax-9 2121  ax-ext 2703

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 2710  df-cleq 2723  df-clel 2806  df-rab 3396  df-v 3438  df-dif 3900  df-un 3902  df-in 3904  df-ss 3914  df-nul 4283  df-if 4475  df-sn 4576  df-pr 4578  df-op 4582  df-br 5094  df-opab 5156  df-cnv 5627  df-dm 5629  df-rn 5630  df-res 5631  df-ima 5632

This theorem is referenced by:  imaeq12d  6015  nfimad  6023  csbrn  6156  f1imacnv  6785  foimacnv  6786  fimacnvinrn  7010  seqomeq12  8379  ssenen  9070  fipreima  9248  oieq1  9404  oieq2  9405  dfac12lem1  10041  dfac12r  10044  fpwwe2cbv  10527  fpwwe2lem2  10529  fpwwecbv  10541  fpwwelem  10542  seqeq1  13917  seqeq2  13918  seqeq3  13919  1arith  16845  vdwmc  16896  vdwnnlem1  16913  ramub2  16932  rami  16933  imasless  17450  gsumvalx  18590  eqglact  19097  eqg0subgecsn  19115  psgnunilem1  19411  evpmss  21529  psgnevpmb  21530  frlmup3  21743  psrbag  21860  psrbaglefi  21869  iscn  23156  ptbasfi  23502  ptval2  23522  ptrescn  23560  xkoptsub  23575  qtopval  23616  cmphaushmeo  23721  ptcmpg  23978  restutopopn  24159  prdsxmslem2  24450  metuval  24470  nghmfval  24643  isnghm  24644  ismbf1  25558  ismbf  25562  mbfconst  25567  mbfres2  25579  cncombf  25592  isi1f  25608  itg1val  25617  deg1val  26034  fta1glem2  26107  fta1g  26108  fta1b  26110  dgrval  26166  dgrlem  26167  coeidlem  26175  coe11  26191  fta1lem  26248  fta1  26249  vieta1lem2  26252  vieta1  26253  taylthlem2  26315  taylthlem2OLD  26316  areaval  26907  sqff1o  27125  seqseq123d  28222  nlfnval  31868  xppreima2  32640  ofpreima  32654  mptiffisupp  32681  fpwrelmapffslem  32722  indf1ofs  32854  evpmval  33121  altgnsg  33125  ply1dg3rt0irred  33553  xrhval  34038  ismbfm  34271  mbfmcst  34279  issibf  34353  sitgfval  34361  eulerpartlemelr  34377  eulerpartleme  34383  eulerpartlemo  34385  eulerpartlemt0  34389  eulerpartlemt  34391  eulerpartlemr  34394  eulerpartlemgf  34399  eulerpartlemgs2  34400  eulerpartlemn  34401  eulerpart  34402  ballotlemscr  34539  ballotlemrv  34540  ballotlemrinv0  34553  iscvm  35310  cvmliftmolem1  35332  cvmlift2lem9a  35354  cvmlift2lem9  35362  msrfval  35588  ismfs  35600  mthmval  35626  bj-imdirval2  37234  bj-iminvval2  37245  poimirlem4  37670  poimirlem5  37671  poimirlem6  37672  poimirlem7  37673  poimirlem8  37674  poimirlem10  37676  poimirlem11  37677  poimirlem12  37678  poimirlem13  37679  poimirlem14  37680  poimirlem15  37681  poimirlem16  37682  poimirlem17  37683  poimirlem18  37684  poimirlem19  37685  poimirlem20  37686  poimirlem21  37687  poimirlem22  37688  poimirlem26  37692  poimirlem27  37693  poimirlem32  37698  cnambfre  37714  itg2addnclem2  37718  ftc1anclem1  37739  ftc1anclem6  37744  lkrval  39193  aks6d1c6lem4  42272  aks6d1c6lem5  42276  aks6d1c7lem3  42281  prjcrvfval  42730  prjcrvval  42731  prjcrv0  42732  pw2f1o2val  43137  aomclem8  43159  pwfi2f1o  43194  trclimalb2  43824  frege131d  43862  colleq12d  44351  dirkercncflem2  46207  issmflem  46830  smfpimioo  46890  smfpimcc  46911  smfsuplem2  46915  3f1oss1  47180  imaidfu2lem  49215  imaidfu  49216  imaidfu2  49217