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 ⊢ (𝜑 → (𝐴 “ 𝐶) = (𝐵 “ 𝐶))

This proof depends on syntax axioms:   → wi 4   = wceq 1570   “ cima 5666

This proof depends on axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1828  ax-4 1842  ax-5 1943  ax-6 2000  ax-7 2041  ax-8 2148  ax-9 2156  ax-ext 2737

This proof depends on definitions:  df-bi 210  df-an 402  df-or 862  df-3an 1105  df-tru 1573  df-fal 1583  df-ex 1813  df-sb 2100  df-clab 2744  df-cleq 2757  df-clel 2840  df-rab 3419  df-v 3459  df-dif 3909  df-un 3911  df-in 3913  df-ss 3923  df-nul 4287  df-if 4490  df-sn 4592  df-pr 4594  df-op 4598  df-br 5112  df-opab 5176  df-cnv 5671  df-dm 5673  df-rn 5674  df-res 5675  df-ima 5676

This theorem is used by:  imaeq12d  6065  nfimad  6073  csbrn  6206  f1imacnv  6841  foimacnv  6842  fimacnvinrn  7070  seqomeq12  8443  ssenen  9142  fipreima  9318  oieq1  9477  oieq2  9478  dfac12lem1  10139  dfac12r  10142  fpwwe2cbv  10626  fpwwe2lem2  10628  fpwwecbv  10640  fpwwelem  10641  seqeq1  14053  seqeq2  14054  seqeq3  14055  1arith  17004  vdwmc  17055  vdwnnlem1  17072  ramub2  17091  rami  17092  imasless  17611  gsumvalx  18755  eqglact  19270  eqg0subgecsn  19291  psgnunilem1  19586  evpmss  21765  psgnevpmb  21766  frlmup3  21979  psrbag  22096  psrbaglefi  22105  iscn  23421  ptbasfi  23767  ptval2  23787  ptrescn  23825  xkoptsub  23840  qtopval  23881  cmphaushmeo  23986  ptcmpg  24243  restutopopn  24424  prdsxmslem2  24715  metuval  24735  nghmfval  24908  isnghm  24909  ismbf1  25812  ismbf  25816  mbfconst  25821  mbfres2  25833  cncombf  25846  isi1f  25862  itg1val  25871  deg1val  26282  fta1glem2  26355  fta1g  26356  fta1b  26358  dgrval  26414  dgrlem  26415  coeidlem  26423  coe11  26439  fta1lem  26497  fta1  26498  vieta1lem2  26501  vieta1  26502  taylthlem2  26566  areaval  27158  sqff1o  27375  seqseq123d  28508  nlfnval  32262  xppreima2  33025  ofpreima  33039  mptiffisupp  33067  fpwrelmapffslem  33106  indf1ofs  33215  evpmval  33488  altgnsg  33492  ply1dg3rt0irred  33897  vieta  33993  xrhval  34431  ismbfm  34665  mbfmcst  34673  issibf  34747  sitgfval  34755  eulerpartlemelr  34771  eulerpartleme  34777  eulerpartlemo  34779  eulerpartlemt0  34783  eulerpartlemt  34785  eulerpartlemr  34788  eulerpartlemgf  34793  eulerpartlemgs2  34794  eulerpartlemn  34795  eulerpart  34796  ballotlemscr  34933  ballotlemrv  34934  ballotlemrinv0  34947  iscvm  35764  cvmliftmolem1  35786  cvmlift2lem9a  35808  cvmlift2lem9  35816  msrfval  36042  ismfs  36054  mthmval  36080  ttcid  37036  bj-imdirval2  37860  bj-iminvval2  37871  poimirlem4  38308  poimirlem5  38309  poimirlem6  38310  poimirlem7  38311  poimirlem8  38312  poimirlem10  38314  poimirlem11  38315  poimirlem12  38316  poimirlem13  38317  poimirlem14  38318  poimirlem15  38319  poimirlem16  38320  poimirlem17  38321  poimirlem18  38322  poimirlem19  38323  poimirlem20  38324  poimirlem21  38325  poimirlem22  38326  poimirlem26  38330  poimirlem27  38331  poimirlem32  38336  cnambfre  38352  itg2addnclem2  38356  ftc1anclem1  38377  ftc1anclem6  38382  lkrval  39895  aks6d1c6lem4  42973  aks6d1c6lem5  42977  aks6d1c7lem3  42982  prjcrvfval  43396  prjcrvval  43397  prjcrv0  43398  pw2f1o2val  43799  aomclem8  43821  pwfi2f1o  43856  trclimalb2  44485  frege131d  44523  colleq12d  44996  dirkercncflem2  46851  issmflem  47474  smfpimioo  47534  smfpimcc  47555  smfsuplem2  47559  3f1oss1  47845  imaidfu2lem  49920  imaidfu  49921  imaidfu2  49922