Theorem imaeq1d 6030

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

Syntax hints:   → wi 4   = wceq 1540   “ cima 5641

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1795  ax-4 1809  ax-5 1910  ax-6 1967  ax-7 2008  ax-8 2111  ax-9 2119  ax-ext 2701

This theorem depends on definitions:  df-bi 207  df-an 396  df-or 848  df-3an 1088  df-tru 1543  df-fal 1553  df-ex 1780  df-sb 2066  df-clab 2708  df-cleq 2721  df-clel 2803  df-rab 3406  df-v 3449  df-dif 3917  df-un 3919  df-in 3921  df-ss 3931  df-nul 4297  df-if 4489  df-sn 4590  df-pr 4592  df-op 4596  df-br 5108  df-opab 5170  df-cnv 5646  df-dm 5648  df-rn 5649  df-res 5650  df-ima 5651

This theorem is referenced by:  imaeq12d  6032  nfimad  6040  csbrn  6176  f1imacnv  6816  foimacnv  6817  fimacnvinrn  7043  seqomeq12  8422  ssenen  9115  fipreima  9309  oieq1  9465  oieq2  9466  dfac12lem1  10097  dfac12r  10100  fpwwe2cbv  10583  fpwwe2lem2  10585  fpwwecbv  10597  fpwwelem  10598  seqeq1  13969  seqeq2  13970  seqeq3  13971  1arith  16898  vdwmc  16949  vdwnnlem1  16966  ramub2  16985  rami  16986  imasless  17503  gsumvalx  18603  eqglact  19111  eqg0subgecsn  19129  psgnunilem1  19423  evpmss  21495  psgnevpmb  21496  frlmup3  21709  psrbag  21826  psrbaglefi  21835  iscn  23122  ptbasfi  23468  ptval2  23488  ptrescn  23526  xkoptsub  23541  qtopval  23582  cmphaushmeo  23687  ptcmpg  23944  restutopopn  24126  prdsxmslem2  24417  metuval  24437  nghmfval  24610  isnghm  24611  ismbf1  25525  ismbf  25529  mbfconst  25534  mbfres2  25546  cncombf  25559  isi1f  25575  itg1val  25584  deg1val  26001  fta1glem2  26074  fta1g  26075  fta1b  26077  dgrval  26133  dgrlem  26134  coeidlem  26142  coe11  26158  fta1lem  26215  fta1  26216  vieta1lem2  26219  vieta1  26220  taylthlem2  26282  taylthlem2OLD  26283  areaval  26874  sqff1o  27092  seqseq123d  28180  nlfnval  31810  xppreima2  32575  ofpreima  32589  mptiffisupp  32616  fpwrelmapffslem  32655  indf1ofs  32789  evpmval  33102  altgnsg  33106  ply1dg3rt0irred  33551  xrhval  34008  ismbfm  34241  mbfmcst  34250  issibf  34324  sitgfval  34332  eulerpartlemelr  34348  eulerpartleme  34354  eulerpartlemo  34356  eulerpartlemt0  34360  eulerpartlemt  34362  eulerpartlemr  34365  eulerpartlemgf  34370  eulerpartlemgs2  34371  eulerpartlemn  34372  eulerpart  34373  ballotlemscr  34510  ballotlemrv  34511  ballotlemrinv0  34524  iscvm  35246  cvmliftmolem1  35268  cvmlift2lem9a  35290  cvmlift2lem9  35298  msrfval  35524  ismfs  35536  mthmval  35562  bj-imdirval2  37171  bj-iminvval2  37182  poimirlem4  37618  poimirlem5  37619  poimirlem6  37620  poimirlem7  37621  poimirlem8  37622  poimirlem10  37624  poimirlem11  37625  poimirlem12  37626  poimirlem13  37627  poimirlem14  37628  poimirlem15  37629  poimirlem16  37630  poimirlem17  37631  poimirlem18  37632  poimirlem19  37633  poimirlem20  37634  poimirlem21  37635  poimirlem22  37636  poimirlem26  37640  poimirlem27  37641  poimirlem32  37646  cnambfre  37662  itg2addnclem2  37666  ftc1anclem1  37687  ftc1anclem6  37692  lkrval  39081  aks6d1c6lem4  42161  aks6d1c6lem5  42165  aks6d1c7lem3  42170  prjcrvfval  42619  prjcrvval  42620  prjcrv0  42621  pw2f1o2val  43028  aomclem8  43050  pwfi2f1o  43085  trclimalb2  43715  frege131d  43753  colleq12d  44242  dirkercncflem2  46102  issmflem  46725  smfpimioo  46785  smfpimcc  46806  smfsuplem2  46810  3f1oss1  47076  imaidfu2lem  49098  imaidfu  49099  imaidfu2  49100