Theorem fveq2d 5694

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

Syntax hints:   → wi 4   = wceq 1402  ‘cfv 5372

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 721  ax-5 1500  ax-7 1501  ax-gen 1502  ax-ie1 1546  ax-ie2 1547  ax-8 1557  ax-10 1558  ax-11 1559  ax-i12 1560  ax-bndl 1562  ax-4 1563  ax-17 1579  ax-i9 1583  ax-ial 1587  ax-i5r 1588  ax-ext 2220

This theorem depends on definitions:  df-bi 117  df-3an 1011  df-tru 1405  df-nf 1514  df-sb 1816  df-clab 2225  df-cleq 2231  df-clel 2234  df-nfc 2381  df-rex 2534  df-v 2823  df-un 3224  df-sn 3711  df-pr 3712  df-op 3714  df-uni 3931  df-br 4126  df-iota 5332  df-fv 5380

This theorem is referenced by:  2fveq3  5695  fveq12d  5697  fveqeq2d  5698  csbfvg  5732  fvmptdf  5787  fvmptt  5791  resfvresima  5946  fcof1  5979  oveq1  6082  oveq2  6083  fvoveq1d  6097  caofinvl  6318  op1stg  6374  op2ndg  6375  ot1stg  6376  ot2ndg  6377  eloprabi  6422  1stconst  6447  algrflemg  6456  tfrlem1  6569  tfrlem3ag  6570  tfrlem3a  6571  tfrlem9  6580  tfr0dm  6583  tfrlemisucaccv  6586  tfrlemiubacc  6591  tfrlemiex  6592  tfrlemi1  6593  tfr1onlem3ag  6598  tfr1onlemsucaccv  6602  tfr1onlemubacc  6607  tfr1onlemex  6608  tfr1onlemaccex  6609  tfrcllemsucaccv  6615  tfrcllembxssdm  6617  tfrcllemubacc  6620  tfrcllemex  6621  tfrcllemaccex  6622  tfrcllemres  6623  tfrcldm  6624  rdgivallem  6642  rdgival  6643  rdgss  6644  rdgisuc1  6645  rdgon  6647  rdg0  6648  frec0g  6658  frecabcl  6660  freccllem  6663  frecfcllem  6665  frecsuclem  6667  frecsuc  6668  frecrdg  6669  oav2  6726  omv2  6728  xpdom2  7119  xpmapenlem  7139  xpmapen  7140  ac6sfi  7192  1stinl  7404  2ndinl  7405  1stinr  7406  2ndinr  7407  updjudhcoinlf  7410  updjudhcoinrg  7411  caseinl  7421  caseinr  7422  omp1eomlem  7424  omp1eom  7425  difinfsn  7430  ctmlemr  7438  ctm  7439  ctssdclemn0  7440  ctssdccl  7441  nninfninc  7453  nnnninfeq  7458  nnnninfeq2  7459  enomnilem  7468  enmkvlem  7491  enwomnilem  7499  exmidfodomrlemeldju  7541  exmidfodomrlemreseldju  7542  exmidfodomrlemr  7544  exmidfodomrlemrALT  7545  exmidaclem  7554  cc2  7623  cc3  7624  ltdfpr  7863  genpelvl  7869  genpelvu  7870  recexpr  7995  cauappcvgprlem1  8016  caucvgprlemnkj  8023  caucvgprlemnbj  8024  caucvgprlemm  8025  caucvgprlemdisj  8031  caucvgprlemloc  8032  caucvgprlemcl  8033  caucvgprlemladdfu  8034  caucvgprlemladdrl  8035  caucvgprlem1  8036  caucvgprlem2  8037  caucvgpr  8039  caucvgprprlemell  8042  caucvgprprlemelu  8043  caucvgprprlemcbv  8044  caucvgprprlemval  8045  caucvgprprlemnkeqj  8047  caucvgprprlemmu  8052  caucvgprprlemopl  8054  caucvgprprlemlol  8055  caucvgprprlemopu  8056  caucvgprprlemloc  8060  caucvgprprlemclphr  8062  caucvgprprlemexbt  8063  caucvgprprlem1  8066  caucvgprprlem2  8067  caucvgsr  8159  axcaucvglemval  8254  axcaucvglemres  8256  fv0p1e1  9398  uzin  9934  cnref1o  10030  fzsuc2  10464  fseq1m1p1  10480  fzoss2  10559  elfzonlteqm1  10606  divfl0  10709  flqzadd  10711  fldiv4p1lem1div2  10718  ceilqval  10721  flqdiv  10736  modqval  10739  modqfrac  10752  modqmulnn  10757  modqid  10764  modqcyc  10774  modqdi  10807  frec2uzuzd  10817  frec2uzrdg  10824  frecuzrdgrcl  10825  frecuzrdgtcl  10827  frecuzrdgsuc  10829  frecuzrdgrclt  10830  frecuzrdgg  10831  frecuzrdgfunlem  10834  frecuzrdgsuctlem  10838  iseqovex  10873  iseqvalcbv  10874  seq3val  10875  seqvalcd  10876  seq3m1  10888  seq3shft2  10896  seqshft2g  10897  monoord  10900  monoord2  10901  iseqf1olemqval  10915  iseqf1olemab  10917  iseqf1olemqk  10922  iseqf1olemjpcl  10923  iseqf1olemqpcl  10924  iseqf1olemfvp  10925  seq3f1olemqsumkj  10926  seq3f1olemqsumk  10927  seq3f1olemqsum  10928  seq3f1olemp  10930  seq3f1oleml  10931  seqf1oglem1  10934  seqf1oglem2  10935  seqf1og  10936  seq3homo  10942  seqhomog  10945  exp3val  10956  expnegap0  10962  facnn2  11150  facwordi  11156  faclbnd6  11160  bcval  11165  bccmpl  11170  bcn0  11171  bcm1k  11176  bcp1n  11177  bcn2  11180  hashinfom  11195  hashennn  11197  hashsng  11215  omgadd  11220  hashprg  11227  fihashssdif  11237  hashdifpr  11239  hashfzo  11241  hashfzp1  11243  hashxp  11245  hashmap  11246  hashfibclem  11260  hashfibc  11261  hashf1lem2  11264  hashf1  11265  hashfac  11266  zfz1isolemiso  11269  zfz1iso  11271  hashtpglem  11276  lsw1  11332  ccatfvalfi  11338  ccatlen  11341  ccatval3  11345  ccatval21sw  11351  ccatlid  11352  ccatass  11354  lswccatn0lsw  11357  lswccat0lsw  11358  ccatalpha  11359  s1leng  11370  ccats1val2  11386  lswccats1  11389  swrdfv0  11404  swrdfv2  11413  swrdsbslen  11416  swrds1  11418  ccatswrd  11420  pfxmpt  11430  pfxfv  11434  pfxtrcfvl  11447  ccatpfx  11451  swrdswrd  11455  lenpfxcctswrd  11461  ccatopth  11466  cats1un  11471  swrdccatin2  11479  pfxccatin12lem2  11481  shftval2  11569  shftval3  11570  shftval4  11571  shftval5  11572  seq3shft  11581  imval  11593  imre  11594  reim  11595  crim  11601  reim0  11604  mulreap  11607  recj  11610  reneg  11611  readd  11612  resub  11613  remullem  11614  redivap  11617  imcj  11618  imneg  11619  imadd  11620  imsub  11621  imdivap  11624  cjsub  11635  cjexp  11636  cjreim2  11648  cjap  11650  cjdivap  11653  cnrecnv  11654  cvg1nlemcau  11728  cvg1nlemres  11729  absval  11745  rennim  11746  sqrtdiv  11786  sqrtmsq  11789  absneg  11794  abscj  11796  absval2  11801  absreim  11812  absmul  11813  absdivap  11814  absid  11815  absre  11821  absexp  11823  absexpzap  11824  absimle  11828  abssub  11845  abs3dif  11849  abs2dif  11850  abs2dif2  11851  recan  11853  cau3lem  11858  max0addsup  11963  minabs  11980  bdtrilem  11983  clim  12025  clim2  12027  clim0  12029  clim0c  12030  climi0  12033  climconst  12034  climshftlemg  12046  climcn1  12052  climcn2  12053  addcn2  12054  subcn2  12055  mulcn2  12056  reccn2ap  12057  cjcn2  12060  recn2  12061  imcn2  12062  iser3shft  12090  climcau  12091  climcvg1nlem  12093  climcvg1n  12094  serf0  12096  fzf1o  12120  summodclem3  12125  summodclem2a  12126  summodc  12128  fsumf1o  12135  sumsnf  12154  fsumm1  12161  fsumcnv  12182  fsumabs  12210  fsumrelem  12216  iserabs  12220  hash2iun1dif1  12225  isumshft  12235  isumsplit  12236  expcnvap0  12247  expcnv  12249  cvgratnnlemseq  12271  cvgratnnlemrate  12275  cvgratz  12277  mertenslemub  12279  mertenslemi1  12280  mertenslem2  12281  mertensabs  12282  prodmodclem3  12320  fprodf1o  12333  prodsnf  12337  fprodm1  12343  fprodabs  12361  fprodcnv  12370  efcllemp  12403  efcj  12418  efaddlem  12419  efcan  12421  efsub  12426  efexp  12427  efzval  12428  efgt0  12429  eftlub  12435  efltim  12443  sinval  12447  cosval  12448  tanval3ap  12459  resinval  12460  recosval  12461  resin4p  12463  recos4p  12464  sinneg  12471  cosneg  12472  efmival  12478  efeul  12479  sinadd  12481  cosadd  12482  sinsub  12485  cossub  12486  addsin  12487  subsin  12488  addcos  12491  subcos  12492  sincossq  12493  sin2t  12494  cos2t  12495  sin01bnd  12502  cos01bnd  12503  sin02gt0  12509  cos12dec  12513  absefi  12514  absef  12515  absefib  12516  efieq1re  12517  demoivre  12518  demoivreALT  12519  flodddiv4  12681  bitsval  12688  bits0  12693  bitsp1  12696  bitsp1e  12697  bitsp1o  12698  bitsmod  12701  nninfctlemfo  12795  alginv  12803  algcvg  12804  eucalgval  12810  eucalginv  12812  eucalglt  12813  eucalgcvga  12814  eucalg  12815  lcmgcd  12834  lcm1  12837  sqpweven  12931  2sqpwodd  12932  sqne2sq  12933  qnumval  12941  qdenval  12942  qden1elz  12961  nn0sqrtelqelz  12962  phival  12969  dfphi2  12976  phiprmpw  12978  phiprm  12979  eulerthlemth  12988  hashgcdeq  12996  phisum  12997  pythagtriplem6  13027  pythagtriplem7  13028  pythagtriplem12  13032  pythagtriplem14  13034  fldivp1  13105  4sqlem11  13158  ballotfilemfval  13207  ballotfilemfp1  13209  ballotfilemfc0  13210  ballotfilemfcc  13211  ballotfilemfmpn  13212  ballotfilemsval  13230  ballotfilemgval  13245  ballotfilemgun  13246  ballotfilemfrc  13248  ballotfilemrinv0  13254  ennnfonelemg  13272  ennnfonelemp1  13275  ennnfonelemkh  13281  ennnfonelemhf1o  13282  ennnfonelemnn0  13291  ctinfomlemom  13296  ctiunctlemu1st  13303  ctiunctlemu2nd  13304  ctiunctlemudc  13306  ctiunctlemfo  13308  isstruct2im  13340  isstruct2r  13341  setsslid  13381  ressbasd  13398  resseqnbasd  13404  ressplusgd  13460  ptex  13595  imasex  13603  imasival  13604  f1ocpbl  13609  f1ovscpbl  13610  imasaddvallemg  13613  qusval  13621  fvprif  13641  xpsff1o  13647  gzsumvalx  13686  imasmnd  13737  ismhm  13745  mhmpropd  13750  mhmlin  13751  mhmf1o  13754  resmhm  13771  mhmco  13774  gzsumwmhm  13780  grpinvsub  13864  imasgrp2  13890  imasgrp  13891  mhmlem  13894  mhmid  13895  mhmmnd  13896  ghmgrp  13898  mulgfvalg  13901  mulgval  13902  mulgnegnn  13912  mulgneg  13920  mulgnegneg  13921  mulgm1  13922  mulginvcom  13927  mulgz  13930  mulgnndir  13931  mulgdir  13934  mulgass  13939  mhmmulg  13943  subgmulg  13968  isnsg  13982  eqgfval  14002  ghmlin  14028  ghmid  14029  ghminv  14030  ghmsub  14031  ghmmulg  14036  resghm  14040  ghmeql  14047  ablsub2inv  14092  ghmcmn  14108  invghm  14110  imasabl  14117  gzsumreidx  14118  gzsummhm  14122  gzsumsplit0  14125  gzsumshift  14126  gsumvalfi  14129  gsump1  14134  gsumf1ofi  14137  gsummhmfi  14141  prdsex  14149  prdsval  14150  prdsbas3  14164  pwsval  14181  pwsbas  14182  pwsplusgval  14185  pwsmulrval  14186  pws0g  14190  pwsinvg  14192  mgpplusgg  14198  mgpbasg  14200  mgpscag  14201  mgptsetg  14202  mgpdsg  14204  rngm2neg  14223  imasrng  14230  isring  14278  ringm2neg  14333  imasring  14342  opprmulfvalg  14348  opprsllem  14352  isunitd  14386  opprunitd  14390  invrfvald  14402  rdivmuldivd  14424  rhmmul  14444  isrhm2d  14445  rhm1  14447  rhmdvdsr  14455  rhmopp  14456  rhmunitinv  14458  islmod  14600  islmodd  14602  scaffvalg  14615  lmodpropd  14658  lsssetm  14665  islssmd  14668  lssats2  14723  lspsnneg  14729  lspsnsub  14730  lspun0  14734  lmodindp1  14737  sralemg  14747  srascag  14751  sravscag  14752  sraipg  14753  rlmscabas  14769  ixpsnbasval  14775  2idlval  14811  2idlvalg  14812  mulgrhm2  14917  zlmlemg  14935  zlmsca  14939  zlmvscag  14940  znval  14943  znle  14944  znbaslemnn  14946  znidomb  14965  psrval  14973  psrbasg  14988  psrplusgg  14992  mplvalcoe  15004  mplsubgfileminv  15014  mpl0fi  15016  mplnegfi  15019  istps  15056  tpspropd  15060  eltpsg  15064  txvalex  15278  txval  15279  txbasval  15291  upxp  15296  uptx  15298  txrest  15300  cnmpt11  15307  cnmpt21  15315  hmeontr  15337  txhmeo  15343  psmetxrge0  15356  xmetunirn  15382  mopnval  15466  mopntopon  15467  isxms  15475  isxms2  15476  isms  15477  msrtri  15500  xmspropd  15501  mspropd  15502  setsmsbasg  15503  setsmsdsg  15504  setsmstsetg  15505  comet  15523  metcnpi  15539  metcnpi2  15540  cnbl0  15558  cnblcld  15559  resubmet  15580  mpomulcn  15590  elcncf  15597  cncfi  15602  rescncf  15605  mulc1cncf  15613  cncfco  15615  cncfmptid  15621  addccncf  15624  cdivcncfap  15628  negcncf  15629  mulcncflem  15631  ivthinclemlopn  15660  ivthinclemuopn  15662  limccl  15683  ellimc3apf  15684  limcimolemlt  15688  cnplimclemle  15692  limccnpcntop  15699  reldvg  15703  dvfvalap  15705  dveflem  15750  dvef  15751  plymullem1  15772  plycjlemc  15784  plycj  15785  plyrecj  15787  plyreres  15788  sin0pilem1  15805  ef2kpi  15830  sinperlem  15832  sin2kpi  15835  cos2kpi  15836  sin2pim  15837  cos2pim  15838  ptolemy  15848  sincosq2sgn  15851  sincosq3sgn  15852  sincosq4sgn  15853  sinq12gt0  15854  tangtx  15862  sincosq1eq  15863  abssinper  15870  sinkpi  15871  coskpi  15872  cosq34lt1  15874  relogeftb  15889  relogoprlem  15892  relogexp  15896  logfac  15918  rpcxpef  15919  logcxp  15922  1cxp  15925  ecxp  15926  rpcxpadd  15930  rpmulcxp  15934  cxpmul  15937  abscxp  15940  logsqrt  15948  rpabscxpbnd  15965  rpcxplogb  15989  pellexlem1  16005  pellexlem2  16006  pellexlem3  16007  lgsval  16037  lgsval2lem  16043  lgsval4a  16055  lgsdi  16070  lgseisenlem3  16105  lgseisenlem4  16106  lgsquadlem1  16110  lgsquadlem2  16111  lgsquadlem3  16112  2lgslem1  16124  2lgslem3a  16126  2lgslem3b  16127  2lgslem3c  16128  2lgslem3d  16129  vtxdgfval  16443  vtxdgfifival  16446  vtxdgop  16447  vtxdgfi0e  16450  vtxdeqd  16451  vtxdfifiun  16452  vtxdumgrfival  16453  1hevtxdg1en  16463  iswlk  16478  2wlklem  16531  wlkres  16534  clwwlkccatlem  16555  clwwlkn2  16576  clwwlkext2edg  16577  umgr2cwwk2dif  16579  clwwlknonex2lem2  16593  eupth2fi  16634  eulerpathprum  16635  depindlem1  16661  depind  16664  nnsf  16953  peano4nninf  16954  peano3nninf  16955  nninfalllem1  16956  nninfall  16957  nninfsellemdc  16958  nninfsellemeq  16962  nninfsellemqall  16963  nninfsellemeqinf  16964  nninfsel  16965  nnnninfex  16970  exmidsbthr  16973  qdencn  16977  refeq  16978  repiecele0  16980  repiecege0  16981  repiecef  16982  isomninnlem  16984  apdifflemr  17001  apdiff  17002  qdiff  17003  ismkvnnlem  17007  nconstwlpolem  17020