Theorem imaeq1d 5957

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

Syntax hints:   → wi 4   = wceq 1539   “ cima 5583

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1799  ax-4 1813  ax-5 1914  ax-6 1972  ax-7 2012  ax-8 2110  ax-9 2118  ax-ext 2709

This theorem depends on definitions:  df-bi 206  df-an 396  df-or 844  df-3an 1087  df-tru 1542  df-fal 1552  df-ex 1784  df-sb 2069  df-clab 2716  df-cleq 2730  df-clel 2817  df-rab 3072  df-v 3424  df-dif 3886  df-un 3888  df-in 3890  df-ss 3900  df-nul 4254  df-if 4457  df-sn 4559  df-pr 4561  df-op 4565  df-br 5071  df-opab 5133  df-cnv 5588  df-dm 5590  df-rn 5591  df-res 5592  df-ima 5593

This theorem is referenced by:  imaeq12d  5959  nfimad  5967  csbrn  6095  f1imacnv  6716  foimacnv  6717  fimacnvinrn  6931  seqomeq12  8255  ssenen  8887  fipreima  9055  oieq1  9201  oieq2  9202  dfac12lem1  9830  dfac12r  9833  fpwwe2cbv  10317  fpwwe2lem2  10319  fpwwecbv  10331  fpwwelem  10332  seqeq1  13652  seqeq2  13653  seqeq3  13654  1arith  16556  vdwmc  16607  vdwnnlem1  16624  ramub2  16643  rami  16644  imasless  17168  gsumvalx  18275  eqglact  18722  psgnunilem1  19016  evpmss  20703  psgnevpmb  20704  frlmup3  20917  psrbag  21030  psrbaglefi  21045  psrbaglefiOLD  21046  iscn  22294  ptbasfi  22640  ptval2  22660  ptrescn  22698  xkoptsub  22713  qtopval  22754  cmphaushmeo  22859  ptcmpg  23116  restutopopn  23298  prdsxmslem2  23591  metuval  23611  nghmfval  23792  isnghm  23793  ismbf1  24693  ismbf  24697  mbfconst  24702  mbfres2  24714  cncombf  24727  isi1f  24743  itg1val  24752  deg1val  25166  fta1glem2  25236  fta1g  25237  fta1b  25239  dgrval  25294  dgrlem  25295  coeidlem  25303  coe11  25319  fta1lem  25372  fta1  25373  vieta1lem2  25376  vieta1  25377  taylthlem2  25438  areaval  26019  sqff1o  26236  nlfnval  30144  xppreima2  30889  ofpreima  30904  fpwrelmapffslem  30969  evpmval  31314  altgnsg  31318  xrhval  31868  indf1ofs  31894  ismbfm  32119  mbfmcst  32126  issibf  32200  sitgfval  32208  eulerpartlemelr  32224  eulerpartleme  32230  eulerpartlemo  32232  eulerpartlemt0  32236  eulerpartlemt  32238  eulerpartlemr  32241  eulerpartlemgf  32246  eulerpartlemgs2  32247  eulerpartlemn  32248  eulerpart  32249  ballotlemscr  32385  ballotlemrv  32386  ballotlemrinv0  32399  iscvm  33121  cvmliftmolem1  33143  cvmlift2lem9a  33165  cvmlift2lem9  33173  msrfval  33399  ismfs  33411  mthmval  33437  bj-imdirval2  35281  bj-iminvval2  35292  poimirlem4  35708  poimirlem5  35709  poimirlem6  35710  poimirlem7  35711  poimirlem8  35712  poimirlem10  35714  poimirlem11  35715  poimirlem12  35716  poimirlem13  35717  poimirlem14  35718  poimirlem15  35719  poimirlem16  35720  poimirlem17  35721  poimirlem18  35722  poimirlem19  35723  poimirlem20  35724  poimirlem21  35725  poimirlem22  35726  poimirlem26  35730  poimirlem27  35731  poimirlem32  35736  cnambfre  35752  itg2addnclem2  35756  ftc1anclem1  35777  ftc1anclem6  35782  lkrval  37029  pw2f1o2val  40777  aomclem8  40802  pwfi2f1o  40837  trclimalb2  41223  frege131d  41261  colleq12d  41760  dirkercncflem2  43535  issmflem  44150  smfpimioo  44208  smfpimcc  44228  smfsuplem2  44232