Theorem fveq2d 5633

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

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

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 2801  df-un 3201  df-sn 3672  df-pr 3673  df-op 3675  df-uni 3889  df-br 4084  df-iota 5278  df-fv 5326

This theorem is referenced by:  2fveq3  5634  fveq12d  5636  fveqeq2d  5637  csbfvg  5671  fvmptdf  5724  fvmptt  5728  resfvresima  5880  fcof1  5913  oveq1  6014  oveq2  6015  fvoveq1d  6029  caofinvl  6250  op1stg  6302  op2ndg  6303  ot1stg  6304  ot2ndg  6305  eloprabi  6348  1stconst  6373  algrflemg  6382  tfrlem1  6460  tfrlem3ag  6461  tfrlem3a  6462  tfrlem9  6471  tfr0dm  6474  tfrlemisucaccv  6477  tfrlemiubacc  6482  tfrlemiex  6483  tfrlemi1  6484  tfr1onlem3ag  6489  tfr1onlemsucaccv  6493  tfr1onlemubacc  6498  tfr1onlemex  6499  tfr1onlemaccex  6500  tfrcllemsucaccv  6506  tfrcllembxssdm  6508  tfrcllemubacc  6511  tfrcllemex  6512  tfrcllemaccex  6513  tfrcllemres  6514  tfrcldm  6515  rdgivallem  6533  rdgival  6534  rdgss  6535  rdgisuc1  6536  rdgon  6538  rdg0  6539  frec0g  6549  frecabcl  6551  freccllem  6554  frecfcllem  6556  frecsuclem  6558  frecsuc  6559  frecrdg  6560  oav2  6617  omv2  6619  xpdom2  6998  xpmapenlem  7018  xpmapen  7019  ac6sfi  7068  1stinl  7252  2ndinl  7253  1stinr  7254  2ndinr  7255  updjudhcoinlf  7258  updjudhcoinrg  7259  caseinl  7269  caseinr  7270  omp1eomlem  7272  omp1eom  7273  difinfsn  7278  ctmlemr  7286  ctm  7287  ctssdclemn0  7288  ctssdccl  7289  nninfninc  7301  nnnninfeq  7306  nnnninfeq2  7307  enomnilem  7316  enmkvlem  7339  enwomnilem  7347  exmidfodomrlemeldju  7388  exmidfodomrlemreseldju  7389  exmidfodomrlemr  7391  exmidfodomrlemrALT  7392  exmidaclem  7401  cc2  7464  cc3  7465  ltdfpr  7704  genpelvl  7710  genpelvu  7711  recexpr  7836  cauappcvgprlem1  7857  caucvgprlemnkj  7864  caucvgprlemnbj  7865  caucvgprlemm  7866  caucvgprlemdisj  7872  caucvgprlemloc  7873  caucvgprlemcl  7874  caucvgprlemladdfu  7875  caucvgprlemladdrl  7876  caucvgprlem1  7877  caucvgprlem2  7878  caucvgpr  7880  caucvgprprlemell  7883  caucvgprprlemelu  7884  caucvgprprlemcbv  7885  caucvgprprlemval  7886  caucvgprprlemnkeqj  7888  caucvgprprlemmu  7893  caucvgprprlemopl  7895  caucvgprprlemlol  7896  caucvgprprlemopu  7897  caucvgprprlemloc  7901  caucvgprprlemclphr  7903  caucvgprprlemexbt  7904  caucvgprprlem1  7907  caucvgprprlem2  7908  caucvgsr  8000  axcaucvglemval  8095  axcaucvglemres  8097  fv0p1e1  9236  uzin  9767  cnref1o  9858  fzsuc2  10287  fseq1m1p1  10303  fzoss2  10382  elfzonlteqm1  10428  divfl0  10528  flqzadd  10530  fldiv4p1lem1div2  10537  ceilqval  10540  flqdiv  10555  modqval  10558  modqfrac  10571  modqmulnn  10576  modqid  10583  modqcyc  10593  modqdi  10626  frec2uzuzd  10636  frec2uzrdg  10643  frecuzrdgrcl  10644  frecuzrdgtcl  10646  frecuzrdgsuc  10648  frecuzrdgrclt  10649  frecuzrdgg  10650  frecuzrdgfunlem  10653  frecuzrdgsuctlem  10657  iseqovex  10692  iseqvalcbv  10693  seq3val  10694  seqvalcd  10695  seq3m1  10707  seq3shft2  10715  seqshft2g  10716  monoord  10719  monoord2  10720  iseqf1olemqval  10734  iseqf1olemab  10736  iseqf1olemqk  10741  iseqf1olemjpcl  10742  iseqf1olemqpcl  10743  iseqf1olemfvp  10744  seq3f1olemqsumkj  10745  seq3f1olemqsumk  10746  seq3f1olemqsum  10747  seq3f1olemp  10749  seq3f1oleml  10750  seqf1oglem1  10753  seqf1oglem2  10754  seqf1og  10755  seq3homo  10761  seqhomog  10764  exp3val  10775  expnegap0  10781  facnn2  10968  facwordi  10974  faclbnd6  10978  bcval  10983  bccmpl  10988  bcn0  10989  bcm1k  10994  bcp1n  10995  bcn2  10998  hashinfom  11012  hashennn  11014  hashsng  11032  omgadd  11036  hashprg  11043  fihashssdif  11053  hashdifpr  11055  hashfzo  11057  hashfzp1  11059  hashxp  11061  zfz1isolemiso  11074  zfz1iso  11076  lsw1  11134  ccatfvalfi  11140  ccatlen  11143  ccatval3  11147  ccatval21sw  11153  ccatlid  11154  ccatass  11156  lswccatn0lsw  11159  lswccat0lsw  11160  ccatalpha  11161  s1leng  11172  ccats1val2  11186  lswccats1  11189  swrdfv0  11201  swrdfv2  11210  swrdsbslen  11213  swrds1  11215  ccatswrd  11217  pfxmpt  11227  pfxfv  11231  pfxtrcfvl  11244  ccatpfx  11248  swrdswrd  11252  lenpfxcctswrd  11258  ccatopth  11263  cats1un  11268  swrdccatin2  11276  pfxccatin12lem2  11278  shftval2  11352  shftval3  11353  shftval4  11354  shftval5  11355  seq3shft  11364  imval  11376  imre  11377  reim  11378  crim  11384  reim0  11387  mulreap  11390  recj  11393  reneg  11394  readd  11395  resub  11396  remullem  11397  redivap  11400  imcj  11401  imneg  11402  imadd  11403  imsub  11404  imdivap  11407  cjsub  11418  cjexp  11419  cjreim2  11430  cjap  11432  cjdivap  11435  cnrecnv  11436  cvg1nlemcau  11510  cvg1nlemres  11511  absval  11527  rennim  11528  sqrtdiv  11568  sqrtmsq  11571  absneg  11576  abscj  11578  absval2  11583  absreim  11594  absmul  11595  absdivap  11596  absid  11597  absre  11603  absexp  11605  absexpzap  11606  absimle  11610  abssub  11627  abs3dif  11631  abs2dif  11632  abs2dif2  11633  recan  11635  cau3lem  11640  max0addsup  11745  minabs  11762  bdtrilem  11765  clim  11807  clim2  11809  clim0  11811  clim0c  11812  climi0  11815  climconst  11816  climshftlemg  11828  climcn1  11834  climcn2  11835  addcn2  11836  subcn2  11837  mulcn2  11838  reccn2ap  11839  cjcn2  11842  recn2  11843  imcn2  11844  iser3shft  11872  climcau  11873  climcvg1nlem  11875  climcvg1n  11876  serf0  11878  summodclem3  11906  summodclem2a  11907  summodc  11909  fsumf1o  11916  sumsnf  11935  fsumm1  11942  fsumcnv  11963  fsumabs  11991  fsumrelem  11997  iserabs  12001  hash2iun1dif1  12006  isumshft  12016  isumsplit  12017  expcnvap0  12028  expcnv  12030  cvgratnnlemseq  12052  cvgratnnlemrate  12056  cvgratz  12058  mertenslemub  12060  mertenslemi1  12061  mertenslem2  12062  mertensabs  12063  prodmodclem3  12101  fprodf1o  12114  prodsnf  12118  fprodm1  12124  fprodabs  12142  fprodcnv  12151  efcllemp  12184  efcj  12199  efaddlem  12200  efcan  12202  efsub  12207  efexp  12208  efzval  12209  efgt0  12210  eftlub  12216  efltim  12224  sinval  12228  cosval  12229  tanval3ap  12240  resinval  12241  recosval  12242  resin4p  12244  recos4p  12245  sinneg  12252  cosneg  12253  efmival  12259  efeul  12260  sinadd  12262  cosadd  12263  sinsub  12266  cossub  12267  addsin  12268  subsin  12269  addcos  12272  subcos  12273  sincossq  12274  sin2t  12275  cos2t  12276  sin01bnd  12283  cos01bnd  12284  sin02gt0  12290  cos12dec  12294  absefi  12295  absef  12296  absefib  12297  efieq1re  12298  demoivre  12299  demoivreALT  12300  flodddiv4  12462  bitsval  12469  bits0  12474  bitsp1  12477  bitsp1e  12478  bitsp1o  12479  bitsmod  12482  nninfctlemfo  12576  alginv  12584  algcvg  12585  eucalgval  12591  eucalginv  12593  eucalglt  12594  eucalgcvga  12595  eucalg  12596  lcmgcd  12615  lcm1  12618  sqpweven  12712  2sqpwodd  12713  sqne2sq  12714  qnumval  12722  qdenval  12723  qden1elz  12742  nn0sqrtelqelz  12743  phival  12750  dfphi2  12757  phiprmpw  12759  phiprm  12760  eulerthlemth  12769  hashgcdeq  12777  phisum  12778  pythagtriplem6  12808  pythagtriplem7  12809  pythagtriplem12  12813  pythagtriplem14  12815  fldivp1  12886  4sqlem11  12939  ennnfonelemg  12989  ennnfonelemp1  12992  ennnfonelemkh  12998  ennnfonelemhf1o  12999  ennnfonelemnn0  13008  ctinfomlemom  13013  ctiunctlemu1st  13020  ctiunctlemu2nd  13021  ctiunctlemudc  13023  ctiunctlemfo  13025  isstruct2im  13057  isstruct2r  13058  setsslid  13098  ressbasd  13115  resseqnbasd  13121  ressplusgd  13177  ptex  13312  prdsex  13317  prdsval  13321  prdsbas3  13335  pwsval  13339  pwsbas  13340  pwsplusgval  13343  pwsmulrval  13344  imasex  13353  imasival  13354  f1ocpbl  13359  f1ovscpbl  13360  imasaddvallemg  13363  qusval  13371  fvprif  13391  xpsff1o  13397  igsumvalx  13437  gsumprval  13447  pws0g  13499  imasmnd  13501  ismhm  13509  mhmpropd  13514  mhmlin  13515  mhmf1o  13518  resmhm  13535  mhmco  13538  gsumwmhm  13546  grpinvsub  13630  pwsinvg  13660  imasgrp2  13662  imasgrp  13663  mhmlem  13666  mhmid  13667  mhmmnd  13668  ghmgrp  13670  mulgfvalg  13673  mulgval  13674  mulgnegnn  13684  mulgneg  13692  mulgnegneg  13693  mulgm1  13694  mulginvcom  13699  mulgz  13702  mulgnndir  13703  mulgdir  13706  mulgass  13711  mhmmulg  13715  subgmulg  13740  isnsg  13754  eqgfval  13774  ghmlin  13800  ghmid  13801  ghminv  13802  ghmsub  13803  ghmmulg  13808  resghm  13812  ghmeql  13819  ablsub2inv  13863  ghmcmn  13879  invghm  13881  imasabl  13888  gsumfzreidx  13889  gsumfzmhm  13895  mgpplusgg  13902  mgpbasg  13904  mgpscag  13905  mgptsetg  13906  mgpdsg  13908  rngm2neg  13927  imasrng  13934  isring  13978  ringm2neg  14033  imasring  14042  opprmulfvalg  14048  opprsllem  14052  isunitd  14085  opprunitd  14089  invrfvald  14101  rdivmuldivd  14123  rhmmul  14143  isrhm2d  14144  rhm1  14146  rhmdvdsr  14154  rhmopp  14155  rhmunitinv  14157  islmod  14270  islmodd  14272  scaffvalg  14285  lmodpropd  14328  lsssetm  14335  islssmd  14338  lssats2  14393  lspsnneg  14399  lspsnsub  14400  lspun0  14404  lmodindp1  14407  sralemg  14417  srascag  14421  sravscag  14422  sraipg  14423  rlmscabas  14439  ixpsnbasval  14445  2idlval  14481  2idlvalg  14482  mulgrhm2  14589  zlmlemg  14607  zlmsca  14611  zlmvscag  14612  znval  14615  znle  14616  znbaslemnn  14618  znidomb  14637  psrval  14645  psrbasg  14653  psrplusgg  14657  mplvalcoe  14669  mplsubgfileminv  14679  mpl0fi  14681  mplnegfi  14684  istps  14721  tpspropd  14725  eltpsg  14729  txvalex  14943  txval  14944  txbasval  14956  upxp  14961  uptx  14963  txrest  14965  cnmpt11  14972  cnmpt21  14980  hmeontr  15002  txhmeo  15008  psmetxrge0  15021  xmetunirn  15047  mopnval  15131  mopntopon  15132  isxms  15140  isxms2  15141  isms  15142  msrtri  15165  xmspropd  15166  mspropd  15167  setsmsbasg  15168  setsmsdsg  15169  setsmstsetg  15170  comet  15188  metcnpi  15204  metcnpi2  15205  cnbl0  15223  cnblcld  15224  resubmet  15245  mpomulcn  15255  elcncf  15262  cncfi  15267  rescncf  15270  mulc1cncf  15278  cncfco  15280  cncfmptid  15286  addccncf  15289  cdivcncfap  15293  negcncf  15294  mulcncflem  15296  ivthinclemlopn  15325  ivthinclemuopn  15327  limccl  15348  ellimc3apf  15349  limcimolemlt  15353  cnplimclemle  15357  limccnpcntop  15364  reldvg  15368  dvfvalap  15370  dveflem  15415  dvef  15416  plymullem1  15437  plycjlemc  15449  plycj  15450  plyrecj  15452  plyreres  15453  sin0pilem1  15470  ef2kpi  15495  sinperlem  15497  sin2kpi  15500  cos2kpi  15501  sin2pim  15502  cos2pim  15503  ptolemy  15513  sincosq2sgn  15516  sincosq3sgn  15517  sincosq4sgn  15518  sinq12gt0  15519  tangtx  15527  sincosq1eq  15528  abssinper  15535  sinkpi  15536  coskpi  15537  cosq34lt1  15539  relogeftb  15554  relogoprlem  15557  relogexp  15561  rpcxpef  15583  logcxp  15586  1cxp  15589  ecxp  15590  rpcxpadd  15594  rpmulcxp  15598  cxpmul  15601  abscxp  15604  logsqrt  15612  rpabscxpbnd  15629  rpcxplogb  15653  lgsval  15698  lgsval2lem  15704  lgsval4a  15716  lgsdi  15731  lgseisenlem3  15766  lgseisenlem4  15767  lgsquadlem1  15771  lgsquadlem2  15772  lgsquadlem3  15773  2lgslem1  15785  2lgslem3a  15787  2lgslem3b  15788  2lgslem3c  15789  2lgslem3d  15790  vtxdgfval  16047  vtxdgfifival  16050  vtxdgop  16051  vtxdgfi0e  16054  vtxdeqd  16055  vtxdfifiun  16056  vtxdumgrfival  16057  iswlk  16064  2wlklem  16115  wlkres  16118  clwwlkccatlem  16137  nnsf  16431  peano4nninf  16432  peano3nninf  16433  nninfalllem1  16434  nninfall  16435  nninfsellemdc  16436  nninfsellemeq  16440  nninfsellemqall  16441  nninfsellemeqinf  16442  nninfsel  16443  nnnninfex  16448  exmidsbthr  16451  qdencn  16455  refeq  16456  isomninnlem  16458  apdifflemr  16475  apdiff  16476  ismkvnnlem  16480  nconstwlpolem  16493