Theorem imaeq1d 6008

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

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

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 3905  df-un 3907  df-in 3909  df-ss 3919  df-nul 4284  df-if 4476  df-sn 4577  df-pr 4579  df-op 4583  df-br 5092  df-opab 5154  df-cnv 5624  df-dm 5626  df-rn 5627  df-res 5628  df-ima 5629

This theorem is referenced by:  imaeq12d  6010  nfimad  6018  csbrn  6150  f1imacnv  6779  foimacnv  6780  fimacnvinrn  7004  seqomeq12  8373  ssenen  9064  fipreima  9242  oieq1  9398  oieq2  9399  dfac12lem1  10035  dfac12r  10038  fpwwe2cbv  10521  fpwwe2lem2  10523  fpwwecbv  10535  fpwwelem  10536  seqeq1  13911  seqeq2  13912  seqeq3  13913  1arith  16839  vdwmc  16890  vdwnnlem1  16907  ramub2  16926  rami  16927  imasless  17444  gsumvalx  18584  eqglact  19092  eqg0subgecsn  19110  psgnunilem1  19406  evpmss  21524  psgnevpmb  21525  frlmup3  21738  psrbag  21855  psrbaglefi  21864  iscn  23151  ptbasfi  23497  ptval2  23517  ptrescn  23555  xkoptsub  23570  qtopval  23611  cmphaushmeo  23716  ptcmpg  23973  restutopopn  24154  prdsxmslem2  24445  metuval  24465  nghmfval  24638  isnghm  24639  ismbf1  25553  ismbf  25557  mbfconst  25562  mbfres2  25574  cncombf  25587  isi1f  25603  itg1val  25612  deg1val  26029  fta1glem2  26102  fta1g  26103  fta1b  26105  dgrval  26161  dgrlem  26162  coeidlem  26170  coe11  26186  fta1lem  26243  fta1  26244  vieta1lem2  26247  vieta1  26248  taylthlem2  26310  taylthlem2OLD  26311  areaval  26902  sqff1o  27120  seqseq123d  28217  nlfnval  31859  xppreima2  32631  ofpreima  32645  mptiffisupp  32672  fpwrelmapffslem  32713  indf1ofs  32845  evpmval  33112  altgnsg  33116  ply1dg3rt0irred  33544  xrhval  34029  ismbfm  34262  mbfmcst  34270  issibf  34344  sitgfval  34352  eulerpartlemelr  34368  eulerpartleme  34374  eulerpartlemo  34376  eulerpartlemt0  34380  eulerpartlemt  34382  eulerpartlemr  34385  eulerpartlemgf  34390  eulerpartlemgs2  34391  eulerpartlemn  34392  eulerpart  34393  ballotlemscr  34530  ballotlemrv  34531  ballotlemrinv0  34544  iscvm  35301  cvmliftmolem1  35323  cvmlift2lem9a  35345  cvmlift2lem9  35353  msrfval  35579  ismfs  35591  mthmval  35617  bj-imdirval2  37223  bj-iminvval2  37234  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  39133  aks6d1c6lem4  42212  aks6d1c6lem5  42216  aks6d1c7lem3  42221  prjcrvfval  42670  prjcrvval  42671  prjcrv0  42672  pw2f1o2val  43078  aomclem8  43100  pwfi2f1o  43135  trclimalb2  43765  frege131d  43803  colleq12d  44292  dirkercncflem2  46148  issmflem  46771  smfpimioo  46831  smfpimcc  46852  smfsuplem2  46856  3f1oss1  47112  imaidfu2lem  49147  imaidfu  49148  imaidfu2  49149