Theorem imaeq1d 6014

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

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

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 2705

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 2712  df-cleq 2725  df-clel 2808  df-rab 3397  df-v 3439  df-dif 3901  df-un 3903  df-in 3905  df-ss 3915  df-nul 4283  df-if 4477  df-sn 4578  df-pr 4580  df-op 4584  df-br 5096  df-opab 5158  df-cnv 5629  df-dm 5631  df-rn 5632  df-res 5633  df-ima 5634

This theorem is referenced by:  imaeq12d  6016  nfimad  6024  csbrn  6157  f1imacnv  6786  foimacnv  6787  fimacnvinrn  7012  seqomeq12  8381  ssenen  9073  fipreima  9251  oieq1  9407  oieq2  9408  dfac12lem1  10044  dfac12r  10047  fpwwe2cbv  10530  fpwwe2lem2  10532  fpwwecbv  10544  fpwwelem  10545  seqeq1  13915  seqeq2  13916  seqeq3  13917  1arith  16843  vdwmc  16894  vdwnnlem1  16911  ramub2  16930  rami  16931  imasless  17448  gsumvalx  18588  eqglact  19095  eqg0subgecsn  19113  psgnunilem1  19409  evpmss  21527  psgnevpmb  21528  frlmup3  21741  psrbag  21858  psrbaglefi  21867  iscn  23153  ptbasfi  23499  ptval2  23519  ptrescn  23557  xkoptsub  23572  qtopval  23613  cmphaushmeo  23718  ptcmpg  23975  restutopopn  24156  prdsxmslem2  24447  metuval  24467  nghmfval  24640  isnghm  24641  ismbf1  25555  ismbf  25559  mbfconst  25564  mbfres2  25576  cncombf  25589  isi1f  25605  itg1val  25614  deg1val  26031  fta1glem2  26104  fta1g  26105  fta1b  26107  dgrval  26163  dgrlem  26164  coeidlem  26172  coe11  26188  fta1lem  26245  fta1  26246  vieta1lem2  26249  vieta1  26250  taylthlem2  26312  taylthlem2OLD  26313  areaval  26904  sqff1o  27122  seqseq123d  28219  nlfnval  31865  xppreima2  32637  ofpreima  32651  mptiffisupp  32680  fpwrelmapffslem  32721  indf1ofs  32856  evpmval  33123  altgnsg  33127  ply1dg3rt0irred  33555  xrhval  34054  ismbfm  34287  mbfmcst  34295  issibf  34369  sitgfval  34377  eulerpartlemelr  34393  eulerpartleme  34399  eulerpartlemo  34401  eulerpartlemt0  34405  eulerpartlemt  34407  eulerpartlemr  34410  eulerpartlemgf  34415  eulerpartlemgs2  34416  eulerpartlemn  34417  eulerpart  34418  ballotlemscr  34555  ballotlemrv  34556  ballotlemrinv0  34569  iscvm  35326  cvmliftmolem1  35348  cvmlift2lem9a  35370  cvmlift2lem9  35378  msrfval  35604  ismfs  35616  mthmval  35642  bj-imdirval2  37250  bj-iminvval2  37261  poimirlem4  37687  poimirlem5  37688  poimirlem6  37689  poimirlem7  37690  poimirlem8  37691  poimirlem10  37693  poimirlem11  37694  poimirlem12  37695  poimirlem13  37696  poimirlem14  37697  poimirlem15  37698  poimirlem16  37699  poimirlem17  37700  poimirlem18  37701  poimirlem19  37702  poimirlem20  37703  poimirlem21  37704  poimirlem22  37705  poimirlem26  37709  poimirlem27  37710  poimirlem32  37715  cnambfre  37731  itg2addnclem2  37735  ftc1anclem1  37756  ftc1anclem6  37761  lkrval  39210  aks6d1c6lem4  42289  aks6d1c6lem5  42293  aks6d1c7lem3  42298  prjcrvfval  42752  prjcrvval  42753  prjcrv0  42754  pw2f1o2val  43159  aomclem8  43181  pwfi2f1o  43216  trclimalb2  43846  frege131d  43884  colleq12d  44373  dirkercncflem2  46229  issmflem  46852  smfpimioo  46912  smfpimcc  46933  smfsuplem2  46937  3f1oss1  47202  imaidfu2lem  49237  imaidfu  49238  imaidfu2  49239