Theorem fveq2d 5702

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

This proof depends on syntax axioms:   → wi 4   = wceq 1402  ‘cfv 5380

This proof depends on 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 proof 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 3715  df-pr 3716  df-op 3718  df-uni 3936  df-br 4132  df-iota 5340  df-fv 5388

This theorem is used by:  2fveq3  5703  fveq12d  5705  fveqeq2d  5706  csbfvg  5741  fvmptdf  5796  fvmptt  5800  resfvresima  5959  fcof1  5992  oveq1  6095  oveq2  6096  fvoveq1d  6110  caofinvl  6332  op1stg  6388  op2ndg  6389  ot1stg  6390  ot2ndg  6391  eloprabi  6436  1stconst  6461  algrflemg  6470  tfrlem1  6583  tfrlem3ag  6584  tfrlem3a  6585  tfrlem9  6594  tfr0dm  6597  tfrlemisucaccv  6600  tfrlemiubacc  6605  tfrlemiex  6606  tfrlemi1  6607  tfr1onlem3ag  6612  tfr1onlemsucaccv  6616  tfr1onlemubacc  6621  tfr1onlemex  6622  tfr1onlemaccex  6623  tfrcllemsucaccv  6629  tfrcllembxssdm  6631  tfrcllemubacc  6634  tfrcllemex  6635  tfrcllemaccex  6636  tfrcllemres  6637  tfrcldm  6638  rdgivallem  6656  rdgival  6657  rdgss  6658  rdgisuc1  6659  rdgon  6661  rdg0  6662  frec0g  6672  frecabcl  6674  freccllem  6677  frecfcllem  6679  frecsuclem  6681  frecsuc  6682  frecrdg  6683  oav2  6740  omv2  6742  xpdom2  7133  xpmapenlem  7153  xpmapen  7154  ac6sfi  7206  1stinl  7420  2ndinl  7421  1stinr  7422  2ndinr  7423  updjudhcoinlf  7426  updjudhcoinrg  7427  caseinl  7437  caseinr  7438  omp1eomlem  7440  omp1eom  7441  difinfsn  7446  ctmlemr  7454  ctm  7455  ctssdclemn0  7456  ctssdccl  7457  nninfninc  7469  nnnninfeq  7474  nnnninfeq2  7475  enomnilem  7484  enmkvlem  7507  enwomnilem  7515  exmidfodomrlemeldju  7557  exmidfodomrlemreseldju  7558  exmidfodomrlemr  7560  exmidfodomrlemrALT  7561  exmidaclem  7570  cc2  7639  cc3  7640  ltdfpr  7879  genpelvl  7885  genpelvu  7886  recexpr  8011  cauappcvgprlem1  8032  caucvgprlemnkj  8039  caucvgprlemnbj  8040  caucvgprlemm  8041  caucvgprlemdisj  8047  caucvgprlemloc  8048  caucvgprlemcl  8049  caucvgprlemladdfu  8050  caucvgprlemladdrl  8051  caucvgprlem1  8052  caucvgprlem2  8053  caucvgpr  8055  caucvgprprlemell  8058  caucvgprprlemelu  8059  caucvgprprlemcbv  8060  caucvgprprlemval  8061  caucvgprprlemnkeqj  8063  caucvgprprlemmu  8068  caucvgprprlemopl  8070  caucvgprprlemlol  8071  caucvgprprlemopu  8072  caucvgprprlemloc  8076  caucvgprprlemclphr  8078  caucvgprprlemexbt  8079  caucvgprprlem1  8082  caucvgprprlem2  8083  caucvgsr  8175  axcaucvglemval  8270  axcaucvglemres  8272  fv0p1e1  9428  uzin  9971  cnref1o  10068  fzsuc2  10503  fseq1m1p1  10519  fzoss2  10598  elfzonlteqm1  10645  divfl0  10752  flqzadd  10754  fldiv4p1lem1div2  10761  ceilqval  10764  flqdiv  10779  modqval  10782  modqfrac  10795  modqmulnn  10800  modqid  10807  modqcyc  10817  modqdi  10850  frec2uzuzd  10860  frec2uzrdg  10867  frecuzrdgrcl  10868  frecuzrdgtcl  10870  frecuzrdgsuc  10872  frecuzrdgrclt  10873  frecuzrdgg  10874  frecuzrdgfunlem  10877  frecuzrdgsuctlem  10881  iseqovex  10916  iseqvalcbv  10917  seq3val  10918  seqvalcd  10919  seq3m1  10931  seq3shft2  10939  seqshft2g  10940  monoord  10943  monoord2  10944  iseqf1olemqval  10958  iseqf1olemab  10960  iseqf1olemqk  10965  iseqf1olemjpcl  10966  iseqf1olemqpcl  10967  iseqf1olemfvp  10968  seq3f1olemqsumkj  10969  seq3f1olemqsumk  10970  seq3f1olemqsum  10971  seq3f1olemp  10973  seq3f1oleml  10974  seqf1oglem1  10977  seqf1oglem2  10978  seqf1og  10979  seq3homo  10985  seqhomog  10988  exp3val  10999  expnegap0  11005  facnn2  11194  facwordi  11200  faclbnd6  11204  bcval  11209  bccmpl  11214  bcn0  11215  bcm1k  11220  bcp1n  11221  bcn2  11224  hashinfom  11239  hashennn  11241  hashsng  11259  omgadd  11264  hashprg  11271  fihashssdif  11281  hashdifpr  11283  hashfzo  11285  hashfzp1  11287  hashxp  11289  hashmap  11290  hashfibclem  11304  hashfibc  11305  hashf1lem2  11308  hashf1  11309  hashfac  11310  zfz1isolemiso  11313  zfz1iso  11315  hashtpglem  11320  lsw1  11376  ccatfvalfi  11382  ccatlen  11385  ccatval3  11389  ccatval21sw  11395  ccatlid  11396  ccatass  11398  lswccatn0lsw  11401  lswccat0lsw  11402  ccatalpha  11403  s1leng  11414  ccats1val2  11430  lswccats1  11433  swrdfv0  11448  swrdfv2  11457  swrdsbslen  11460  swrds1  11462  ccatswrd  11464  pfxmpt  11474  pfxfv  11478  pfxtrcfvl  11491  ccatpfx  11495  swrdswrd  11499  lenpfxcctswrd  11505  ccatopth  11510  cats1un  11515  swrdccatin2  11523  pfxccatin12lem2  11525  shftval2  11613  shftval3  11614  shftval4  11615  shftval5  11616  seq3shft  11625  imval  11637  imre  11638  reim  11639  crim  11645  reim0  11648  mulreap  11651  recj  11654  reneg  11655  readd  11656  resub  11657  remullem  11658  redivap  11661  imcj  11662  imneg  11663  imadd  11664  imsub  11665  imdivap  11668  cjsub  11679  cjexp  11680  cjreim2  11692  cjap  11694  cjdivap  11697  cnrecnv  11698  cvg1nlemcau  11772  cvg1nlemres  11773  absval  11789  rennim  11790  sqrtdiv  11830  sqrtmsq  11833  absneg  11838  abscj  11840  absval2  11845  absreim  11856  absmul  11857  absdivap  11858  absid  11859  absre  11866  absexp  11868  absexpzap  11869  absimle  11873  abssub  11890  abs3dif  11894  abs2dif  11895  abs2dif2  11896  recan  11898  cau3lem  11903  max0addsup  12008  minabs  12026  bdtrilem  12030  clim  12072  clim2  12074  clim0  12076  clim0c  12077  climi0  12080  climconst  12081  climshftlemg  12093  climcn1  12099  climcn2  12100  addcn2  12101  subcn2  12102  mulcn2  12103  reccn2ap  12104  cjcn2  12107  recn2  12108  imcn2  12109  iser3shft  12137  climcau  12138  climcvg1nlem  12140  climcvg1n  12141  serf0  12143  fzf1o  12167  summodclem3  12172  summodclem2a  12173  summodc  12175  fsumf1o  12182  sumsnf  12201  fsumm1  12208  fsumcnv  12229  fsumabs  12257  fsumrelem  12263  iserabs  12267  hash2iun1dif1  12272  isumshft  12282  isumsplit  12283  expcnvap0  12294  expcnv  12296  cvgratnnlemseq  12318  cvgratnnlemrate  12322  cvgratz  12324  mertenslemub  12326  mertenslemi1  12327  mertenslem2  12328  mertensabs  12329  prodmodclem3  12367  fprodf1o  12380  prodsnf  12384  fprodm1  12390  fprodabs  12408  fprodcnv  12417  efcllemp  12450  efcj  12465  efaddlem  12466  efcan  12468  efsub  12473  efexp  12474  efzval  12475  efgt0  12476  eftlub  12482  efltim  12490  sinval  12494  cosval  12495  tanval3ap  12506  resinval  12507  recosval  12508  resin4p  12510  recos4p  12511  sinneg  12518  cosneg  12519  efmival  12525  efeul  12526  sinadd  12528  cosadd  12529  sinsub  12532  cossub  12533  addsin  12534  subsin  12535  addcos  12538  subcos  12539  sincossq  12540  sin2t  12541  cos2t  12542  sin01bnd  12549  cos01bnd  12550  sin02gt0  12556  cos12dec  12560  absefi  12561  absef  12562  absefib  12563  efieq1re  12564  demoivre  12565  demoivreALT  12566  flodddiv4  12728  bitsval  12735  bits0  12740  bitsp1  12743  bitsp1e  12744  bitsp1o  12745  bitsmod  12748  nninfctlemfo  12842  alginv  12850  algcvg  12851  eucalgval  12857  eucalginv  12859  eucalglt  12860  eucalgcvga  12861  eucalg  12862  lcmgcd  12881  lcm1  12884  sqpweven  12980  2sqpwodd  12981  sqne2sq  12982  qnumval  12990  qdenval  12991  qden1elz  13010  nn0sqrtelqelz  13011  nn0sqdcq  13013  sqrtrirr  13014  phival  13020  dfphi2  13027  phiprmpw  13029  phiprm  13030  eulerthlemth  13039  hashgcdeq  13047  phisum  13048  pythagtriplem6  13078  pythagtriplem7  13079  pythagtriplem12  13083  pythagtriplem14  13085  fldivp1  13156  4sqlem11  13209  prmlem0  13249  ballotfilemfval  13287  ballotfilemfp1  13289  ballotfilemfc0  13290  ballotfilemfcc  13291  ballotfilemfmpn  13292  ballotfilemsval  13310  ballotfilemgval  13325  ballotfilemgun  13326  ballotfilemfrc  13328  ballotfilemrinv0  13334  ennnfonelemg  13352  ennnfonelemp1  13355  ennnfonelemkh  13361  ennnfonelemhf1o  13362  ennnfonelemnn0  13371  ctinfomlemom  13376  ctiunctlemu1st  13383  ctiunctlemu2nd  13384  ctiunctlemudc  13386  ctiunctlemfo  13388  isstruct2im  13420  isstruct2r  13421  setsslid  13461  ressbasd  13480  resseqnbasd  13486  ressplusgd  13542  ptex  13677  imasex  13685  imasival  13686  f1ocpbl  13691  f1ovscpbl  13692  imasaddvallemg  13695  qusval  13703  fvprif  13723  xpsff1o  13729  gzsumvalx  13768  imasmnd  13819  ismhm  13827  mhmpropd  13832  mhmlin  13833  mhmf1o  13836  resmhm  13853  mhmco  13856  gzsumwmhm  13862  grpinvsub  13946  imasgrp2  13972  imasgrp  13973  mhmlem  13976  mhmid  13977  mhmmnd  13978  ghmgrp  13980  mulgfvalg  13983  mulgval  13984  mulgnegnn  13994  mulgneg  14002  mulgnegneg  14003  mulgm1  14004  mulginvcom  14009  mulgz  14012  mulgnndir  14013  mulgdir  14016  mulgass  14021  mhmmulg  14025  subgmulg  14050  isnsg  14064  eqgfval  14084  ghmlin  14110  ghmid  14111  ghminv  14112  ghmsub  14113  ghmmulg  14118  resghm  14122  ghmeql  14129  cntzmhm  14173  ablsub2inv  14205  ghmcmn  14221  invghm  14223  imasabl  14230  gzsumreidx  14231  gzsummhm  14235  gzsumsplit0  14238  gzsumshift  14239  gsumvalfi  14242  gsump1  14247  gsumf1ofi  14250  gsummhmfi  14264  gsum2dfilem2  14272  gsumcom2fi  14275  prdsex  14279  prdsval  14280  prdsbas3  14294  pwsval  14311  pwsbas  14312  pwsplusgval  14315  pwsmulrval  14316  pws0g  14320  pwsinvg  14322  mgpplusgg  14328  mgpbasg  14331  mgpscag  14333  mgptsetg  14334  mgpdsg  14336  rngm2neg  14355  imasrng  14362  isring  14411  ringm2neg  14467  imasring  14478  opprmulfvalg  14484  opprsllem  14488  isunitd  14522  opprunitd  14526  invrfvald  14538  rdivmuldivd  14560  rhmmul  14580  isrhm2d  14581  rhm1  14583  rhmdvdsr  14591  rhmopp  14592  rhmunitinv  14594  islmod  14736  islmodd  14738  scaffvalg  14752  lmodpropd  14795  lsssetm  14802  islssmd  14805  lssats2  14860  lspsnneg  14866  lspsnsub  14867  lspun0  14871  lmodindp1  14874  sralemg  14884  srascag  14888  sravscag  14889  sraipg  14890  rlmscabas  14906  ixpsnbasval  14912  2idlval  14948  2idlvalg  14949  mulgrhm2  15054  zlmlemg  15072  zlmsca  15076  zlmvscag  15077  znval  15080  znle  15081  znbaslemnn  15083  znidomb  15102  isassad  15120  assapropd  15123  asclfval  15130  ressascl  15148  assamulgscmlem2  15151  psrval  15159  psrbasg  15178  psrplusgg  15182  psrlidmfi  15199  psrridmfi  15200  psrass1fi  15201  mplvalcoe  15206  mplsubgfileminv  15216  mpl0fi  15218  mplnegfi  15221  istps  15258  tpspropd  15262  eltpsg  15266  txvalex  15480  txval  15481  txbasval  15493  upxp  15498  uptx  15500  txrest  15502  cnmpt11  15509  cnmpt21  15517  hmeontr  15539  txhmeo  15545  psmetxrge0  15558  xmetunirn  15584  mopnval  15668  mopntopon  15669  isxms  15677  isxms2  15678  isms  15679  msrtri  15702  xmspropd  15703  mspropd  15704  setsmsbasg  15705  setsmsdsg  15706  setsmstsetg  15707  comet  15725  metcnpi  15741  metcnpi2  15742  cnbl0  15760  cnblcld  15761  resubmet  15782  mpomulcn  15792  elcncf  15799  cncfi  15804  rescncf  15807  mulc1cncf  15815  cncfco  15817  cncfmptid  15823  addccncf  15826  cdivcncfap  15830  negcncf  15831  mulcncflem  15833  ivthinclemlopn  15862  ivthinclemuopn  15864  limccl  15885  ellimc3apf  15886  limcimolemlt  15890  cnplimclemle  15894  limccnpcntop  15901  reldvg  15905  dvfvalap  15907  dveflem  15952  dvef  15953  plymullem1  15974  plycjlemc  15986  plycj  15987  plyrecj  15989  plyreres  15990  sin0pilem1  16008  ef2kpi  16033  sinperlem  16035  sin2kpi  16038  cos2kpi  16039  sin2pim  16040  cos2pim  16041  ptolemy  16051  sincosq2sgn  16054  sincosq3sgn  16055  sincosq4sgn  16056  sinq12gt0  16057  tangtx  16065  sincosq1eq  16066  abssinper  16073  sinkpi  16074  coskpi  16075  sineq0re  16076  cosq34lt1  16078  root1idef  16084  relogeftb  16094  relogoprlem  16098  relogexp  16102  logfac  16126  rpcxpef  16127  logcxp  16130  1cxp  16133  ecxp  16134  rpcxpadd  16138  rpmulcxp  16142  cxpmul  16145  abscxp  16150  logsqrt  16158  rpabscxpbnd  16175  rpcxplogb  16200  zprmlogbaplem3  16217  birthdaylem2  16226  birthdaylem3  16227  pellexlem1  16229  pellexlem2  16230  pellexlem3  16231  efchtqcl  16246  ppiqval  16248  ppival2  16249  ppival2g  16250  ppiprm  16259  ppinprm  16260  ppiqfl  16266  ppiqp1le  16267  ppidif  16269  ppiqltx  16281  prmorcht  16282  chtublem  16295  chtqub  16296  bcctr  16302  bcmono  16304  bposlem2  16312  bposlem6  16316  bposlem7  16317  bposlem8  16318  bposlem9  16319  lgsval  16328  lgsval2lem  16334  lgsval4a  16346  lgsdi  16361  lgseisenlem3  16396  lgseisenlem4  16397  lgsquadlem1  16401  lgsquadlem2  16402  lgsquadlem3  16403  2lgslem1  16415  2lgslem3a  16417  2lgslem3b  16418  2lgslem3c  16419  2lgslem3d  16420  vtxdgfval  16734  vtxdgfifival  16737  vtxdgop  16738  vtxdgfi0e  16741  vtxdeqd  16742  vtxdfifiun  16743  vtxdumgrfival  16744  1hevtxdg1en  16754  iswlk  16769  2wlklem  16822  wlkres  16825  clwwlkccatlem  16846  clwwlkn2  16867  clwwlkext2edg  16868  umgr2cwwk2dif  16870  clwwlknonex2lem2  16884  eupth2fi  16925  eulerpathprum  16926  depindlem1  16952  depind  16955  nnsf  17254  peano4nninf  17255  peano3nninf  17256  nninfalllem1  17257  nninfall  17258  nninfsellemdc  17259  nninfsellemeq  17263  nninfsellemqall  17264  nninfsellemeqinf  17265  nninfsel  17266  nnnninfex  17271  exmidsbthr  17274  qdencn  17278  refeq  17279  repiecele0  17281  repiecege0  17282  repiecef  17283  isomninnlem  17285  apdifflemr  17303  apdiff  17304  qdiff  17305  ismkvnnlem  17309  nconstwlpolem  17322