Theorem imaeq1d 6088

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

Syntax hints:   → wi 4   = wceq 1537   “ cima 5703

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1793  ax-4 1807  ax-5 1909  ax-6 1967  ax-7 2007  ax-8 2110  ax-9 2118  ax-ext 2711

This theorem depends on definitions:  df-bi 207  df-an 396  df-or 847  df-3an 1089  df-tru 1540  df-fal 1550  df-ex 1778  df-sb 2065  df-clab 2718  df-cleq 2732  df-clel 2819  df-rab 3444  df-v 3490  df-dif 3979  df-un 3981  df-in 3983  df-ss 3993  df-nul 4353  df-if 4549  df-sn 4649  df-pr 4651  df-op 4655  df-br 5167  df-opab 5229  df-cnv 5708  df-dm 5710  df-rn 5711  df-res 5712  df-ima 5713

This theorem is referenced by:  imaeq12d  6090  nfimad  6098  csbrn  6234  f1imacnv  6878  foimacnv  6879  fimacnvinrn  7105  seqomeq12  8510  ssenen  9217  fipreima  9428  oieq1  9581  oieq2  9582  dfac12lem1  10213  dfac12r  10216  fpwwe2cbv  10699  fpwwe2lem2  10701  fpwwecbv  10713  fpwwelem  10714  seqeq1  14055  seqeq2  14056  seqeq3  14057  1arith  16974  vdwmc  17025  vdwnnlem1  17042  ramub2  17061  rami  17062  imasless  17600  gsumvalx  18714  eqglact  19219  eqg0subgecsn  19237  psgnunilem1  19535  evpmss  21627  psgnevpmb  21628  frlmup3  21843  psrbag  21960  psrbaglefi  21969  iscn  23264  ptbasfi  23610  ptval2  23630  ptrescn  23668  xkoptsub  23683  qtopval  23724  cmphaushmeo  23829  ptcmpg  24086  restutopopn  24268  prdsxmslem2  24563  metuval  24583  nghmfval  24764  isnghm  24765  ismbf1  25678  ismbf  25682  mbfconst  25687  mbfres2  25699  cncombf  25712  isi1f  25728  itg1val  25737  deg1val  26155  fta1glem2  26228  fta1g  26229  fta1b  26231  dgrval  26287  dgrlem  26288  coeidlem  26296  coe11  26312  fta1lem  26367  fta1  26368  vieta1lem2  26371  vieta1  26372  taylthlem2  26434  taylthlem2OLD  26435  areaval  27025  sqff1o  27243  seqseq123d  28310  nlfnval  31913  xppreima2  32669  ofpreima  32683  mptiffisupp  32705  fpwrelmapffslem  32746  evpmval  33138  altgnsg  33142  ply1dg3rt0irred  33572  xrhval  33964  indf1ofs  33990  ismbfm  34215  mbfmcst  34224  issibf  34298  sitgfval  34306  eulerpartlemelr  34322  eulerpartleme  34328  eulerpartlemo  34330  eulerpartlemt0  34334  eulerpartlemt  34336  eulerpartlemr  34339  eulerpartlemgf  34344  eulerpartlemgs2  34345  eulerpartlemn  34346  eulerpart  34347  ballotlemscr  34483  ballotlemrv  34484  ballotlemrinv0  34497  iscvm  35227  cvmliftmolem1  35249  cvmlift2lem9a  35271  cvmlift2lem9  35279  msrfval  35505  ismfs  35517  mthmval  35543  bj-imdirval2  37149  bj-iminvval2  37160  poimirlem4  37584  poimirlem5  37585  poimirlem6  37586  poimirlem7  37587  poimirlem8  37588  poimirlem10  37590  poimirlem11  37591  poimirlem12  37592  poimirlem13  37593  poimirlem14  37594  poimirlem15  37595  poimirlem16  37596  poimirlem17  37597  poimirlem18  37598  poimirlem19  37599  poimirlem20  37600  poimirlem21  37601  poimirlem22  37602  poimirlem26  37606  poimirlem27  37607  poimirlem32  37612  cnambfre  37628  itg2addnclem2  37632  ftc1anclem1  37653  ftc1anclem6  37658  lkrval  39044  aks6d1c6lem4  42130  aks6d1c6lem5  42134  aks6d1c7lem3  42139  prjcrvfval  42586  prjcrvval  42587  prjcrv0  42588  pw2f1o2val  42996  aomclem8  43018  pwfi2f1o  43053  trclimalb2  43688  frege131d  43726  colleq12d  44222  dirkercncflem2  46025  issmflem  46648  smfpimioo  46708  smfpimcc  46729  smfsuplem2  46733  3f1oss1  46990