Theorem imaeq1d 5966

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

Syntax hints:   → wi 4   = wceq 1542   “ cima 5592

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1802  ax-4 1816  ax-5 1917  ax-6 1975  ax-7 2015  ax-8 2112  ax-9 2120  ax-ext 2711

This theorem depends on definitions:  df-bi 206  df-an 397  df-or 845  df-3an 1088  df-tru 1545  df-fal 1555  df-ex 1787  df-sb 2072  df-clab 2718  df-cleq 2732  df-clel 2818  df-rab 3075  df-v 3433  df-dif 3895  df-un 3897  df-in 3899  df-ss 3909  df-nul 4263  df-if 4466  df-sn 4568  df-pr 4570  df-op 4574  df-br 5080  df-opab 5142  df-cnv 5597  df-dm 5599  df-rn 5600  df-res 5601  df-ima 5602

This theorem is referenced by:  imaeq12d  5968  nfimad  5976  csbrn  6104  f1imacnv  6729  foimacnv  6730  fimacnvinrn  6944  seqomeq12  8270  ssenen  8912  fipreima  9095  oieq1  9241  oieq2  9242  dfac12lem1  9892  dfac12r  9895  fpwwe2cbv  10379  fpwwe2lem2  10381  fpwwecbv  10393  fpwwelem  10394  seqeq1  13714  seqeq2  13715  seqeq3  13716  1arith  16618  vdwmc  16669  vdwnnlem1  16686  ramub2  16705  rami  16706  imasless  17241  gsumvalx  18350  eqglact  18797  psgnunilem1  19091  evpmss  20781  psgnevpmb  20782  frlmup3  20997  psrbag  21110  psrbaglefi  21125  psrbaglefiOLD  21126  iscn  22376  ptbasfi  22722  ptval2  22742  ptrescn  22780  xkoptsub  22795  qtopval  22836  cmphaushmeo  22941  ptcmpg  23198  restutopopn  23380  prdsxmslem2  23675  metuval  23695  nghmfval  23876  isnghm  23877  ismbf1  24778  ismbf  24782  mbfconst  24787  mbfres2  24799  cncombf  24812  isi1f  24828  itg1val  24837  deg1val  25251  fta1glem2  25321  fta1g  25322  fta1b  25324  dgrval  25379  dgrlem  25380  coeidlem  25388  coe11  25404  fta1lem  25457  fta1  25458  vieta1lem2  25461  vieta1  25462  taylthlem2  25523  areaval  26104  sqff1o  26321  nlfnval  30231  xppreima2  30976  ofpreima  30990  fpwrelmapffslem  31055  evpmval  31400  altgnsg  31404  xrhval  31956  indf1ofs  31982  ismbfm  32207  mbfmcst  32214  issibf  32288  sitgfval  32296  eulerpartlemelr  32312  eulerpartleme  32318  eulerpartlemo  32320  eulerpartlemt0  32324  eulerpartlemt  32326  eulerpartlemr  32329  eulerpartlemgf  32334  eulerpartlemgs2  32335  eulerpartlemn  32336  eulerpart  32337  ballotlemscr  32473  ballotlemrv  32474  ballotlemrinv0  32487  iscvm  33209  cvmliftmolem1  33231  cvmlift2lem9a  33253  cvmlift2lem9  33261  msrfval  33487  ismfs  33499  mthmval  33525  bj-imdirval2  35342  bj-iminvval2  35353  poimirlem4  35769  poimirlem5  35770  poimirlem6  35771  poimirlem7  35772  poimirlem8  35773  poimirlem10  35775  poimirlem11  35776  poimirlem12  35777  poimirlem13  35778  poimirlem14  35779  poimirlem15  35780  poimirlem16  35781  poimirlem17  35782  poimirlem18  35783  poimirlem19  35784  poimirlem20  35785  poimirlem21  35786  poimirlem22  35787  poimirlem26  35791  poimirlem27  35792  poimirlem32  35797  cnambfre  35813  itg2addnclem2  35817  ftc1anclem1  35838  ftc1anclem6  35843  lkrval  37090  prjcrvfval  40457  prjcrvval  40458  prjcrv0  40459  pw2f1o2val  40850  aomclem8  40875  pwfi2f1o  40910  trclimalb2  41296  frege131d  41334  colleq12d  41833  dirkercncflem2  43608  issmflem  44223  smfpimioo  44281  smfpimcc  44301  smfsuplem2  44305