Theorem imaeq1d 6063

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

Syntax hints:   → wi 4   = wceq 1570   “ cima 5666

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1825  ax-4 1839  ax-5 1940  ax-6 1997  ax-7 2038  ax-8 2145  ax-9 2153  ax-ext 2735

This theorem depends on definitions:  df-bi 210  df-an 401  df-or 861  df-3an 1105  df-tru 1573  df-fal 1583  df-ex 1810  df-sb 2097  df-clab 2742  df-cleq 2755  df-clel 2838  df-rab 3417  df-v 3457  df-dif 3909  df-un 3911  df-in 3913  df-ss 3923  df-nul 4288  df-if 4489  df-sn 4591  df-pr 4593  df-op 4597  df-br 5111  df-opab 5175  df-cnv 5671  df-dm 5673  df-rn 5674  df-res 5675  df-ima 5676

This theorem is referenced by:  imaeq12d  6065  nfimad  6073  csbrn  6206  f1imacnv  6839  foimacnv  6840  fimacnvinrn  7068  seqomeq12  8442  ssenen  9140  fipreima  9316  oieq1  9475  oieq2  9476  dfac12lem1  10128  dfac12r  10131  fpwwe2cbv  10616  fpwwe2lem2  10618  fpwwecbv  10630  fpwwelem  10631  seqeq1  14042  seqeq2  14043  seqeq3  14044  1arith  16988  vdwmc  17039  vdwnnlem1  17056  ramub2  17075  rami  17076  imasless  17595  gsumvalx  18735  eqglact  19248  eqg0subgecsn  19269  psgnunilem1  19564  evpmss  21717  psgnevpmb  21718  frlmup3  21931  psrbag  22048  psrbaglefi  22057  iscn  23373  ptbasfi  23719  ptval2  23739  ptrescn  23777  xkoptsub  23792  qtopval  23833  cmphaushmeo  23938  ptcmpg  24195  restutopopn  24376  prdsxmslem2  24667  metuval  24687  nghmfval  24860  isnghm  24861  ismbf1  25764  ismbf  25768  mbfconst  25773  mbfres2  25785  cncombf  25798  isi1f  25814  itg1val  25823  deg1val  26234  fta1glem2  26307  fta1g  26308  fta1b  26310  dgrval  26366  dgrlem  26367  coeidlem  26375  coe11  26391  fta1lem  26449  fta1  26450  vieta1lem2  26453  vieta1  26454  taylthlem2  26518  areaval  27110  sqff1o  27327  seqseq123d  28460  nlfnval  32214  xppreima2  32977  ofpreima  32991  mptiffisupp  33019  fpwrelmapffslem  33058  indf1ofs  33167  evpmval  33446  altgnsg  33450  ply1dg3rt0irred  33855  vieta  33951  xrhval  34389  ismbfm  34622  mbfmcst  34630  issibf  34704  sitgfval  34712  eulerpartlemelr  34728  eulerpartleme  34734  eulerpartlemo  34736  eulerpartlemt0  34740  eulerpartlemt  34742  eulerpartlemr  34745  eulerpartlemgf  34750  eulerpartlemgs2  34751  eulerpartlemn  34752  eulerpart  34753  ballotlemscr  34890  ballotlemrv  34891  ballotlemrinv0  34904  iscvm  35732  cvmliftmolem1  35754  cvmlift2lem9a  35776  cvmlift2lem9  35784  msrfval  36010  ismfs  36022  mthmval  36048  ttcid  36984  bj-imdirval2  37808  bj-iminvval2  37819  poimirlem4  38256  poimirlem5  38257  poimirlem6  38258  poimirlem7  38259  poimirlem8  38260  poimirlem10  38262  poimirlem11  38263  poimirlem12  38264  poimirlem13  38265  poimirlem14  38266  poimirlem15  38267  poimirlem16  38268  poimirlem17  38269  poimirlem18  38270  poimirlem19  38271  poimirlem20  38272  poimirlem21  38273  poimirlem22  38274  poimirlem26  38278  poimirlem27  38279  poimirlem32  38284  cnambfre  38300  itg2addnclem2  38304  ftc1anclem1  38325  ftc1anclem6  38330  lkrval  39843  aks6d1c6lem4  42921  aks6d1c6lem5  42925  aks6d1c7lem3  42930  prjcrvfval  43346  prjcrvval  43347  prjcrv0  43348  pw2f1o2val  43749  aomclem8  43771  pwfi2f1o  43806  trclimalb2  44435  frege131d  44473  colleq12d  44946  dirkercncflem2  46801  issmflem  47424  smfpimioo  47484  smfpimcc  47505  smfsuplem2  47509  3f1oss1  47795  imaidfu2lem  49870  imaidfu  49871  imaidfu2  49872