Theorem fveq2d 5674

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 5670	. 2 ⊢ (𝐴 = 𝐵 → (𝐹‘𝐴) = (𝐹‘𝐵))
3	1, 2	syl 14	1 ⊢ (𝜑 → (𝐹‘𝐴) = (𝐹‘𝐵))

Syntax hints:   → wi 4   = wceq 1398  ‘cfv 5352

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 717  ax-5 1496  ax-7 1497  ax-gen 1498  ax-ie1 1542  ax-ie2 1543  ax-8 1553  ax-10 1554  ax-11 1555  ax-i12 1556  ax-bndl 1558  ax-4 1559  ax-17 1575  ax-i9 1579  ax-ial 1583  ax-i5r 1584  ax-ext 2214

This theorem depends on definitions:  df-bi 117  df-3an 1007  df-tru 1401  df-nf 1510  df-sb 1812  df-clab 2219  df-cleq 2225  df-clel 2228  df-nfc 2373  df-rex 2526  df-v 2815  df-un 3215  df-sn 3695  df-pr 3696  df-op 3698  df-uni 3915  df-br 4110  df-iota 5312  df-fv 5360

This theorem is referenced by:  2fveq3  5675  fveq12d  5677  fveqeq2d  5678  csbfvg  5712  fvmptdf  5765  fvmptt  5769  resfvresima  5923  fcof1  5956  oveq1  6057  oveq2  6058  fvoveq1d  6072  caofinvl  6292  op1stg  6344  op2ndg  6345  ot1stg  6346  ot2ndg  6347  eloprabi  6392  1stconst  6417  algrflemg  6426  tfrlem1  6539  tfrlem3ag  6540  tfrlem3a  6541  tfrlem9  6550  tfr0dm  6553  tfrlemisucaccv  6556  tfrlemiubacc  6561  tfrlemiex  6562  tfrlemi1  6563  tfr1onlem3ag  6568  tfr1onlemsucaccv  6572  tfr1onlemubacc  6577  tfr1onlemex  6578  tfr1onlemaccex  6579  tfrcllemsucaccv  6585  tfrcllembxssdm  6587  tfrcllemubacc  6590  tfrcllemex  6591  tfrcllemaccex  6592  tfrcllemres  6593  tfrcldm  6594  rdgivallem  6612  rdgival  6613  rdgss  6614  rdgisuc1  6615  rdgon  6617  rdg0  6618  frec0g  6628  frecabcl  6630  freccllem  6633  frecfcllem  6635  frecsuclem  6637  frecsuc  6638  frecrdg  6639  oav2  6696  omv2  6698  xpdom2  7082  xpmapenlem  7102  xpmapen  7103  ac6sfi  7155  1stinl  7365  2ndinl  7366  1stinr  7367  2ndinr  7368  updjudhcoinlf  7371  updjudhcoinrg  7372  caseinl  7382  caseinr  7383  omp1eomlem  7385  omp1eom  7386  difinfsn  7391  ctmlemr  7399  ctm  7400  ctssdclemn0  7401  ctssdccl  7402  nninfninc  7414  nnnninfeq  7419  nnnninfeq2  7420  enomnilem  7429  enmkvlem  7452  enwomnilem  7460  exmidfodomrlemeldju  7502  exmidfodomrlemreseldju  7503  exmidfodomrlemr  7505  exmidfodomrlemrALT  7506  exmidaclem  7515  cc2  7581  cc3  7582  ltdfpr  7821  genpelvl  7827  genpelvu  7828  recexpr  7953  cauappcvgprlem1  7974  caucvgprlemnkj  7981  caucvgprlemnbj  7982  caucvgprlemm  7983  caucvgprlemdisj  7989  caucvgprlemloc  7990  caucvgprlemcl  7991  caucvgprlemladdfu  7992  caucvgprlemladdrl  7993  caucvgprlem1  7994  caucvgprlem2  7995  caucvgpr  7997  caucvgprprlemell  8000  caucvgprprlemelu  8001  caucvgprprlemcbv  8002  caucvgprprlemval  8003  caucvgprprlemnkeqj  8005  caucvgprprlemmu  8010  caucvgprprlemopl  8012  caucvgprprlemlol  8013  caucvgprprlemopu  8014  caucvgprprlemloc  8018  caucvgprprlemclphr  8020  caucvgprprlemexbt  8021  caucvgprprlem1  8024  caucvgprprlem2  8025  caucvgsr  8117  axcaucvglemval  8212  axcaucvglemres  8214  fv0p1e1  9352  uzin  9887  cnref1o  9983  fzsuc2  10413  fseq1m1p1  10429  fzoss2  10508  elfzonlteqm1  10555  divfl0  10656  flqzadd  10658  fldiv4p1lem1div2  10665  ceilqval  10668  flqdiv  10683  modqval  10686  modqfrac  10699  modqmulnn  10704  modqid  10711  modqcyc  10721  modqdi  10754  frec2uzuzd  10764  frec2uzrdg  10771  frecuzrdgrcl  10772  frecuzrdgtcl  10774  frecuzrdgsuc  10776  frecuzrdgrclt  10777  frecuzrdgg  10778  frecuzrdgfunlem  10781  frecuzrdgsuctlem  10785  iseqovex  10820  iseqvalcbv  10821  seq3val  10822  seqvalcd  10823  seq3m1  10835  seq3shft2  10843  seqshft2g  10844  monoord  10847  monoord2  10848  iseqf1olemqval  10862  iseqf1olemab  10864  iseqf1olemqk  10869  iseqf1olemjpcl  10870  iseqf1olemqpcl  10871  iseqf1olemfvp  10872  seq3f1olemqsumkj  10873  seq3f1olemqsumk  10874  seq3f1olemqsum  10875  seq3f1olemp  10877  seq3f1oleml  10878  seqf1oglem1  10881  seqf1oglem2  10882  seqf1og  10883  seq3homo  10889  seqhomog  10892  exp3val  10903  expnegap0  10909  facnn2  11096  facwordi  11102  faclbnd6  11106  bcval  11111  bccmpl  11116  bcn0  11117  bcm1k  11122  bcp1n  11123  bcn2  11126  hashinfom  11141  hashennn  11143  hashsng  11161  omgadd  11166  hashprg  11173  fihashssdif  11183  hashdifpr  11185  hashfzo  11187  hashfzp1  11189  hashxp  11191  hashmap  11192  hashfibclem  11206  hashfibc  11207  zfz1isolemiso  11211  zfz1iso  11213  hashtpglem  11218  lsw1  11274  ccatfvalfi  11280  ccatlen  11283  ccatval3  11287  ccatval21sw  11293  ccatlid  11294  ccatass  11296  lswccatn0lsw  11299  lswccat0lsw  11300  ccatalpha  11301  s1leng  11312  ccats1val2  11328  lswccats1  11331  swrdfv0  11346  swrdfv2  11355  swrdsbslen  11358  swrds1  11360  ccatswrd  11362  pfxmpt  11372  pfxfv  11376  pfxtrcfvl  11389  ccatpfx  11393  swrdswrd  11397  lenpfxcctswrd  11403  ccatopth  11408  cats1un  11413  swrdccatin2  11421  pfxccatin12lem2  11423  shftval2  11511  shftval3  11512  shftval4  11513  shftval5  11514  seq3shft  11523  imval  11535  imre  11536  reim  11537  crim  11543  reim0  11546  mulreap  11549  recj  11552  reneg  11553  readd  11554  resub  11555  remullem  11556  redivap  11559  imcj  11560  imneg  11561  imadd  11562  imsub  11563  imdivap  11566  cjsub  11577  cjexp  11578  cjreim2  11589  cjap  11591  cjdivap  11594  cnrecnv  11595  cvg1nlemcau  11669  cvg1nlemres  11670  absval  11686  rennim  11687  sqrtdiv  11727  sqrtmsq  11730  absneg  11735  abscj  11737  absval2  11742  absreim  11753  absmul  11754  absdivap  11755  absid  11756  absre  11762  absexp  11764  absexpzap  11765  absimle  11769  abssub  11786  abs3dif  11790  abs2dif  11791  abs2dif2  11792  recan  11794  cau3lem  11799  max0addsup  11904  minabs  11921  bdtrilem  11924  clim  11966  clim2  11968  clim0  11970  clim0c  11971  climi0  11974  climconst  11975  climshftlemg  11987  climcn1  11993  climcn2  11994  addcn2  11995  subcn2  11996  mulcn2  11997  reccn2ap  11998  cjcn2  12001  recn2  12002  imcn2  12003  iser3shft  12031  climcau  12032  climcvg1nlem  12034  climcvg1n  12035  serf0  12037  fzf1o  12061  summodclem3  12066  summodclem2a  12067  summodc  12069  fsumf1o  12076  sumsnf  12095  fsumm1  12102  fsumcnv  12123  fsumabs  12151  fsumrelem  12157  iserabs  12161  hash2iun1dif1  12166  isumshft  12176  isumsplit  12177  expcnvap0  12188  expcnv  12190  cvgratnnlemseq  12212  cvgratnnlemrate  12216  cvgratz  12218  mertenslemub  12220  mertenslemi1  12221  mertenslem2  12222  mertensabs  12223  prodmodclem3  12261  fprodf1o  12274  prodsnf  12278  fprodm1  12284  fprodabs  12302  fprodcnv  12311  efcllemp  12344  efcj  12359  efaddlem  12360  efcan  12362  efsub  12367  efexp  12368  efzval  12369  efgt0  12370  eftlub  12376  efltim  12384  sinval  12388  cosval  12389  tanval3ap  12400  resinval  12401  recosval  12402  resin4p  12404  recos4p  12405  sinneg  12412  cosneg  12413  efmival  12419  efeul  12420  sinadd  12422  cosadd  12423  sinsub  12426  cossub  12427  addsin  12428  subsin  12429  addcos  12432  subcos  12433  sincossq  12434  sin2t  12435  cos2t  12436  sin01bnd  12443  cos01bnd  12444  sin02gt0  12450  cos12dec  12454  absefi  12455  absef  12456  absefib  12457  efieq1re  12458  demoivre  12459  demoivreALT  12460  flodddiv4  12622  bitsval  12629  bits0  12634  bitsp1  12637  bitsp1e  12638  bitsp1o  12639  bitsmod  12642  nninfctlemfo  12736  alginv  12744  algcvg  12745  eucalgval  12751  eucalginv  12753  eucalglt  12754  eucalgcvga  12755  eucalg  12756  lcmgcd  12775  lcm1  12778  sqpweven  12872  2sqpwodd  12873  sqne2sq  12874  qnumval  12882  qdenval  12883  qden1elz  12902  nn0sqrtelqelz  12903  phival  12910  dfphi2  12917  phiprmpw  12919  phiprm  12920  eulerthlemth  12929  hashgcdeq  12937  phisum  12938  pythagtriplem6  12968  pythagtriplem7  12969  pythagtriplem12  12973  pythagtriplem14  12975  fldivp1  13046  4sqlem11  13099  ennnfonelemg  13154  ennnfonelemp1  13157  ennnfonelemkh  13163  ennnfonelemhf1o  13164  ennnfonelemnn0  13173  ctinfomlemom  13178  ctiunctlemu1st  13185  ctiunctlemu2nd  13186  ctiunctlemudc  13188  ctiunctlemfo  13190  isstruct2im  13222  isstruct2r  13223  setsslid  13263  ressbasd  13280  resseqnbasd  13286  ressplusgd  13342  ptex  13477  prdsex  13482  prdsval  13486  prdsbas3  13500  pwsval  13504  pwsbas  13505  pwsplusgval  13508  pwsmulrval  13509  imasex  13518  imasival  13519  f1ocpbl  13524  f1ovscpbl  13525  imasaddvallemg  13528  qusval  13536  fvprif  13556  xpsff1o  13562  igsumvalx  13602  gsumprval  13612  pws0g  13664  imasmnd  13666  ismhm  13674  mhmpropd  13679  mhmlin  13680  mhmf1o  13683  resmhm  13700  mhmco  13703  gsumwmhm  13711  grpinvsub  13795  pwsinvg  13825  imasgrp2  13827  imasgrp  13828  mhmlem  13831  mhmid  13832  mhmmnd  13833  ghmgrp  13835  mulgfvalg  13838  mulgval  13839  mulgnegnn  13849  mulgneg  13857  mulgnegneg  13858  mulgm1  13859  mulginvcom  13864  mulgz  13867  mulgnndir  13868  mulgdir  13871  mulgass  13876  mhmmulg  13880  subgmulg  13905  isnsg  13919  eqgfval  13939  ghmlin  13965  ghmid  13966  ghminv  13967  ghmsub  13968  ghmmulg  13973  resghm  13977  ghmeql  13984  ablsub2inv  14028  ghmcmn  14044  invghm  14046  imasabl  14053  gsumfzreidx  14054  gsumfzmhm  14060  gsumsplit0  14063  mgpplusgg  14068  mgpbasg  14070  mgpscag  14071  mgptsetg  14072  mgpdsg  14074  rngm2neg  14093  imasrng  14100  isring  14144  ringm2neg  14199  imasring  14208  opprmulfvalg  14214  opprsllem  14218  isunitd  14251  opprunitd  14255  invrfvald  14267  rdivmuldivd  14289  rhmmul  14309  isrhm2d  14310  rhm1  14312  rhmdvdsr  14320  rhmopp  14321  rhmunitinv  14323  islmod  14439  islmodd  14441  scaffvalg  14454  lmodpropd  14497  lsssetm  14504  islssmd  14507  lssats2  14562  lspsnneg  14568  lspsnsub  14569  lspun0  14573  lmodindp1  14576  sralemg  14586  srascag  14590  sravscag  14591  sraipg  14592  rlmscabas  14608  ixpsnbasval  14614  2idlval  14650  2idlvalg  14651  mulgrhm2  14758  zlmlemg  14776  zlmsca  14780  zlmvscag  14781  znval  14784  znle  14785  znbaslemnn  14787  znidomb  14806  psrval  14814  psrbasg  14829  psrplusgg  14833  mplvalcoe  14845  mplsubgfileminv  14855  mpl0fi  14857  mplnegfi  14860  istps  14897  tpspropd  14901  eltpsg  14905  txvalex  15119  txval  15120  txbasval  15132  upxp  15137  uptx  15139  txrest  15141  cnmpt11  15148  cnmpt21  15156  hmeontr  15178  txhmeo  15184  psmetxrge0  15197  xmetunirn  15223  mopnval  15307  mopntopon  15308  isxms  15316  isxms2  15317  isms  15318  msrtri  15341  xmspropd  15342  mspropd  15343  setsmsbasg  15344  setsmsdsg  15345  setsmstsetg  15346  comet  15364  metcnpi  15380  metcnpi2  15381  cnbl0  15399  cnblcld  15400  resubmet  15421  mpomulcn  15431  elcncf  15438  cncfi  15443  rescncf  15446  mulc1cncf  15454  cncfco  15456  cncfmptid  15462  addccncf  15465  cdivcncfap  15469  negcncf  15470  mulcncflem  15472  ivthinclemlopn  15501  ivthinclemuopn  15503  limccl  15524  ellimc3apf  15525  limcimolemlt  15529  cnplimclemle  15533  limccnpcntop  15540  reldvg  15544  dvfvalap  15546  dveflem  15591  dvef  15592  plymullem1  15613  plycjlemc  15625  plycj  15626  plyrecj  15628  plyreres  15629  sin0pilem1  15646  ef2kpi  15671  sinperlem  15673  sin2kpi  15676  cos2kpi  15677  sin2pim  15678  cos2pim  15679  ptolemy  15689  sincosq2sgn  15692  sincosq3sgn  15693  sincosq4sgn  15694  sinq12gt0  15695  tangtx  15703  sincosq1eq  15704  abssinper  15711  sinkpi  15712  coskpi  15713  cosq34lt1  15715  relogeftb  15730  relogoprlem  15733  relogexp  15737  rpcxpef  15759  logcxp  15762  1cxp  15765  ecxp  15766  rpcxpadd  15770  rpmulcxp  15774  cxpmul  15777  abscxp  15780  logsqrt  15788  rpabscxpbnd  15805  rpcxplogb  15829  pellexlem1  15845  pellexlem2  15846  pellexlem3  15847  lgsval  15877  lgsval2lem  15883  lgsval4a  15895  lgsdi  15910  lgseisenlem3  15945  lgseisenlem4  15946  lgsquadlem1  15950  lgsquadlem2  15951  lgsquadlem3  15952  2lgslem1  15964  2lgslem3a  15966  2lgslem3b  15967  2lgslem3c  15968  2lgslem3d  15969  vtxdgfval  16283  vtxdgfifival  16286  vtxdgop  16287  vtxdgfi0e  16290  vtxdeqd  16291  vtxdfifiun  16292  vtxdumgrfival  16293  1hevtxdg1en  16303  iswlk  16318  2wlklem  16371  wlkres  16374  clwwlkccatlem  16395  clwwlkn2  16416  clwwlkext2edg  16417  umgr2cwwk2dif  16419  clwwlknonex2lem2  16433  eupth2fi  16474  eulerpathprum  16475  depindlem1  16501  depind  16504  nnsf  16783  peano4nninf  16784  peano3nninf  16785  nninfalllem1  16786  nninfall  16787  nninfsellemdc  16788  nninfsellemeq  16792  nninfsellemqall  16793  nninfsellemeqinf  16794  nninfsel  16795  nnnninfex  16800  exmidsbthr  16803  qdencn  16807  refeq  16808  repiecele0  16810  repiecege0  16811  repiecef  16812  isomninnlem  16814  apdifflemr  16831  apdiff  16832  qdiff  16833  ismkvnnlem  16837  nconstwlpolem  16851  gfsumval  16862  gsumgfsumlem  16865  gfsump1  16868