Theorem imaeq1d 6058

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

Syntax hints:   → wi 4   = wceq 1541   “ cima 5679

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1797  ax-4 1811  ax-5 1913  ax-6 1971  ax-7 2011  ax-8 2108  ax-9 2116  ax-ext 2703

This theorem depends on definitions:  df-bi 206  df-an 397  df-or 846  df-3an 1089  df-tru 1544  df-fal 1554  df-ex 1782  df-sb 2068  df-clab 2710  df-cleq 2724  df-clel 2810  df-rab 3433  df-v 3476  df-dif 3951  df-un 3953  df-in 3955  df-ss 3965  df-nul 4323  df-if 4529  df-sn 4629  df-pr 4631  df-op 4635  df-br 5149  df-opab 5211  df-cnv 5684  df-dm 5686  df-rn 5687  df-res 5688  df-ima 5689

This theorem is referenced by:  imaeq12d  6060  nfimad  6068  csbrn  6202  f1imacnv  6849  foimacnv  6850  fimacnvinrn  7073  seqomeq12  8456  ssenen  9153  fipreima  9360  oieq1  9509  oieq2  9510  dfac12lem1  10140  dfac12r  10143  fpwwe2cbv  10627  fpwwe2lem2  10629  fpwwecbv  10641  fpwwelem  10642  seqeq1  13973  seqeq2  13974  seqeq3  13975  1arith  16864  vdwmc  16915  vdwnnlem1  16932  ramub2  16951  rami  16952  imasless  17490  gsumvalx  18601  eqglact  19095  eqg0subgecsn  19112  psgnunilem1  19402  evpmss  21358  psgnevpmb  21359  frlmup3  21574  psrbag  21689  psrbaglefi  21704  psrbaglefiOLD  21705  iscn  22959  ptbasfi  23305  ptval2  23325  ptrescn  23363  xkoptsub  23378  qtopval  23419  cmphaushmeo  23524  ptcmpg  23781  restutopopn  23963  prdsxmslem2  24258  metuval  24278  nghmfval  24459  isnghm  24460  ismbf1  25365  ismbf  25369  mbfconst  25374  mbfres2  25386  cncombf  25399  isi1f  25415  itg1val  25424  deg1val  25838  fta1glem2  25908  fta1g  25909  fta1b  25911  dgrval  25966  dgrlem  25967  coeidlem  25975  coe11  25991  fta1lem  26044  fta1  26045  vieta1lem2  26048  vieta1  26049  taylthlem2  26110  areaval  26693  sqff1o  26910  nlfnval  31389  xppreima2  32131  ofpreima  32145  mptiffisupp  32170  fpwrelmapffslem  32212  evpmval  32562  altgnsg  32566  xrhval  33284  indf1ofs  33310  ismbfm  33535  mbfmcst  33544  issibf  33618  sitgfval  33626  eulerpartlemelr  33642  eulerpartleme  33648  eulerpartlemo  33650  eulerpartlemt0  33654  eulerpartlemt  33656  eulerpartlemr  33659  eulerpartlemgf  33664  eulerpartlemgs2  33665  eulerpartlemn  33666  eulerpart  33667  ballotlemscr  33803  ballotlemrv  33804  ballotlemrinv0  33817  iscvm  34536  cvmliftmolem1  34558  cvmlift2lem9a  34580  cvmlift2lem9  34588  msrfval  34814  ismfs  34826  mthmval  34852  bj-imdirval2  36367  bj-iminvval2  36378  poimirlem4  36795  poimirlem5  36796  poimirlem6  36797  poimirlem7  36798  poimirlem8  36799  poimirlem10  36801  poimirlem11  36802  poimirlem12  36803  poimirlem13  36804  poimirlem14  36805  poimirlem15  36806  poimirlem16  36807  poimirlem17  36808  poimirlem18  36809  poimirlem19  36810  poimirlem20  36811  poimirlem21  36812  poimirlem22  36813  poimirlem26  36817  poimirlem27  36818  poimirlem32  36823  cnambfre  36839  itg2addnclem2  36843  ftc1anclem1  36864  ftc1anclem6  36869  lkrval  38261  prjcrvfval  41675  prjcrvval  41676  prjcrv0  41677  pw2f1o2val  42080  aomclem8  42105  pwfi2f1o  42140  trclimalb2  42779  frege131d  42817  colleq12d  43314  dirkercncflem2  45119  issmflem  45742  smfpimioo  45802  smfpimcc  45823  smfsuplem2  45827