Theorem fveq2d 5679

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

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

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 2216

This theorem depends on definitions:  df-bi 117  df-3an 1007  df-tru 1401  df-nf 1510  df-sb 1812  df-clab 2221  df-cleq 2227  df-clel 2230  df-nfc 2375  df-rex 2528  df-v 2817  df-un 3218  df-sn 3700  df-pr 3701  df-op 3703  df-uni 3920  df-br 4115  df-iota 5317  df-fv 5365

This theorem is referenced by:  2fveq3  5680  fveq12d  5682  fveqeq2d  5683  csbfvg  5717  fvmptdf  5770  fvmptt  5774  resfvresima  5929  fcof1  5962  oveq1  6065  oveq2  6066  fvoveq1d  6080  caofinvl  6301  op1stg  6357  op2ndg  6358  ot1stg  6359  ot2ndg  6360  eloprabi  6405  1stconst  6430  algrflemg  6439  tfrlem1  6552  tfrlem3ag  6553  tfrlem3a  6554  tfrlem9  6563  tfr0dm  6566  tfrlemisucaccv  6569  tfrlemiubacc  6574  tfrlemiex  6575  tfrlemi1  6576  tfr1onlem3ag  6581  tfr1onlemsucaccv  6585  tfr1onlemubacc  6590  tfr1onlemex  6591  tfr1onlemaccex  6592  tfrcllemsucaccv  6598  tfrcllembxssdm  6600  tfrcllemubacc  6603  tfrcllemex  6604  tfrcllemaccex  6605  tfrcllemres  6606  tfrcldm  6607  rdgivallem  6625  rdgival  6626  rdgss  6627  rdgisuc1  6628  rdgon  6630  rdg0  6631  frec0g  6641  frecabcl  6643  freccllem  6646  frecfcllem  6648  frecsuclem  6650  frecsuc  6651  frecrdg  6652  oav2  6709  omv2  6711  xpdom2  7095  xpmapenlem  7115  xpmapen  7116  ac6sfi  7168  1stinl  7378  2ndinl  7379  1stinr  7380  2ndinr  7381  updjudhcoinlf  7384  updjudhcoinrg  7385  caseinl  7395  caseinr  7396  omp1eomlem  7398  omp1eom  7399  difinfsn  7404  ctmlemr  7412  ctm  7413  ctssdclemn0  7414  ctssdccl  7415  nninfninc  7427  nnnninfeq  7432  nnnninfeq2  7433  enomnilem  7442  enmkvlem  7465  enwomnilem  7473  exmidfodomrlemeldju  7515  exmidfodomrlemreseldju  7516  exmidfodomrlemr  7518  exmidfodomrlemrALT  7519  exmidaclem  7528  cc2  7597  cc3  7598  ltdfpr  7837  genpelvl  7843  genpelvu  7844  recexpr  7969  cauappcvgprlem1  7990  caucvgprlemnkj  7997  caucvgprlemnbj  7998  caucvgprlemm  7999  caucvgprlemdisj  8005  caucvgprlemloc  8006  caucvgprlemcl  8007  caucvgprlemladdfu  8008  caucvgprlemladdrl  8009  caucvgprlem1  8010  caucvgprlem2  8011  caucvgpr  8013  caucvgprprlemell  8016  caucvgprprlemelu  8017  caucvgprprlemcbv  8018  caucvgprprlemval  8019  caucvgprprlemnkeqj  8021  caucvgprprlemmu  8026  caucvgprprlemopl  8028  caucvgprprlemlol  8029  caucvgprprlemopu  8030  caucvgprprlemloc  8034  caucvgprprlemclphr  8036  caucvgprprlemexbt  8037  caucvgprprlem1  8040  caucvgprprlem2  8041  caucvgsr  8133  axcaucvglemval  8228  axcaucvglemres  8230  fv0p1e1  9369  uzin  9905  cnref1o  10001  fzsuc2  10435  fseq1m1p1  10451  fzoss2  10530  elfzonlteqm1  10577  divfl0  10680  flqzadd  10682  fldiv4p1lem1div2  10689  ceilqval  10692  flqdiv  10707  modqval  10710  modqfrac  10723  modqmulnn  10728  modqid  10735  modqcyc  10745  modqdi  10778  frec2uzuzd  10788  frec2uzrdg  10795  frecuzrdgrcl  10796  frecuzrdgtcl  10798  frecuzrdgsuc  10800  frecuzrdgrclt  10801  frecuzrdgg  10802  frecuzrdgfunlem  10805  frecuzrdgsuctlem  10809  iseqovex  10844  iseqvalcbv  10845  seq3val  10846  seqvalcd  10847  seq3m1  10859  seq3shft2  10867  seqshft2g  10868  monoord  10871  monoord2  10872  iseqf1olemqval  10886  iseqf1olemab  10888  iseqf1olemqk  10893  iseqf1olemjpcl  10894  iseqf1olemqpcl  10895  iseqf1olemfvp  10896  seq3f1olemqsumkj  10897  seq3f1olemqsumk  10898  seq3f1olemqsum  10899  seq3f1olemp  10901  seq3f1oleml  10902  seqf1oglem1  10905  seqf1oglem2  10906  seqf1og  10907  seq3homo  10913  seqhomog  10916  exp3val  10927  expnegap0  10933  facnn2  11121  facwordi  11127  faclbnd6  11131  bcval  11136  bccmpl  11141  bcn0  11142  bcm1k  11147  bcp1n  11148  bcn2  11151  hashinfom  11166  hashennn  11168  hashsng  11186  omgadd  11191  hashprg  11198  fihashssdif  11208  hashdifpr  11210  hashfzo  11212  hashfzp1  11214  hashxp  11216  hashmap  11217  hashfibclem  11231  hashfibc  11232  zfz1isolemiso  11236  zfz1iso  11238  hashtpglem  11243  lsw1  11299  ccatfvalfi  11305  ccatlen  11308  ccatval3  11312  ccatval21sw  11318  ccatlid  11319  ccatass  11321  lswccatn0lsw  11324  lswccat0lsw  11325  ccatalpha  11326  s1leng  11337  ccats1val2  11353  lswccats1  11356  swrdfv0  11371  swrdfv2  11380  swrdsbslen  11383  swrds1  11385  ccatswrd  11387  pfxmpt  11397  pfxfv  11401  pfxtrcfvl  11414  ccatpfx  11418  swrdswrd  11422  lenpfxcctswrd  11428  ccatopth  11433  cats1un  11438  swrdccatin2  11446  pfxccatin12lem2  11448  shftval2  11536  shftval3  11537  shftval4  11538  shftval5  11539  seq3shft  11548  imval  11560  imre  11561  reim  11562  crim  11568  reim0  11571  mulreap  11574  recj  11577  reneg  11578  readd  11579  resub  11580  remullem  11581  redivap  11584  imcj  11585  imneg  11586  imadd  11587  imsub  11588  imdivap  11591  cjsub  11602  cjexp  11603  cjreim2  11614  cjap  11616  cjdivap  11619  cnrecnv  11620  cvg1nlemcau  11694  cvg1nlemres  11695  absval  11711  rennim  11712  sqrtdiv  11752  sqrtmsq  11755  absneg  11760  abscj  11762  absval2  11767  absreim  11778  absmul  11779  absdivap  11780  absid  11781  absre  11787  absexp  11789  absexpzap  11790  absimle  11794  abssub  11811  abs3dif  11815  abs2dif  11816  abs2dif2  11817  recan  11819  cau3lem  11824  max0addsup  11929  minabs  11946  bdtrilem  11949  clim  11991  clim2  11993  clim0  11995  clim0c  11996  climi0  11999  climconst  12000  climshftlemg  12012  climcn1  12018  climcn2  12019  addcn2  12020  subcn2  12021  mulcn2  12022  reccn2ap  12023  cjcn2  12026  recn2  12027  imcn2  12028  iser3shft  12056  climcau  12057  climcvg1nlem  12059  climcvg1n  12060  serf0  12062  fzf1o  12086  summodclem3  12091  summodclem2a  12092  summodc  12094  fsumf1o  12101  sumsnf  12120  fsumm1  12127  fsumcnv  12148  fsumabs  12176  fsumrelem  12182  iserabs  12186  hash2iun1dif1  12191  isumshft  12201  isumsplit  12202  expcnvap0  12213  expcnv  12215  cvgratnnlemseq  12237  cvgratnnlemrate  12241  cvgratz  12243  mertenslemub  12245  mertenslemi1  12246  mertenslem2  12247  mertensabs  12248  prodmodclem3  12286  fprodf1o  12299  prodsnf  12303  fprodm1  12309  fprodabs  12327  fprodcnv  12336  efcllemp  12369  efcj  12384  efaddlem  12385  efcan  12387  efsub  12392  efexp  12393  efzval  12394  efgt0  12395  eftlub  12401  efltim  12409  sinval  12413  cosval  12414  tanval3ap  12425  resinval  12426  recosval  12427  resin4p  12429  recos4p  12430  sinneg  12437  cosneg  12438  efmival  12444  efeul  12445  sinadd  12447  cosadd  12448  sinsub  12451  cossub  12452  addsin  12453  subsin  12454  addcos  12457  subcos  12458  sincossq  12459  sin2t  12460  cos2t  12461  sin01bnd  12468  cos01bnd  12469  sin02gt0  12475  cos12dec  12479  absefi  12480  absef  12481  absefib  12482  efieq1re  12483  demoivre  12484  demoivreALT  12485  flodddiv4  12647  bitsval  12654  bits0  12659  bitsp1  12662  bitsp1e  12663  bitsp1o  12664  bitsmod  12667  nninfctlemfo  12761  alginv  12769  algcvg  12770  eucalgval  12776  eucalginv  12778  eucalglt  12779  eucalgcvga  12780  eucalg  12781  lcmgcd  12800  lcm1  12803  sqpweven  12897  2sqpwodd  12898  sqne2sq  12899  qnumval  12907  qdenval  12908  qden1elz  12927  nn0sqrtelqelz  12928  phival  12935  dfphi2  12942  phiprmpw  12944  phiprm  12945  eulerthlemth  12954  hashgcdeq  12962  phisum  12963  pythagtriplem6  12993  pythagtriplem7  12994  pythagtriplem12  12998  pythagtriplem14  13000  fldivp1  13071  4sqlem11  13124  ballotfilemfval  13173  ballotfilemfp1  13175  ballotfilemfc0  13176  ballotfilemfcc  13177  ballotfilemfmpn  13178  ballotfilemsval  13196  ballotfilemgval  13211  ballotfilemgun  13212  ballotfilemfrc  13214  ballotfilemrinv0  13220  ennnfonelemg  13238  ennnfonelemp1  13241  ennnfonelemkh  13247  ennnfonelemhf1o  13248  ennnfonelemnn0  13257  ctinfomlemom  13262  ctiunctlemu1st  13269  ctiunctlemu2nd  13270  ctiunctlemudc  13272  ctiunctlemfo  13274  isstruct2im  13306  isstruct2r  13307  setsslid  13347  ressbasd  13364  resseqnbasd  13370  ressplusgd  13426  ptex  13561  imasex  13569  imasival  13570  f1ocpbl  13575  f1ovscpbl  13576  imasaddvallemg  13579  qusval  13587  fvprif  13607  xpsff1o  13613  igsumvalx  13652  gsumprval  13662  imasmnd  13708  ismhm  13716  mhmpropd  13721  mhmlin  13722  mhmf1o  13725  resmhm  13742  mhmco  13745  gsumwmhm  13753  grpinvsub  13837  imasgrp2  13863  imasgrp  13864  mhmlem  13867  mhmid  13868  mhmmnd  13869  ghmgrp  13871  mulgfvalg  13874  mulgval  13875  mulgnegnn  13885  mulgneg  13893  mulgnegneg  13894  mulgm1  13895  mulginvcom  13900  mulgz  13903  mulgnndir  13904  mulgdir  13907  mulgass  13912  mhmmulg  13916  subgmulg  13941  isnsg  13955  eqgfval  13975  ghmlin  14001  ghmid  14002  ghminv  14003  ghmsub  14004  ghmmulg  14009  resghm  14013  ghmeql  14020  ablsub2inv  14064  ghmcmn  14080  invghm  14082  imasabl  14089  gsumfzreidx  14090  gsumfzmhm  14096  gsumsplit0  14099  gfsumval  14102  gsumshift  14105  gfsump1  14108  prdsex  14114  prdsval  14115  prdsbas3  14129  pwsval  14146  pwsbas  14147  pwsplusgval  14150  pwsmulrval  14151  pws0g  14155  pwsinvg  14157  mgpplusgg  14163  mgpbasg  14165  mgpscag  14166  mgptsetg  14167  mgpdsg  14169  rngm2neg  14188  imasrng  14195  isring  14243  ringm2neg  14298  imasring  14307  opprmulfvalg  14313  opprsllem  14317  isunitd  14351  opprunitd  14355  invrfvald  14367  rdivmuldivd  14389  rhmmul  14409  isrhm2d  14410  rhm1  14412  rhmdvdsr  14420  rhmopp  14421  rhmunitinv  14423  islmod  14565  islmodd  14567  scaffvalg  14580  lmodpropd  14623  lsssetm  14630  islssmd  14633  lssats2  14688  lspsnneg  14694  lspsnsub  14695  lspun0  14699  lmodindp1  14702  sralemg  14712  srascag  14716  sravscag  14717  sraipg  14718  rlmscabas  14734  ixpsnbasval  14740  2idlval  14776  2idlvalg  14777  mulgrhm2  14884  zlmlemg  14902  zlmsca  14906  zlmvscag  14907  znval  14910  znle  14911  znbaslemnn  14913  znidomb  14932  psrval  14940  psrbasg  14955  psrplusgg  14959  mplvalcoe  14971  mplsubgfileminv  14981  mpl0fi  14983  mplnegfi  14986  istps  15023  tpspropd  15027  eltpsg  15031  txvalex  15245  txval  15246  txbasval  15258  upxp  15263  uptx  15265  txrest  15267  cnmpt11  15274  cnmpt21  15282  hmeontr  15304  txhmeo  15310  psmetxrge0  15323  xmetunirn  15349  mopnval  15433  mopntopon  15434  isxms  15442  isxms2  15443  isms  15444  msrtri  15467  xmspropd  15468  mspropd  15469  setsmsbasg  15470  setsmsdsg  15471  setsmstsetg  15472  comet  15490  metcnpi  15506  metcnpi2  15507  cnbl0  15525  cnblcld  15526  resubmet  15547  mpomulcn  15557  elcncf  15564  cncfi  15569  rescncf  15572  mulc1cncf  15580  cncfco  15582  cncfmptid  15588  addccncf  15591  cdivcncfap  15595  negcncf  15596  mulcncflem  15598  ivthinclemlopn  15627  ivthinclemuopn  15629  limccl  15650  ellimc3apf  15651  limcimolemlt  15655  cnplimclemle  15659  limccnpcntop  15666  reldvg  15670  dvfvalap  15672  dveflem  15717  dvef  15718  plymullem1  15739  plycjlemc  15751  plycj  15752  plyrecj  15754  plyreres  15755  sin0pilem1  15772  ef2kpi  15797  sinperlem  15799  sin2kpi  15802  cos2kpi  15803  sin2pim  15804  cos2pim  15805  ptolemy  15815  sincosq2sgn  15818  sincosq3sgn  15819  sincosq4sgn  15820  sinq12gt0  15821  tangtx  15829  sincosq1eq  15830  abssinper  15837  sinkpi  15838  coskpi  15839  cosq34lt1  15841  relogeftb  15856  relogoprlem  15859  relogexp  15863  rpcxpef  15885  logcxp  15888  1cxp  15891  ecxp  15892  rpcxpadd  15896  rpmulcxp  15900  cxpmul  15903  abscxp  15906  logsqrt  15914  rpabscxpbnd  15931  rpcxplogb  15955  pellexlem1  15971  pellexlem2  15972  pellexlem3  15973  lgsval  16003  lgsval2lem  16009  lgsval4a  16021  lgsdi  16036  lgseisenlem3  16071  lgseisenlem4  16072  lgsquadlem1  16076  lgsquadlem2  16077  lgsquadlem3  16078  2lgslem1  16090  2lgslem3a  16092  2lgslem3b  16093  2lgslem3c  16094  2lgslem3d  16095  vtxdgfval  16409  vtxdgfifival  16412  vtxdgop  16413  vtxdgfi0e  16416  vtxdeqd  16417  vtxdfifiun  16418  vtxdumgrfival  16419  1hevtxdg1en  16429  iswlk  16444  2wlklem  16497  wlkres  16500  clwwlkccatlem  16521  clwwlkn2  16542  clwwlkext2edg  16543  umgr2cwwk2dif  16545  clwwlknonex2lem2  16559  eupth2fi  16600  eulerpathprum  16601  depindlem1  16627  depind  16630  nnsf  16909  peano4nninf  16910  peano3nninf  16911  nninfalllem1  16912  nninfall  16913  nninfsellemdc  16914  nninfsellemeq  16918  nninfsellemqall  16919  nninfsellemeqinf  16920  nninfsel  16921  nnnninfex  16926  exmidsbthr  16929  qdencn  16933  refeq  16934  repiecele0  16936  repiecege0  16937  repiecef  16938  isomninnlem  16940  apdifflemr  16957  apdiff  16958  qdiff  16959  ismkvnnlem  16963  nconstwlpolem  16977