Theorem imaeq1d 6026

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

Syntax hints:   → wi 4   = wceq 1542   “ cima 5635

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 3402  df-v 3444  df-dif 3906  df-un 3908  df-in 3910  df-ss 3920  df-nul 4288  df-if 4482  df-sn 4583  df-pr 4585  df-op 4589  df-br 5101  df-opab 5163  df-cnv 5640  df-dm 5642  df-rn 5643  df-res 5644  df-ima 5645

This theorem is referenced by:  imaeq12d  6028  nfimad  6036  csbrn  6169  f1imacnv  6798  foimacnv  6799  fimacnvinrn  7025  seqomeq12  8395  ssenen  9091  fipreima  9270  oieq1  9429  oieq2  9430  dfac12lem1  10066  dfac12r  10069  fpwwe2cbv  10553  fpwwe2lem2  10555  fpwwecbv  10567  fpwwelem  10568  seqeq1  13939  seqeq2  13940  seqeq3  13941  1arith  16867  vdwmc  16918  vdwnnlem1  16935  ramub2  16954  rami  16955  imasless  17473  gsumvalx  18613  eqglact  19120  eqg0subgecsn  19138  psgnunilem1  19434  evpmss  21553  psgnevpmb  21554  frlmup3  21767  psrbag  21885  psrbaglefi  21894  iscn  23191  ptbasfi  23537  ptval2  23557  ptrescn  23595  xkoptsub  23610  qtopval  23651  cmphaushmeo  23756  ptcmpg  24013  restutopopn  24194  prdsxmslem2  24485  metuval  24505  nghmfval  24678  isnghm  24679  ismbf1  25593  ismbf  25597  mbfconst  25602  mbfres2  25614  cncombf  25627  isi1f  25643  itg1val  25652  deg1val  26069  fta1glem2  26142  fta1g  26143  fta1b  26145  dgrval  26201  dgrlem  26202  coeidlem  26210  coe11  26226  fta1lem  26283  fta1  26284  vieta1lem2  26287  vieta1  26288  taylthlem2  26350  taylthlem2OLD  26351  areaval  26942  sqff1o  27160  seqseq123d  28294  nlfnval  31968  xppreima2  32740  ofpreima  32754  mptiffisupp  32782  fpwrelmapffslem  32821  indf1ofs  32958  evpmval  33238  altgnsg  33242  ply1dg3rt0irred  33676  vieta  33756  xrhval  34195  ismbfm  34428  mbfmcst  34436  issibf  34510  sitgfval  34518  eulerpartlemelr  34534  eulerpartleme  34540  eulerpartlemo  34542  eulerpartlemt0  34546  eulerpartlemt  34548  eulerpartlemr  34551  eulerpartlemgf  34556  eulerpartlemgs2  34557  eulerpartlemn  34558  eulerpart  34559  ballotlemscr  34696  ballotlemrv  34697  ballotlemrinv0  34710  iscvm  35472  cvmliftmolem1  35494  cvmlift2lem9a  35516  cvmlift2lem9  35524  msrfval  35750  ismfs  35762  mthmval  35788  bj-imdirval2  37435  bj-iminvval2  37446  poimirlem4  37872  poimirlem5  37873  poimirlem6  37874  poimirlem7  37875  poimirlem8  37876  poimirlem10  37878  poimirlem11  37879  poimirlem12  37880  poimirlem13  37881  poimirlem14  37882  poimirlem15  37883  poimirlem16  37884  poimirlem17  37885  poimirlem18  37886  poimirlem19  37887  poimirlem20  37888  poimirlem21  37889  poimirlem22  37890  poimirlem26  37894  poimirlem27  37895  poimirlem32  37900  cnambfre  37916  itg2addnclem2  37920  ftc1anclem1  37941  ftc1anclem6  37946  lkrval  39461  aks6d1c6lem4  42540  aks6d1c6lem5  42544  aks6d1c7lem3  42549  prjcrvfval  42986  prjcrvval  42987  prjcrv0  42988  pw2f1o2val  43393  aomclem8  43415  pwfi2f1o  43450  trclimalb2  44079  frege131d  44117  colleq12d  44606  dirkercncflem2  46459  issmflem  47082  smfpimioo  47142  smfpimcc  47163  smfsuplem2  47167  3f1oss1  47432  imaidfu2lem  49465  imaidfu  49466  imaidfu2  49467