Theorem fveq2d 5639

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

Syntax hints:   → wi 4   = wceq 1395  ‘cfv 5324

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 714  ax-5 1493  ax-7 1494  ax-gen 1495  ax-ie1 1539  ax-ie2 1540  ax-8 1550  ax-10 1551  ax-11 1552  ax-i12 1553  ax-bndl 1555  ax-4 1556  ax-17 1572  ax-i9 1576  ax-ial 1580  ax-i5r 1581  ax-ext 2211

This theorem depends on definitions:  df-bi 117  df-3an 1004  df-tru 1398  df-nf 1507  df-sb 1809  df-clab 2216  df-cleq 2222  df-clel 2225  df-nfc 2361  df-rex 2514  df-v 2802  df-un 3202  df-sn 3673  df-pr 3674  df-op 3676  df-uni 3892  df-br 4087  df-iota 5284  df-fv 5332

This theorem is referenced by:  2fveq3  5640  fveq12d  5642  fveqeq2d  5643  csbfvg  5677  fvmptdf  5730  fvmptt  5734  resfvresima  5886  fcof1  5919  oveq1  6020  oveq2  6021  fvoveq1d  6035  caofinvl  6256  op1stg  6308  op2ndg  6309  ot1stg  6310  ot2ndg  6311  eloprabi  6356  1stconst  6381  algrflemg  6390  tfrlem1  6469  tfrlem3ag  6470  tfrlem3a  6471  tfrlem9  6480  tfr0dm  6483  tfrlemisucaccv  6486  tfrlemiubacc  6491  tfrlemiex  6492  tfrlemi1  6493  tfr1onlem3ag  6498  tfr1onlemsucaccv  6502  tfr1onlemubacc  6507  tfr1onlemex  6508  tfr1onlemaccex  6509  tfrcllemsucaccv  6515  tfrcllembxssdm  6517  tfrcllemubacc  6520  tfrcllemex  6521  tfrcllemaccex  6522  tfrcllemres  6523  tfrcldm  6524  rdgivallem  6542  rdgival  6543  rdgss  6544  rdgisuc1  6545  rdgon  6547  rdg0  6548  frec0g  6558  frecabcl  6560  freccllem  6563  frecfcllem  6565  frecsuclem  6567  frecsuc  6568  frecrdg  6569  oav2  6626  omv2  6628  xpdom2  7010  xpmapenlem  7030  xpmapen  7031  ac6sfi  7080  1stinl  7264  2ndinl  7265  1stinr  7266  2ndinr  7267  updjudhcoinlf  7270  updjudhcoinrg  7271  caseinl  7281  caseinr  7282  omp1eomlem  7284  omp1eom  7285  difinfsn  7290  ctmlemr  7298  ctm  7299  ctssdclemn0  7300  ctssdccl  7301  nninfninc  7313  nnnninfeq  7318  nnnninfeq2  7319  enomnilem  7328  enmkvlem  7351  enwomnilem  7359  exmidfodomrlemeldju  7400  exmidfodomrlemreseldju  7401  exmidfodomrlemr  7403  exmidfodomrlemrALT  7404  exmidaclem  7413  cc2  7476  cc3  7477  ltdfpr  7716  genpelvl  7722  genpelvu  7723  recexpr  7848  cauappcvgprlem1  7869  caucvgprlemnkj  7876  caucvgprlemnbj  7877  caucvgprlemm  7878  caucvgprlemdisj  7884  caucvgprlemloc  7885  caucvgprlemcl  7886  caucvgprlemladdfu  7887  caucvgprlemladdrl  7888  caucvgprlem1  7889  caucvgprlem2  7890  caucvgpr  7892  caucvgprprlemell  7895  caucvgprprlemelu  7896  caucvgprprlemcbv  7897  caucvgprprlemval  7898  caucvgprprlemnkeqj  7900  caucvgprprlemmu  7905  caucvgprprlemopl  7907  caucvgprprlemlol  7908  caucvgprprlemopu  7909  caucvgprprlemloc  7913  caucvgprprlemclphr  7915  caucvgprprlemexbt  7916  caucvgprprlem1  7919  caucvgprprlem2  7920  caucvgsr  8012  axcaucvglemval  8107  axcaucvglemres  8109  fv0p1e1  9248  uzin  9779  cnref1o  9875  fzsuc2  10304  fseq1m1p1  10320  fzoss2  10399  elfzonlteqm1  10445  divfl0  10546  flqzadd  10548  fldiv4p1lem1div2  10555  ceilqval  10558  flqdiv  10573  modqval  10576  modqfrac  10589  modqmulnn  10594  modqid  10601  modqcyc  10611  modqdi  10644  frec2uzuzd  10654  frec2uzrdg  10661  frecuzrdgrcl  10662  frecuzrdgtcl  10664  frecuzrdgsuc  10666  frecuzrdgrclt  10667  frecuzrdgg  10668  frecuzrdgfunlem  10671  frecuzrdgsuctlem  10675  iseqovex  10710  iseqvalcbv  10711  seq3val  10712  seqvalcd  10713  seq3m1  10725  seq3shft2  10733  seqshft2g  10734  monoord  10737  monoord2  10738  iseqf1olemqval  10752  iseqf1olemab  10754  iseqf1olemqk  10759  iseqf1olemjpcl  10760  iseqf1olemqpcl  10761  iseqf1olemfvp  10762  seq3f1olemqsumkj  10763  seq3f1olemqsumk  10764  seq3f1olemqsum  10765  seq3f1olemp  10767  seq3f1oleml  10768  seqf1oglem1  10771  seqf1oglem2  10772  seqf1og  10773  seq3homo  10779  seqhomog  10782  exp3val  10793  expnegap0  10799  facnn2  10986  facwordi  10992  faclbnd6  10996  bcval  11001  bccmpl  11006  bcn0  11007  bcm1k  11012  bcp1n  11013  bcn2  11016  hashinfom  11030  hashennn  11032  hashsng  11050  omgadd  11055  hashprg  11062  fihashssdif  11072  hashdifpr  11074  hashfzo  11076  hashfzp1  11078  hashxp  11080  zfz1isolemiso  11093  zfz1iso  11095  lsw1  11153  ccatfvalfi  11159  ccatlen  11162  ccatval3  11166  ccatval21sw  11172  ccatlid  11173  ccatass  11175  lswccatn0lsw  11178  lswccat0lsw  11179  ccatalpha  11180  s1leng  11191  ccats1val2  11207  lswccats1  11210  swrdfv0  11225  swrdfv2  11234  swrdsbslen  11237  swrds1  11239  ccatswrd  11241  pfxmpt  11251  pfxfv  11255  pfxtrcfvl  11268  ccatpfx  11272  swrdswrd  11276  lenpfxcctswrd  11282  ccatopth  11287  cats1un  11292  swrdccatin2  11300  pfxccatin12lem2  11302  shftval2  11377  shftval3  11378  shftval4  11379  shftval5  11380  seq3shft  11389  imval  11401  imre  11402  reim  11403  crim  11409  reim0  11412  mulreap  11415  recj  11418  reneg  11419  readd  11420  resub  11421  remullem  11422  redivap  11425  imcj  11426  imneg  11427  imadd  11428  imsub  11429  imdivap  11432  cjsub  11443  cjexp  11444  cjreim2  11455  cjap  11457  cjdivap  11460  cnrecnv  11461  cvg1nlemcau  11535  cvg1nlemres  11536  absval  11552  rennim  11553  sqrtdiv  11593  sqrtmsq  11596  absneg  11601  abscj  11603  absval2  11608  absreim  11619  absmul  11620  absdivap  11621  absid  11622  absre  11628  absexp  11630  absexpzap  11631  absimle  11635  abssub  11652  abs3dif  11656  abs2dif  11657  abs2dif2  11658  recan  11660  cau3lem  11665  max0addsup  11770  minabs  11787  bdtrilem  11790  clim  11832  clim2  11834  clim0  11836  clim0c  11837  climi0  11840  climconst  11841  climshftlemg  11853  climcn1  11859  climcn2  11860  addcn2  11861  subcn2  11862  mulcn2  11863  reccn2ap  11864  cjcn2  11867  recn2  11868  imcn2  11869  iser3shft  11897  climcau  11898  climcvg1nlem  11900  climcvg1n  11901  serf0  11903  summodclem3  11931  summodclem2a  11932  summodc  11934  fsumf1o  11941  sumsnf  11960  fsumm1  11967  fsumcnv  11988  fsumabs  12016  fsumrelem  12022  iserabs  12026  hash2iun1dif1  12031  isumshft  12041  isumsplit  12042  expcnvap0  12053  expcnv  12055  cvgratnnlemseq  12077  cvgratnnlemrate  12081  cvgratz  12083  mertenslemub  12085  mertenslemi1  12086  mertenslem2  12087  mertensabs  12088  prodmodclem3  12126  fprodf1o  12139  prodsnf  12143  fprodm1  12149  fprodabs  12167  fprodcnv  12176  efcllemp  12209  efcj  12224  efaddlem  12225  efcan  12227  efsub  12232  efexp  12233  efzval  12234  efgt0  12235  eftlub  12241  efltim  12249  sinval  12253  cosval  12254  tanval3ap  12265  resinval  12266  recosval  12267  resin4p  12269  recos4p  12270  sinneg  12277  cosneg  12278  efmival  12284  efeul  12285  sinadd  12287  cosadd  12288  sinsub  12291  cossub  12292  addsin  12293  subsin  12294  addcos  12297  subcos  12298  sincossq  12299  sin2t  12300  cos2t  12301  sin01bnd  12308  cos01bnd  12309  sin02gt0  12315  cos12dec  12319  absefi  12320  absef  12321  absefib  12322  efieq1re  12323  demoivre  12324  demoivreALT  12325  flodddiv4  12487  bitsval  12494  bits0  12499  bitsp1  12502  bitsp1e  12503  bitsp1o  12504  bitsmod  12507  nninfctlemfo  12601  alginv  12609  algcvg  12610  eucalgval  12616  eucalginv  12618  eucalglt  12619  eucalgcvga  12620  eucalg  12621  lcmgcd  12640  lcm1  12643  sqpweven  12737  2sqpwodd  12738  sqne2sq  12739  qnumval  12747  qdenval  12748  qden1elz  12767  nn0sqrtelqelz  12768  phival  12775  dfphi2  12782  phiprmpw  12784  phiprm  12785  eulerthlemth  12794  hashgcdeq  12802  phisum  12803  pythagtriplem6  12833  pythagtriplem7  12834  pythagtriplem12  12838  pythagtriplem14  12840  fldivp1  12911  4sqlem11  12964  ennnfonelemg  13014  ennnfonelemp1  13017  ennnfonelemkh  13023  ennnfonelemhf1o  13024  ennnfonelemnn0  13033  ctinfomlemom  13038  ctiunctlemu1st  13045  ctiunctlemu2nd  13046  ctiunctlemudc  13048  ctiunctlemfo  13050  isstruct2im  13082  isstruct2r  13083  setsslid  13123  ressbasd  13140  resseqnbasd  13146  ressplusgd  13202  ptex  13337  prdsex  13342  prdsval  13346  prdsbas3  13360  pwsval  13364  pwsbas  13365  pwsplusgval  13368  pwsmulrval  13369  imasex  13378  imasival  13379  f1ocpbl  13384  f1ovscpbl  13385  imasaddvallemg  13388  qusval  13396  fvprif  13416  xpsff1o  13422  igsumvalx  13462  gsumprval  13472  pws0g  13524  imasmnd  13526  ismhm  13534  mhmpropd  13539  mhmlin  13540  mhmf1o  13543  resmhm  13560  mhmco  13563  gsumwmhm  13571  grpinvsub  13655  pwsinvg  13685  imasgrp2  13687  imasgrp  13688  mhmlem  13691  mhmid  13692  mhmmnd  13693  ghmgrp  13695  mulgfvalg  13698  mulgval  13699  mulgnegnn  13709  mulgneg  13717  mulgnegneg  13718  mulgm1  13719  mulginvcom  13724  mulgz  13727  mulgnndir  13728  mulgdir  13731  mulgass  13736  mhmmulg  13740  subgmulg  13765  isnsg  13779  eqgfval  13799  ghmlin  13825  ghmid  13826  ghminv  13827  ghmsub  13828  ghmmulg  13833  resghm  13837  ghmeql  13844  ablsub2inv  13888  ghmcmn  13904  invghm  13906  imasabl  13913  gsumfzreidx  13914  gsumfzmhm  13920  mgpplusgg  13927  mgpbasg  13929  mgpscag  13930  mgptsetg  13931  mgpdsg  13933  rngm2neg  13952  imasrng  13959  isring  14003  ringm2neg  14058  imasring  14067  opprmulfvalg  14073  opprsllem  14077  isunitd  14110  opprunitd  14114  invrfvald  14126  rdivmuldivd  14148  rhmmul  14168  isrhm2d  14169  rhm1  14171  rhmdvdsr  14179  rhmopp  14180  rhmunitinv  14182  islmod  14295  islmodd  14297  scaffvalg  14310  lmodpropd  14353  lsssetm  14360  islssmd  14363  lssats2  14418  lspsnneg  14424  lspsnsub  14425  lspun0  14429  lmodindp1  14432  sralemg  14442  srascag  14446  sravscag  14447  sraipg  14448  rlmscabas  14464  ixpsnbasval  14470  2idlval  14506  2idlvalg  14507  mulgrhm2  14614  zlmlemg  14632  zlmsca  14636  zlmvscag  14637  znval  14640  znle  14641  znbaslemnn  14643  znidomb  14662  psrval  14670  psrbasg  14678  psrplusgg  14682  mplvalcoe  14694  mplsubgfileminv  14704  mpl0fi  14706  mplnegfi  14709  istps  14746  tpspropd  14750  eltpsg  14754  txvalex  14968  txval  14969  txbasval  14981  upxp  14986  uptx  14988  txrest  14990  cnmpt11  14997  cnmpt21  15005  hmeontr  15027  txhmeo  15033  psmetxrge0  15046  xmetunirn  15072  mopnval  15156  mopntopon  15157  isxms  15165  isxms2  15166  isms  15167  msrtri  15190  xmspropd  15191  mspropd  15192  setsmsbasg  15193  setsmsdsg  15194  setsmstsetg  15195  comet  15213  metcnpi  15229  metcnpi2  15230  cnbl0  15248  cnblcld  15249  resubmet  15270  mpomulcn  15280  elcncf  15287  cncfi  15292  rescncf  15295  mulc1cncf  15303  cncfco  15305  cncfmptid  15311  addccncf  15314  cdivcncfap  15318  negcncf  15319  mulcncflem  15321  ivthinclemlopn  15350  ivthinclemuopn  15352  limccl  15373  ellimc3apf  15374  limcimolemlt  15378  cnplimclemle  15382  limccnpcntop  15389  reldvg  15393  dvfvalap  15395  dveflem  15440  dvef  15441  plymullem1  15462  plycjlemc  15474  plycj  15475  plyrecj  15477  plyreres  15478  sin0pilem1  15495  ef2kpi  15520  sinperlem  15522  sin2kpi  15525  cos2kpi  15526  sin2pim  15527  cos2pim  15528  ptolemy  15538  sincosq2sgn  15541  sincosq3sgn  15542  sincosq4sgn  15543  sinq12gt0  15544  tangtx  15552  sincosq1eq  15553  abssinper  15560  sinkpi  15561  coskpi  15562  cosq34lt1  15564  relogeftb  15579  relogoprlem  15582  relogexp  15586  rpcxpef  15608  logcxp  15611  1cxp  15614  ecxp  15615  rpcxpadd  15619  rpmulcxp  15623  cxpmul  15626  abscxp  15629  logsqrt  15637  rpabscxpbnd  15654  rpcxplogb  15678  lgsval  15723  lgsval2lem  15729  lgsval4a  15741  lgsdi  15756  lgseisenlem3  15791  lgseisenlem4  15792  lgsquadlem1  15796  lgsquadlem2  15797  lgsquadlem3  15798  2lgslem1  15810  2lgslem3a  15812  2lgslem3b  15813  2lgslem3c  15814  2lgslem3d  15815  vtxdgfval  16094  vtxdgfifival  16097  vtxdgop  16098  vtxdgfi0e  16101  vtxdeqd  16102  vtxdfifiun  16103  vtxdumgrfival  16104  iswlk  16120  2wlklem  16171  wlkres  16174  clwwlkccatlem  16195  clwwlkn2  16216  clwwlkext2edg  16217  umgr2cwwk2dif  16219  clwwlknonex2lem2  16233  nnsf  16543  peano4nninf  16544  peano3nninf  16545  nninfalllem1  16546  nninfall  16547  nninfsellemdc  16548  nninfsellemeq  16552  nninfsellemqall  16553  nninfsellemeqinf  16554  nninfsel  16555  nnnninfex  16560  exmidsbthr  16563  qdencn  16567  refeq  16568  isomninnlem  16570  apdifflemr  16587  apdiff  16588  ismkvnnlem  16592  nconstwlpolem  16605