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  5891  fcof1  5924  oveq1  6025  oveq2  6026  fvoveq1d  6040  caofinvl  6261  op1stg  6313  op2ndg  6314  ot1stg  6315  ot2ndg  6316  eloprabi  6361  1stconst  6386  algrflemg  6395  tfrlem1  6474  tfrlem3ag  6475  tfrlem3a  6476  tfrlem9  6485  tfr0dm  6488  tfrlemisucaccv  6491  tfrlemiubacc  6496  tfrlemiex  6497  tfrlemi1  6498  tfr1onlem3ag  6503  tfr1onlemsucaccv  6507  tfr1onlemubacc  6512  tfr1onlemex  6513  tfr1onlemaccex  6514  tfrcllemsucaccv  6520  tfrcllembxssdm  6522  tfrcllemubacc  6525  tfrcllemex  6526  tfrcllemaccex  6527  tfrcllemres  6528  tfrcldm  6529  rdgivallem  6547  rdgival  6548  rdgss  6549  rdgisuc1  6550  rdgon  6552  rdg0  6553  frec0g  6563  frecabcl  6565  freccllem  6568  frecfcllem  6570  frecsuclem  6572  frecsuc  6573  frecrdg  6574  oav2  6631  omv2  6633  xpdom2  7015  xpmapenlem  7035  xpmapen  7036  ac6sfi  7087  1stinl  7273  2ndinl  7274  1stinr  7275  2ndinr  7276  updjudhcoinlf  7279  updjudhcoinrg  7280  caseinl  7290  caseinr  7291  omp1eomlem  7293  omp1eom  7294  difinfsn  7299  ctmlemr  7307  ctm  7308  ctssdclemn0  7309  ctssdccl  7310  nninfninc  7322  nnnninfeq  7327  nnnninfeq2  7328  enomnilem  7337  enmkvlem  7360  enwomnilem  7368  exmidfodomrlemeldju  7410  exmidfodomrlemreseldju  7411  exmidfodomrlemr  7413  exmidfodomrlemrALT  7414  exmidaclem  7423  cc2  7486  cc3  7487  ltdfpr  7726  genpelvl  7732  genpelvu  7733  recexpr  7858  cauappcvgprlem1  7879  caucvgprlemnkj  7886  caucvgprlemnbj  7887  caucvgprlemm  7888  caucvgprlemdisj  7894  caucvgprlemloc  7895  caucvgprlemcl  7896  caucvgprlemladdfu  7897  caucvgprlemladdrl  7898  caucvgprlem1  7899  caucvgprlem2  7900  caucvgpr  7902  caucvgprprlemell  7905  caucvgprprlemelu  7906  caucvgprprlemcbv  7907  caucvgprprlemval  7908  caucvgprprlemnkeqj  7910  caucvgprprlemmu  7915  caucvgprprlemopl  7917  caucvgprprlemlol  7918  caucvgprprlemopu  7919  caucvgprprlemloc  7923  caucvgprprlemclphr  7925  caucvgprprlemexbt  7926  caucvgprprlem1  7929  caucvgprprlem2  7930  caucvgsr  8022  axcaucvglemval  8117  axcaucvglemres  8119  fv0p1e1  9258  uzin  9789  cnref1o  9885  fzsuc2  10314  fseq1m1p1  10330  fzoss2  10409  elfzonlteqm1  10456  divfl0  10557  flqzadd  10559  fldiv4p1lem1div2  10566  ceilqval  10569  flqdiv  10584  modqval  10587  modqfrac  10600  modqmulnn  10605  modqid  10612  modqcyc  10622  modqdi  10655  frec2uzuzd  10665  frec2uzrdg  10672  frecuzrdgrcl  10673  frecuzrdgtcl  10675  frecuzrdgsuc  10677  frecuzrdgrclt  10678  frecuzrdgg  10679  frecuzrdgfunlem  10682  frecuzrdgsuctlem  10686  iseqovex  10721  iseqvalcbv  10722  seq3val  10723  seqvalcd  10724  seq3m1  10736  seq3shft2  10744  seqshft2g  10745  monoord  10748  monoord2  10749  iseqf1olemqval  10763  iseqf1olemab  10765  iseqf1olemqk  10770  iseqf1olemjpcl  10771  iseqf1olemqpcl  10772  iseqf1olemfvp  10773  seq3f1olemqsumkj  10774  seq3f1olemqsumk  10775  seq3f1olemqsum  10776  seq3f1olemp  10778  seq3f1oleml  10779  seqf1oglem1  10782  seqf1oglem2  10783  seqf1og  10784  seq3homo  10790  seqhomog  10793  exp3val  10804  expnegap0  10810  facnn2  10997  facwordi  11003  faclbnd6  11007  bcval  11012  bccmpl  11017  bcn0  11018  bcm1k  11023  bcp1n  11024  bcn2  11027  hashinfom  11041  hashennn  11043  hashsng  11061  omgadd  11066  hashprg  11073  fihashssdif  11083  hashdifpr  11085  hashfzo  11087  hashfzp1  11089  hashxp  11091  zfz1isolemiso  11104  zfz1iso  11106  hashtpglem  11111  lsw1  11167  ccatfvalfi  11173  ccatlen  11176  ccatval3  11180  ccatval21sw  11186  ccatlid  11187  ccatass  11189  lswccatn0lsw  11192  lswccat0lsw  11193  ccatalpha  11194  s1leng  11205  ccats1val2  11221  lswccats1  11224  swrdfv0  11239  swrdfv2  11248  swrdsbslen  11251  swrds1  11253  ccatswrd  11255  pfxmpt  11265  pfxfv  11269  pfxtrcfvl  11282  ccatpfx  11286  swrdswrd  11290  lenpfxcctswrd  11296  ccatopth  11301  cats1un  11306  swrdccatin2  11314  pfxccatin12lem2  11316  shftval2  11391  shftval3  11392  shftval4  11393  shftval5  11394  seq3shft  11403  imval  11415  imre  11416  reim  11417  crim  11423  reim0  11426  mulreap  11429  recj  11432  reneg  11433  readd  11434  resub  11435  remullem  11436  redivap  11439  imcj  11440  imneg  11441  imadd  11442  imsub  11443  imdivap  11446  cjsub  11457  cjexp  11458  cjreim2  11469  cjap  11471  cjdivap  11474  cnrecnv  11475  cvg1nlemcau  11549  cvg1nlemres  11550  absval  11566  rennim  11567  sqrtdiv  11607  sqrtmsq  11610  absneg  11615  abscj  11617  absval2  11622  absreim  11633  absmul  11634  absdivap  11635  absid  11636  absre  11642  absexp  11644  absexpzap  11645  absimle  11649  abssub  11666  abs3dif  11670  abs2dif  11671  abs2dif2  11672  recan  11674  cau3lem  11679  max0addsup  11784  minabs  11801  bdtrilem  11804  clim  11846  clim2  11848  clim0  11850  clim0c  11851  climi0  11854  climconst  11855  climshftlemg  11867  climcn1  11873  climcn2  11874  addcn2  11875  subcn2  11876  mulcn2  11877  reccn2ap  11878  cjcn2  11881  recn2  11882  imcn2  11883  iser3shft  11911  climcau  11912  climcvg1nlem  11914  climcvg1n  11915  serf0  11917  fzf1o  11941  summodclem3  11946  summodclem2a  11947  summodc  11949  fsumf1o  11956  sumsnf  11975  fsumm1  11982  fsumcnv  12003  fsumabs  12031  fsumrelem  12037  iserabs  12041  hash2iun1dif1  12046  isumshft  12056  isumsplit  12057  expcnvap0  12068  expcnv  12070  cvgratnnlemseq  12092  cvgratnnlemrate  12096  cvgratz  12098  mertenslemub  12100  mertenslemi1  12101  mertenslem2  12102  mertensabs  12103  prodmodclem3  12141  fprodf1o  12154  prodsnf  12158  fprodm1  12164  fprodabs  12182  fprodcnv  12191  efcllemp  12224  efcj  12239  efaddlem  12240  efcan  12242  efsub  12247  efexp  12248  efzval  12249  efgt0  12250  eftlub  12256  efltim  12264  sinval  12268  cosval  12269  tanval3ap  12280  resinval  12281  recosval  12282  resin4p  12284  recos4p  12285  sinneg  12292  cosneg  12293  efmival  12299  efeul  12300  sinadd  12302  cosadd  12303  sinsub  12306  cossub  12307  addsin  12308  subsin  12309  addcos  12312  subcos  12313  sincossq  12314  sin2t  12315  cos2t  12316  sin01bnd  12323  cos01bnd  12324  sin02gt0  12330  cos12dec  12334  absefi  12335  absef  12336  absefib  12337  efieq1re  12338  demoivre  12339  demoivreALT  12340  flodddiv4  12502  bitsval  12509  bits0  12514  bitsp1  12517  bitsp1e  12518  bitsp1o  12519  bitsmod  12522  nninfctlemfo  12616  alginv  12624  algcvg  12625  eucalgval  12631  eucalginv  12633  eucalglt  12634  eucalgcvga  12635  eucalg  12636  lcmgcd  12655  lcm1  12658  sqpweven  12752  2sqpwodd  12753  sqne2sq  12754  qnumval  12762  qdenval  12763  qden1elz  12782  nn0sqrtelqelz  12783  phival  12790  dfphi2  12797  phiprmpw  12799  phiprm  12800  eulerthlemth  12809  hashgcdeq  12817  phisum  12818  pythagtriplem6  12848  pythagtriplem7  12849  pythagtriplem12  12853  pythagtriplem14  12855  fldivp1  12926  4sqlem11  12979  ennnfonelemg  13029  ennnfonelemp1  13032  ennnfonelemkh  13038  ennnfonelemhf1o  13039  ennnfonelemnn0  13048  ctinfomlemom  13053  ctiunctlemu1st  13060  ctiunctlemu2nd  13061  ctiunctlemudc  13063  ctiunctlemfo  13065  isstruct2im  13097  isstruct2r  13098  setsslid  13138  ressbasd  13155  resseqnbasd  13161  ressplusgd  13217  ptex  13352  prdsex  13357  prdsval  13361  prdsbas3  13375  pwsval  13379  pwsbas  13380  pwsplusgval  13383  pwsmulrval  13384  imasex  13393  imasival  13394  f1ocpbl  13399  f1ovscpbl  13400  imasaddvallemg  13403  qusval  13411  fvprif  13431  xpsff1o  13437  igsumvalx  13477  gsumprval  13487  pws0g  13539  imasmnd  13541  ismhm  13549  mhmpropd  13554  mhmlin  13555  mhmf1o  13558  resmhm  13575  mhmco  13578  gsumwmhm  13586  grpinvsub  13670  pwsinvg  13700  imasgrp2  13702  imasgrp  13703  mhmlem  13706  mhmid  13707  mhmmnd  13708  ghmgrp  13710  mulgfvalg  13713  mulgval  13714  mulgnegnn  13724  mulgneg  13732  mulgnegneg  13733  mulgm1  13734  mulginvcom  13739  mulgz  13742  mulgnndir  13743  mulgdir  13746  mulgass  13751  mhmmulg  13755  subgmulg  13780  isnsg  13794  eqgfval  13814  ghmlin  13840  ghmid  13841  ghminv  13842  ghmsub  13843  ghmmulg  13848  resghm  13852  ghmeql  13859  ablsub2inv  13903  ghmcmn  13919  invghm  13921  imasabl  13928  gsumfzreidx  13929  gsumfzmhm  13935  gsumsplit0  13938  mgpplusgg  13943  mgpbasg  13945  mgpscag  13946  mgptsetg  13947  mgpdsg  13949  rngm2neg  13968  imasrng  13975  isring  14019  ringm2neg  14074  imasring  14083  opprmulfvalg  14089  opprsllem  14093  isunitd  14126  opprunitd  14130  invrfvald  14142  rdivmuldivd  14164  rhmmul  14184  isrhm2d  14185  rhm1  14187  rhmdvdsr  14195  rhmopp  14196  rhmunitinv  14198  islmod  14311  islmodd  14313  scaffvalg  14326  lmodpropd  14369  lsssetm  14376  islssmd  14379  lssats2  14434  lspsnneg  14440  lspsnsub  14441  lspun0  14445  lmodindp1  14448  sralemg  14458  srascag  14462  sravscag  14463  sraipg  14464  rlmscabas  14480  ixpsnbasval  14486  2idlval  14522  2idlvalg  14523  mulgrhm2  14630  zlmlemg  14648  zlmsca  14652  zlmvscag  14653  znval  14656  znle  14657  znbaslemnn  14659  znidomb  14678  psrval  14686  psrbasg  14694  psrplusgg  14698  mplvalcoe  14710  mplsubgfileminv  14720  mpl0fi  14722  mplnegfi  14725  istps  14762  tpspropd  14766  eltpsg  14770  txvalex  14984  txval  14985  txbasval  14997  upxp  15002  uptx  15004  txrest  15006  cnmpt11  15013  cnmpt21  15021  hmeontr  15043  txhmeo  15049  psmetxrge0  15062  xmetunirn  15088  mopnval  15172  mopntopon  15173  isxms  15181  isxms2  15182  isms  15183  msrtri  15206  xmspropd  15207  mspropd  15208  setsmsbasg  15209  setsmsdsg  15210  setsmstsetg  15211  comet  15229  metcnpi  15245  metcnpi2  15246  cnbl0  15264  cnblcld  15265  resubmet  15286  mpomulcn  15296  elcncf  15303  cncfi  15308  rescncf  15311  mulc1cncf  15319  cncfco  15321  cncfmptid  15327  addccncf  15330  cdivcncfap  15334  negcncf  15335  mulcncflem  15337  ivthinclemlopn  15366  ivthinclemuopn  15368  limccl  15389  ellimc3apf  15390  limcimolemlt  15394  cnplimclemle  15398  limccnpcntop  15405  reldvg  15409  dvfvalap  15411  dveflem  15456  dvef  15457  plymullem1  15478  plycjlemc  15490  plycj  15491  plyrecj  15493  plyreres  15494  sin0pilem1  15511  ef2kpi  15536  sinperlem  15538  sin2kpi  15541  cos2kpi  15542  sin2pim  15543  cos2pim  15544  ptolemy  15554  sincosq2sgn  15557  sincosq3sgn  15558  sincosq4sgn  15559  sinq12gt0  15560  tangtx  15568  sincosq1eq  15569  abssinper  15576  sinkpi  15577  coskpi  15578  cosq34lt1  15580  relogeftb  15595  relogoprlem  15598  relogexp  15602  rpcxpef  15624  logcxp  15627  1cxp  15630  ecxp  15631  rpcxpadd  15635  rpmulcxp  15639  cxpmul  15642  abscxp  15645  logsqrt  15653  rpabscxpbnd  15670  rpcxplogb  15694  lgsval  15739  lgsval2lem  15745  lgsval4a  15757  lgsdi  15772  lgseisenlem3  15807  lgseisenlem4  15808  lgsquadlem1  15812  lgsquadlem2  15813  lgsquadlem3  15814  2lgslem1  15826  2lgslem3a  15828  2lgslem3b  15829  2lgslem3c  15830  2lgslem3d  15831  vtxdgfval  16145  vtxdgfifival  16148  vtxdgop  16149  vtxdgfi0e  16152  vtxdeqd  16153  vtxdfifiun  16154  vtxdumgrfival  16155  1hevtxdg1en  16165  iswlk  16180  2wlklem  16233  wlkres  16236  clwwlkccatlem  16257  clwwlkn2  16278  clwwlkext2edg  16279  umgr2cwwk2dif  16281  clwwlknonex2lem2  16295  eupth2fi  16336  eulerpathprum  16337  depindlem1  16351  depind  16354  nnsf  16633  peano4nninf  16634  peano3nninf  16635  nninfalllem1  16636  nninfall  16637  nninfsellemdc  16638  nninfsellemeq  16642  nninfsellemqall  16643  nninfsellemeqinf  16644  nninfsel  16645  nnnninfex  16650  exmidsbthr  16653  qdencn  16657  refeq  16658  isomninnlem  16660  apdifflemr  16677  apdiff  16678  qdiff  16679  ismkvnnlem  16683  nconstwlpolem  16696  gfsumval  16707  gsumgfsumlem  16710  gfsump1  16713