Theorem imaeq1d 5721

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

Syntax hints:   → wi 4   = wceq 1601   “ cima 5360

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1839  ax-4 1853  ax-5 1953  ax-6 2021  ax-7 2055  ax-9 2116  ax-10 2135  ax-11 2150  ax-12 2163  ax-13 2334  ax-ext 2754

This theorem depends on definitions:  df-bi 199  df-an 387  df-or 837  df-3an 1073  df-tru 1605  df-ex 1824  df-nf 1828  df-sb 2012  df-clab 2764  df-cleq 2770  df-clel 2774  df-nfc 2921  df-rab 3099  df-v 3400  df-dif 3795  df-un 3797  df-in 3799  df-ss 3806  df-nul 4142  df-if 4308  df-sn 4399  df-pr 4401  df-op 4405  df-br 4889  df-opab 4951  df-cnv 5365  df-dm 5367  df-rn 5368  df-res 5369  df-ima 5370

This theorem is referenced by:  imaeq12d  5723  nfimad  5731  csbrn  5852  f1imacnv  6409  foimacnv  6410  fimacnvinrn  6614  seqomeq12  7834  ssenen  8424  fipreima  8562  oieq1  8708  oieq2  8709  dfac12lem1  9302  dfac12r  9305  fpwwe2cbv  9789  fpwwe2lem2  9791  fpwwecbv  9803  fpwwelem  9804  seqeq1  13127  seqeq2  13128  seqeq3  13129  1arith  16046  vdwmc  16097  vdwnnlem1  16114  ramub2  16133  rami  16134  imasless  16597  gsumvalx  17667  eqglact  18040  psgnunilem1  18307  psrbag  19772  psrbaglefi  19780  evpmss  20338  psgnevpmb  20339  frlmup3  20554  iscn  21458  ptbasfi  21804  ptval2  21824  ptrescn  21862  xkoptsub  21877  qtopval  21918  cmphaushmeo  22023  ptcmpg  22280  restutopopn  22461  prdsxmslem2  22753  metuval  22773  nghmfval  22945  isnghm  22946  ismbf1  23839  ismbf  23843  mbfconst  23848  mbfres2  23860  cncombf  23873  isi1f  23889  itg1val  23898  deg1val  24304  fta1glem2  24374  fta1g  24375  fta1b  24377  dgrval  24432  dgrlem  24433  coeidlem  24441  coe11  24457  fta1lem  24510  fta1  24511  vieta1lem2  24514  vieta1  24515  taylthlem2  24576  areaval  25154  sqff1o  25371  nlfnval  29329  xppreima2  30032  ofpreima  30047  fpwrelmapffslem  30090  xrhval  30668  indf1ofs  30694  ismbfm  30920  mbfmcst  30927  issibf  31001  sitgfval  31009  eulerpartlemelr  31025  eulerpartleme  31031  eulerpartlemo  31033  eulerpartlemt0  31037  eulerpartlemt  31039  eulerpartlemr  31042  eulerpartlemgf  31047  eulerpartlemgs2  31048  eulerpartlemn  31049  eulerpart  31050  ballotlemscr  31187  ballotlemrv  31188  ballotlemrinv0  31201  iscvm  31848  cvmliftmolem1  31870  cvmlift2lem9a  31892  cvmlift2lem9  31900  msrfval  32041  ismfs  32053  mthmval  32079  poimirlem4  34048  poimirlem5  34049  poimirlem6  34050  poimirlem7  34051  poimirlem8  34052  poimirlem10  34054  poimirlem11  34055  poimirlem12  34056  poimirlem13  34057  poimirlem14  34058  poimirlem15  34059  poimirlem16  34060  poimirlem17  34061  poimirlem18  34062  poimirlem19  34063  poimirlem20  34064  poimirlem21  34065  poimirlem22  34066  poimirlem26  34070  poimirlem27  34071  poimirlem32  34076  cnambfre  34092  itg2addnclem2  34096  ftc1anclem1  34119  ftc1anclem6  34124  lkrval  35251  pw2f1o2val  38579  aomclem8  38604  pwfi2f1o  38639  trclimalb2  38989  frege131d  39027  dirkercncflem2  41262  issmflem  41877  smfpimioo  41935  smfpimcc  41955  smfsuplem2  41959