Theorem fveq2d 5643

Description: Equality deduction for function value. (Contributed by NM, 29-May-1999.)

Hypothesis

Ref	Expression
fveq2d.1	⊢ (𝜑 → 𝐴 = 𝐵)

Assertion

Ref	Expression
fveq2d	⊢ (𝜑 → (𝐹‘𝐴) = (𝐹‘𝐵))

Proof of Theorem fveq2d

Step	Hyp	Ref	Expression
1		fveq2d.1	. 2 ⊢ (𝜑 → 𝐴 = 𝐵)
2		fveq2 5639	. 2 ⊢ (𝐴 = 𝐵 → (𝐹‘𝐴) = (𝐹‘𝐵))
3	1, 2	syl 14	1 ⊢ (𝜑 → (𝐹‘𝐴) = (𝐹‘𝐵))

Syntax hints:   → wi 4   = wceq 1397  ‘cfv 5326

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-ia1 106  ax-ia2 107  ax-ia3 108  ax-io 716  ax-5 1495  ax-7 1496  ax-gen 1497  ax-ie1 1541  ax-ie2 1542  ax-8 1552  ax-10 1553  ax-11 1554  ax-i12 1555  ax-bndl 1557  ax-4 1558  ax-17 1574  ax-i9 1578  ax-ial 1582  ax-i5r 1583  ax-ext 2213

This theorem depends on definitions:  df-bi 117  df-3an 1006  df-tru 1400  df-nf 1509  df-sb 1811  df-clab 2218  df-cleq 2224  df-clel 2227  df-nfc 2363  df-rex 2516  df-v 2804  df-un 3204  df-sn 3675  df-pr 3676  df-op 3678  df-uni 3894  df-br 4089  df-iota 5286  df-fv 5334

This theorem is referenced by:  2fveq3  5644  fveq12d  5646  fveqeq2d  5647  csbfvg  5681  fvmptdf  5734  fvmptt  5738  resfvresima  5890  fcof1  5923  oveq1  6024  oveq2  6025  fvoveq1d  6039  caofinvl  6260  op1stg  6312  op2ndg  6313  ot1stg  6314  ot2ndg  6315  eloprabi  6360  1stconst  6385  algrflemg  6394  tfrlem1  6473  tfrlem3ag  6474  tfrlem3a  6475  tfrlem9  6484  tfr0dm  6487  tfrlemisucaccv  6490  tfrlemiubacc  6495  tfrlemiex  6496  tfrlemi1  6497  tfr1onlem3ag  6502  tfr1onlemsucaccv  6506  tfr1onlemubacc  6511  tfr1onlemex  6512  tfr1onlemaccex  6513  tfrcllemsucaccv  6519  tfrcllembxssdm  6521  tfrcllemubacc  6524  tfrcllemex  6525  tfrcllemaccex  6526  tfrcllemres  6527  tfrcldm  6528  rdgivallem  6546  rdgival  6547  rdgss  6548  rdgisuc1  6549  rdgon  6551  rdg0  6552  frec0g  6562  frecabcl  6564  freccllem  6567  frecfcllem  6569  frecsuclem  6571  frecsuc  6572  frecrdg  6573  oav2  6630  omv2  6632  xpdom2  7014  xpmapenlem  7034  xpmapen  7035  ac6sfi  7086  1stinl  7272  2ndinl  7273  1stinr  7274  2ndinr  7275  updjudhcoinlf  7278  updjudhcoinrg  7279  caseinl  7289  caseinr  7290  omp1eomlem  7292  omp1eom  7293  difinfsn  7298  ctmlemr  7306  ctm  7307  ctssdclemn0  7308  ctssdccl  7309  nninfninc  7321  nnnninfeq  7326  nnnninfeq2  7327  enomnilem  7336  enmkvlem  7359  enwomnilem  7367  exmidfodomrlemeldju  7409  exmidfodomrlemreseldju  7410  exmidfodomrlemr  7412  exmidfodomrlemrALT  7413  exmidaclem  7422  cc2  7485  cc3  7486  ltdfpr  7725  genpelvl  7731  genpelvu  7732  recexpr  7857  cauappcvgprlem1  7878  caucvgprlemnkj  7885  caucvgprlemnbj  7886  caucvgprlemm  7887  caucvgprlemdisj  7893  caucvgprlemloc  7894  caucvgprlemcl  7895  caucvgprlemladdfu  7896  caucvgprlemladdrl  7897  caucvgprlem1  7898  caucvgprlem2  7899  caucvgpr  7901  caucvgprprlemell  7904  caucvgprprlemelu  7905  caucvgprprlemcbv  7906  caucvgprprlemval  7907  caucvgprprlemnkeqj  7909  caucvgprprlemmu  7914  caucvgprprlemopl  7916  caucvgprprlemlol  7917  caucvgprprlemopu  7918  caucvgprprlemloc  7922  caucvgprprlemclphr  7924  caucvgprprlemexbt  7925  caucvgprprlem1  7928  caucvgprprlem2  7929  caucvgsr  8021  axcaucvglemval  8116  axcaucvglemres  8118  fv0p1e1  9257  uzin  9788  cnref1o  9884  fzsuc2  10313  fseq1m1p1  10329  fzoss2  10408  elfzonlteqm1  10454  divfl0  10555  flqzadd  10557  fldiv4p1lem1div2  10564  ceilqval  10567  flqdiv  10582  modqval  10585  modqfrac  10598  modqmulnn  10603  modqid  10610  modqcyc  10620  modqdi  10653  frec2uzuzd  10663  frec2uzrdg  10670  frecuzrdgrcl  10671  frecuzrdgtcl  10673  frecuzrdgsuc  10675  frecuzrdgrclt  10676  frecuzrdgg  10677  frecuzrdgfunlem  10680  frecuzrdgsuctlem  10684  iseqovex  10719  iseqvalcbv  10720  seq3val  10721  seqvalcd  10722  seq3m1  10734  seq3shft2  10742  seqshft2g  10743  monoord  10746  monoord2  10747  iseqf1olemqval  10761  iseqf1olemab  10763  iseqf1olemqk  10768  iseqf1olemjpcl  10769  iseqf1olemqpcl  10770  iseqf1olemfvp  10771  seq3f1olemqsumkj  10772  seq3f1olemqsumk  10773  seq3f1olemqsum  10774  seq3f1olemp  10776  seq3f1oleml  10777  seqf1oglem1  10780  seqf1oglem2  10781  seqf1og  10782  seq3homo  10788  seqhomog  10791  exp3val  10802  expnegap0  10808  facnn2  10995  facwordi  11001  faclbnd6  11005  bcval  11010  bccmpl  11015  bcn0  11016  bcm1k  11021  bcp1n  11022  bcn2  11025  hashinfom  11039  hashennn  11041  hashsng  11059  omgadd  11064  hashprg  11071  fihashssdif  11081  hashdifpr  11083  hashfzo  11085  hashfzp1  11087  hashxp  11089  zfz1isolemiso  11102  zfz1iso  11104  lsw1  11162  ccatfvalfi  11168  ccatlen  11171  ccatval3  11175  ccatval21sw  11181  ccatlid  11182  ccatass  11184  lswccatn0lsw  11187  lswccat0lsw  11188  ccatalpha  11189  s1leng  11200  ccats1val2  11216  lswccats1  11219  swrdfv0  11234  swrdfv2  11243  swrdsbslen  11246  swrds1  11248  ccatswrd  11250  pfxmpt  11260  pfxfv  11264  pfxtrcfvl  11277  ccatpfx  11281  swrdswrd  11285  lenpfxcctswrd  11291  ccatopth  11296  cats1un  11301  swrdccatin2  11309  pfxccatin12lem2  11311  shftval2  11386  shftval3  11387  shftval4  11388  shftval5  11389  seq3shft  11398  imval  11410  imre  11411  reim  11412  crim  11418  reim0  11421  mulreap  11424  recj  11427  reneg  11428  readd  11429  resub  11430  remullem  11431  redivap  11434  imcj  11435  imneg  11436  imadd  11437  imsub  11438  imdivap  11441  cjsub  11452  cjexp  11453  cjreim2  11464  cjap  11466  cjdivap  11469  cnrecnv  11470  cvg1nlemcau  11544  cvg1nlemres  11545  absval  11561  rennim  11562  sqrtdiv  11602  sqrtmsq  11605  absneg  11610  abscj  11612  absval2  11617  absreim  11628  absmul  11629  absdivap  11630  absid  11631  absre  11637  absexp  11639  absexpzap  11640  absimle  11644  abssub  11661  abs3dif  11665  abs2dif  11666  abs2dif2  11667  recan  11669  cau3lem  11674  max0addsup  11779  minabs  11796  bdtrilem  11799  clim  11841  clim2  11843  clim0  11845  clim0c  11846  climi0  11849  climconst  11850  climshftlemg  11862  climcn1  11868  climcn2  11869  addcn2  11870  subcn2  11871  mulcn2  11872  reccn2ap  11873  cjcn2  11876  recn2  11877  imcn2  11878  iser3shft  11906  climcau  11907  climcvg1nlem  11909  climcvg1n  11910  serf0  11912  summodclem3  11940  summodclem2a  11941  summodc  11943  fsumf1o  11950  sumsnf  11969  fsumm1  11976  fsumcnv  11997  fsumabs  12025  fsumrelem  12031  iserabs  12035  hash2iun1dif1  12040  isumshft  12050  isumsplit  12051  expcnvap0  12062  expcnv  12064  cvgratnnlemseq  12086  cvgratnnlemrate  12090  cvgratz  12092  mertenslemub  12094  mertenslemi1  12095  mertenslem2  12096  mertensabs  12097  prodmodclem3  12135  fprodf1o  12148  prodsnf  12152  fprodm1  12158  fprodabs  12176  fprodcnv  12185  efcllemp  12218  efcj  12233  efaddlem  12234  efcan  12236  efsub  12241  efexp  12242  efzval  12243  efgt0  12244  eftlub  12250  efltim  12258  sinval  12262  cosval  12263  tanval3ap  12274  resinval  12275  recosval  12276  resin4p  12278  recos4p  12279  sinneg  12286  cosneg  12287  efmival  12293  efeul  12294  sinadd  12296  cosadd  12297  sinsub  12300  cossub  12301  addsin  12302  subsin  12303  addcos  12306  subcos  12307  sincossq  12308  sin2t  12309  cos2t  12310  sin01bnd  12317  cos01bnd  12318  sin02gt0  12324  cos12dec  12328  absefi  12329  absef  12330  absefib  12331  efieq1re  12332  demoivre  12333  demoivreALT  12334  flodddiv4  12496  bitsval  12503  bits0  12508  bitsp1  12511  bitsp1e  12512  bitsp1o  12513  bitsmod  12516  nninfctlemfo  12610  alginv  12618  algcvg  12619  eucalgval  12625  eucalginv  12627  eucalglt  12628  eucalgcvga  12629  eucalg  12630  lcmgcd  12649  lcm1  12652  sqpweven  12746  2sqpwodd  12747  sqne2sq  12748  qnumval  12756  qdenval  12757  qden1elz  12776  nn0sqrtelqelz  12777  phival  12784  dfphi2  12791  phiprmpw  12793  phiprm  12794  eulerthlemth  12803  hashgcdeq  12811  phisum  12812  pythagtriplem6  12842  pythagtriplem7  12843  pythagtriplem12  12847  pythagtriplem14  12849  fldivp1  12920  4sqlem11  12973  ennnfonelemg  13023  ennnfonelemp1  13026  ennnfonelemkh  13032  ennnfonelemhf1o  13033  ennnfonelemnn0  13042  ctinfomlemom  13047  ctiunctlemu1st  13054  ctiunctlemu2nd  13055  ctiunctlemudc  13057  ctiunctlemfo  13059  isstruct2im  13091  isstruct2r  13092  setsslid  13132  ressbasd  13149  resseqnbasd  13155  ressplusgd  13211  ptex  13346  prdsex  13351  prdsval  13355  prdsbas3  13369  pwsval  13373  pwsbas  13374  pwsplusgval  13377  pwsmulrval  13378  imasex  13387  imasival  13388  f1ocpbl  13393  f1ovscpbl  13394  imasaddvallemg  13397  qusval  13405  fvprif  13425  xpsff1o  13431  igsumvalx  13471  gsumprval  13481  pws0g  13533  imasmnd  13535  ismhm  13543  mhmpropd  13548  mhmlin  13549  mhmf1o  13552  resmhm  13569  mhmco  13572  gsumwmhm  13580  grpinvsub  13664  pwsinvg  13694  imasgrp2  13696  imasgrp  13697  mhmlem  13700  mhmid  13701  mhmmnd  13702  ghmgrp  13704  mulgfvalg  13707  mulgval  13708  mulgnegnn  13718  mulgneg  13726  mulgnegneg  13727  mulgm1  13728  mulginvcom  13733  mulgz  13736  mulgnndir  13737  mulgdir  13740  mulgass  13745  mhmmulg  13749  subgmulg  13774  isnsg  13788  eqgfval  13808  ghmlin  13834  ghmid  13835  ghminv  13836  ghmsub  13837  ghmmulg  13842  resghm  13846  ghmeql  13853  ablsub2inv  13897  ghmcmn  13913  invghm  13915  imasabl  13922  gsumfzreidx  13923  gsumfzmhm  13929  mgpplusgg  13936  mgpbasg  13938  mgpscag  13939  mgptsetg  13940  mgpdsg  13942  rngm2neg  13961  imasrng  13968  isring  14012  ringm2neg  14067  imasring  14076  opprmulfvalg  14082  opprsllem  14086  isunitd  14119  opprunitd  14123  invrfvald  14135  rdivmuldivd  14157  rhmmul  14177  isrhm2d  14178  rhm1  14180  rhmdvdsr  14188  rhmopp  14189  rhmunitinv  14191  islmod  14304  islmodd  14306  scaffvalg  14319  lmodpropd  14362  lsssetm  14369  islssmd  14372  lssats2  14427  lspsnneg  14433  lspsnsub  14434  lspun0  14438  lmodindp1  14441  sralemg  14451  srascag  14455  sravscag  14456  sraipg  14457  rlmscabas  14473  ixpsnbasval  14479  2idlval  14515  2idlvalg  14516  mulgrhm2  14623  zlmlemg  14641  zlmsca  14645  zlmvscag  14646  znval  14649  znle  14650  znbaslemnn  14652  znidomb  14671  psrval  14679  psrbasg  14687  psrplusgg  14691  mplvalcoe  14703  mplsubgfileminv  14713  mpl0fi  14715  mplnegfi  14718  istps  14755  tpspropd  14759  eltpsg  14763  txvalex  14977  txval  14978  txbasval  14990  upxp  14995  uptx  14997  txrest  14999  cnmpt11  15006  cnmpt21  15014  hmeontr  15036  txhmeo  15042  psmetxrge0  15055  xmetunirn  15081  mopnval  15165  mopntopon  15166  isxms  15174  isxms2  15175  isms  15176  msrtri  15199  xmspropd  15200  mspropd  15201  setsmsbasg  15202  setsmsdsg  15203  setsmstsetg  15204  comet  15222  metcnpi  15238  metcnpi2  15239  cnbl0  15257  cnblcld  15258  resubmet  15279  mpomulcn  15289  elcncf  15296  cncfi  15301  rescncf  15304  mulc1cncf  15312  cncfco  15314  cncfmptid  15320  addccncf  15323  cdivcncfap  15327  negcncf  15328  mulcncflem  15330  ivthinclemlopn  15359  ivthinclemuopn  15361  limccl  15382  ellimc3apf  15383  limcimolemlt  15387  cnplimclemle  15391  limccnpcntop  15398  reldvg  15402  dvfvalap  15404  dveflem  15449  dvef  15450  plymullem1  15471  plycjlemc  15483  plycj  15484  plyrecj  15486  plyreres  15487  sin0pilem1  15504  ef2kpi  15529  sinperlem  15531  sin2kpi  15534  cos2kpi  15535  sin2pim  15536  cos2pim  15537  ptolemy  15547  sincosq2sgn  15550  sincosq3sgn  15551  sincosq4sgn  15552  sinq12gt0  15553  tangtx  15561  sincosq1eq  15562  abssinper  15569  sinkpi  15570  coskpi  15571  cosq34lt1  15573  relogeftb  15588  relogoprlem  15591  relogexp  15595  rpcxpef  15617  logcxp  15620  1cxp  15623  ecxp  15624  rpcxpadd  15628  rpmulcxp  15632  cxpmul  15635  abscxp  15638  logsqrt  15646  rpabscxpbnd  15663  rpcxplogb  15687  lgsval  15732  lgsval2lem  15738  lgsval4a  15750  lgsdi  15765  lgseisenlem3  15800  lgseisenlem4  15801  lgsquadlem1  15805  lgsquadlem2  15806  lgsquadlem3  15807  2lgslem1  15819  2lgslem3a  15821  2lgslem3b  15822  2lgslem3c  15823  2lgslem3d  15824  vtxdgfval  16138  vtxdgfifival  16141  vtxdgop  16142  vtxdgfi0e  16145  vtxdeqd  16146  vtxdfifiun  16147  vtxdumgrfival  16148  1hevtxdg1en  16158  iswlk  16173  2wlklem  16226  wlkres  16229  clwwlkccatlem  16250  clwwlkn2  16271  clwwlkext2edg  16272  umgr2cwwk2dif  16274  clwwlknonex2lem2  16288  nnsf  16607  peano4nninf  16608  peano3nninf  16609  nninfalllem1  16610  nninfall  16611  nninfsellemdc  16612  nninfsellemeq  16616  nninfsellemqall  16617  nninfsellemeqinf  16618  nninfsel  16619  nnnninfex  16624  exmidsbthr  16627  qdencn  16631  refeq  16632  isomninnlem  16634  apdifflemr  16651  apdiff  16652  ismkvnnlem  16656  nconstwlpolem  16669  gfsumval  16680  gsumgfsumlem  16683