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  6584  tfrlem3ag  6585  tfrlem3a  6586  tfrlem9  6595  tfr0dm  6598  tfrlemisucaccv  6601  tfrlemiubacc  6606  tfrlemiex  6607  tfrlemi1  6608  tfr1onlem3ag  6613  tfr1onlemsucaccv  6617  tfr1onlemubacc  6622  tfr1onlemex  6623  tfr1onlemaccex  6624  tfrcllemsucaccv  6630  tfrcllembxssdm  6632  tfrcllemubacc  6635  tfrcllemex  6636  tfrcllemaccex  6637  tfrcllemres  6638  tfrcldm  6639  rdgivallem  6657  rdgival  6658  rdgss  6659  rdgisuc1  6660  rdgon  6662  rdg0  6663  frec0g  6673  frecabcl  6675  freccllem  6678  frecfcllem  6680  frecsuclem  6682  frecsuc  6683  frecrdg  6684  oav2  6741  omv2  6743  xpdom2  7135  xpmapenlem  7155  xpmapen  7156  ac6sfi  7208  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  9970  cnref1o  10067  fzsuc2  10502  fseq1m1p1  10518  fzoss2  10597  elfzonlteqm1  10644  divfl0  10751  flqzadd  10753  fldiv4p1lem1div2  10760  ceilqval  10763  flqdiv  10778  modqval  10781  modqfrac  10794  modqmulnn  10799  modqid  10806  modqcyc  10816  modqdi  10849  frec2uzuzd  10859  frec2uzrdg  10866  frecuzrdgrcl  10867  frecuzrdgtcl  10869  frecuzrdgsuc  10871  frecuzrdgrclt  10872  frecuzrdgg  10873  frecuzrdgfunlem  10876  frecuzrdgsuctlem  10880  iseqovex  10915  iseqvalcbv  10916  seq3val  10917  seqvalcd  10918  seq3m1  10930  seq3shft2  10938  seqshft2g  10939  monoord  10942  monoord2  10943  iseqf1olemqval  10957  iseqf1olemab  10959  iseqf1olemqk  10964  iseqf1olemjpcl  10965  iseqf1olemqpcl  10966  iseqf1olemfvp  10967  seq3f1olemqsumkj  10968  seq3f1olemqsumk  10969  seq3f1olemqsum  10970  seq3f1olemp  10972  seq3f1oleml  10973  seqf1oglem1  10976  seqf1oglem2  10977  seqf1og  10978  seq3homo  10984  seqhomog  10987  exp3val  10998  expnegap0  11004  facnn2  11193  facwordi  11199  faclbnd6  11203  bcval  11208  bccmpl  11213  bcn0  11214  bcm1k  11219  bcp1n  11220  bcn2  11223  hashinfom  11238  hashennn  11240  hashsng  11258  omgadd  11263  hashprg  11270  fihashssdif  11280  hashdifpr  11282  hashfzo  11284  hashfzp1  11286  hashxp  11288  hashmap  11289  hashfibclem  11303  hashfibc  11304  hashf1lem2  11307  hashf1  11308  hashfac  11309  zfz1isolemiso  11312  zfz1iso  11314  hashtpglem  11319  lsw1  11375  ccatfvalfi  11381  ccatlen  11384  ccatval3  11388  ccatval21sw  11394  ccatlid  11395  ccatass  11397  lswccatn0lsw  11400  lswccat0lsw  11401  ccatalpha  11402  s1leng  11413  ccats1val2  11429  lswccats1  11432  swrdfv0  11447  swrdfv2  11456  swrdsbslen  11459  swrds1  11461  ccatswrd  11463  pfxmpt  11473  pfxfv  11477  pfxtrcfvl  11490  ccatpfx  11494  swrdswrd  11498  lenpfxcctswrd  11504  ccatopth  11509  cats1un  11514  swrdccatin2  11522  pfxccatin12lem2  11524  shftval2  11612  shftval3  11613  shftval4  11614  shftval5  11615  seq3shft  11624  imval  11636  imre  11637  reim  11638  crim  11644  reim0  11647  mulreap  11650  recj  11653  reneg  11654  readd  11655  resub  11656  remullem  11657  redivap  11660  imcj  11661  imneg  11662  imadd  11663  imsub  11664  imdivap  11667  cjsub  11678  cjexp  11679  cjreim2  11691  cjap  11693  cjdivap  11696  cnrecnv  11697  cvg1nlemcau  11771  cvg1nlemres  11772  absval  11788  rennim  11789  sqrtdiv  11829  sqrtmsq  11832  absneg  11837  abscj  11839  absval2  11844  absreim  11855  absmul  11856  absdivap  11857  absid  11858  absre  11865  absexp  11867  absexpzap  11868  absimle  11872  abssub  11889  abs3dif  11893  abs2dif  11894  abs2dif2  11895  recan  11897  cau3lem  11902  max0addsup  12007  minabs  12025  bdtrilem  12029  clim  12071  clim2  12073  clim0  12075  clim0c  12076  climi0  12079  climconst  12080  climshftlemg  12092  climcn1  12098  climcn2  12099  addcn2  12100  subcn2  12101  mulcn2  12102  reccn2ap  12103  cjcn2  12106  recn2  12107  imcn2  12108  iser3shft  12136  climcau  12137  climcvg1nlem  12139  climcvg1n  12140  serf0  12142  fzf1o  12166  summodclem3  12171  summodclem2a  12172  summodc  12174  fsumf1o  12181  sumsnf  12200  fsumm1  12207  fsumcnv  12228  fsumabs  12256  fsumrelem  12262  iserabs  12266  hash2iun1dif1  12271  isumshft  12281  isumsplit  12282  expcnvap0  12293  expcnv  12295  cvgratnnlemseq  12317  cvgratnnlemrate  12321  cvgratz  12323  mertenslemub  12325  mertenslemi1  12326  mertenslem2  12327  mertensabs  12328  prodmodclem3  12366  fprodf1o  12379  prodsnf  12383  fprodm1  12389  fprodabs  12407  fprodcnv  12416  efcllemp  12449  efcj  12464  efaddlem  12465  efcan  12467  efsub  12472  efexp  12473  efzval  12474  efgt0  12475  eftlub  12481  efltim  12489  sinval  12493  cosval  12494  tanval3ap  12505  resinval  12506  recosval  12507  resin4p  12509  recos4p  12510  sinneg  12517  cosneg  12518  efmival  12524  efeul  12525  sinadd  12527  cosadd  12528  sinsub  12531  cossub  12532  addsin  12533  subsin  12534  addcos  12537  subcos  12538  sincossq  12539  sin2t  12540  cos2t  12541  sin01bnd  12548  cos01bnd  12549  sin02gt0  12555  cos12dec  12559  absefi  12560  absef  12561  absefib  12562  efieq1re  12563  demoivre  12564  demoivreALT  12565  flodddiv4  12727  bitsval  12734  bits0  12739  bitsp1  12742  bitsp1e  12743  bitsp1o  12744  bitsmod  12747  nninfctlemfo  12841  alginv  12849  algcvg  12850  eucalgval  12856  eucalginv  12858  eucalglt  12859  eucalgcvga  12860  eucalg  12861  lcmgcd  12880  lcm1  12883  sqpweven  12979  2sqpwodd  12980  sqne2sq  12981  qnumval  12989  qdenval  12990  qden1elz  13009  nn0sqrtelqelz  13010  nn0sqdcq  13012  sqrtrirr  13013  phival  13019  dfphi2  13026  phiprmpw  13028  phiprm  13029  eulerthlemth  13038  hashgcdeq  13046  phisum  13047  pythagtriplem6  13077  pythagtriplem7  13078  pythagtriplem12  13082  pythagtriplem14  13084  fldivp1  13155  4sqlem11  13208  prmlem0  13248  ballotfilemfval  13286  ballotfilemfp1  13288  ballotfilemfc0  13289  ballotfilemfcc  13290  ballotfilemfmpn  13291  ballotfilemsval  13309  ballotfilemgval  13324  ballotfilemgun  13325  ballotfilemfrc  13327  ballotfilemrinv0  13333  ennnfonelemg  13351  ennnfonelemp1  13354  ennnfonelemkh  13360  ennnfonelemhf1o  13361  ennnfonelemnn0  13370  ctinfomlemom  13375  ctiunctlemu1st  13382  ctiunctlemu2nd  13383  ctiunctlemudc  13385  ctiunctlemfo  13387  isstruct2im  13419  isstruct2r  13420  setsslid  13460  ressbasd  13479  resseqnbasd  13485  ressplusgd  13541  ptex  13676  imasex  13684  imasival  13685  f1ocpbl  13690  f1ovscpbl  13691  imasaddvallemg  13694  qusval  13702  fvprif  13722  xpsff1o  13728  gzsumvalx  13767  imasmnd  13818  ismhm  13826  mhmpropd  13831  mhmlin  13832  mhmf1o  13835  resmhm  13852  mhmco  13855  gzsumwmhm  13861  grpinvsub  13945  imasgrp2  13971  imasgrp  13972  mhmlem  13975  mhmid  13976  mhmmnd  13977  ghmgrp  13979  mulgfvalg  13982  mulgval  13983  mulgnegnn  13993  mulgneg  14001  mulgnegneg  14002  mulgm1  14003  mulginvcom  14008  mulgz  14011  mulgnndir  14012  mulgdir  14015  mulgass  14020  mhmmulg  14024  subgmulg  14049  isnsg  14063  eqgfval  14083  ghmlin  14109  ghmid  14110  ghminv  14111  ghmsub  14112  ghmmulg  14117  resghm  14121  ghmeql  14128  cntzmhm  14172  ablsub2inv  14204  ghmcmn  14220  invghm  14222  imasabl  14229  gzsumreidx  14230  gzsummhm  14234  gzsumsplit0  14237  gzsumshift  14238  gsumvalfi  14241  gsump1  14246  gsumf1ofi  14249  gsummhmfi  14263  gsum2dfilem2  14271  gsumcom2fi  14274  prdsex  14278  prdsval  14279  prdsbas3  14293  pwsval  14310  pwsbas  14311  pwsplusgval  14314  pwsmulrval  14315  pws0g  14319  pwsinvg  14321  mgpplusgg  14327  mgpbasg  14330  mgpscag  14332  mgptsetg  14333  mgpdsg  14335  rngm2neg  14354  imasrng  14361  isring  14410  ringm2neg  14466  imasring  14477  opprmulfvalg  14483  opprsllem  14487  isunitd  14521  opprunitd  14525  invrfvald  14537  rdivmuldivd  14559  rhmmul  14579  isrhm2d  14580  rhm1  14582  rhmdvdsr  14590  rhmopp  14591  rhmunitinv  14593  islmod  14735  islmodd  14737  scaffvalg  14751  lmodpropd  14794  lsssetm  14801  islssmd  14804  lssats2  14859  lspsnneg  14865  lspsnsub  14866  lspun0  14870  lmodindp1  14873  sralemg  14883  srascag  14887  sravscag  14888  sraipg  14889  rlmscabas  14905  ixpsnbasval  14911  2idlval  14947  2idlvalg  14948  mulgrhm2  15053  zlmlemg  15071  zlmsca  15075  zlmvscag  15076  znval  15079  znle  15080  znbaslemnn  15082  znidomb  15101  isassad  15119  assapropd  15122  asclfval  15129  ressascl  15147  assamulgscmlem2  15150  psrval  15160  psrbasg  15187  psrplusgg  15191  psrlidmfi  15208  psrridmfi  15209  psrass1fi  15210  mvrfval  15214  mplvalg  15222  mplsubgfileminv  15233  mpl0fi  15235  mplnegfi  15238  istps  15275  tpspropd  15279  eltpsg  15283  txvalex  15497  txval  15498  txbasval  15510  upxp  15515  uptx  15517  txrest  15519  cnmpt11  15526  cnmpt21  15534  hmeontr  15556  txhmeo  15562  psmetxrge0  15575  xmetunirn  15601  mopnval  15685  mopntopon  15686  isxms  15694  isxms2  15695  isms  15696  msrtri  15719  xmspropd  15720  mspropd  15721  setsmsbasg  15722  setsmsdsg  15723  setsmstsetg  15724  comet  15742  metcnpi  15758  metcnpi2  15759  cnbl0  15777  cnblcld  15778  resubmet  15799  mpomulcn  15809  elcncf  15816  cncfi  15821  rescncf  15824  mulc1cncf  15832  cncfco  15834  cncfmptid  15840  addccncf  15843  cdivcncfap  15847  negcncf  15848  mulcncflem  15850  ivthinclemlopn  15879  ivthinclemuopn  15881  limccl  15902  ellimc3apf  15903  limcimolemlt  15907  cnplimclemle  15911  limccnpcntop  15918  reldvg  15922  dvfvalap  15924  dveflem  15969  dvef  15970  plymullem1  15991  plycjlemc  16003  plycj  16004  plyrecj  16006  plyreres  16007  sin0pilem1  16025  ef2kpi  16050  sinperlem  16052  sin2kpi  16055  cos2kpi  16056  sin2pim  16057  cos2pim  16058  ptolemy  16068  sincosq2sgn  16071  sincosq3sgn  16072  sincosq4sgn  16073  sinq12gt0  16074  tangtx  16082  sincosq1eq  16083  abssinper  16090  sinkpi  16091  coskpi  16092  sineq0re  16093  cosq34lt1  16095  root1idef  16101  relogeftb  16111  relogoprlem  16115  relogexp  16119  logfac  16143  rpcxpef  16144  logcxp  16147  1cxp  16150  ecxp  16151  rpcxpadd  16155  rpmulcxp  16159  cxpmul  16162  abscxp  16167  logsqrt  16175  rpabscxpbnd  16192  rpcxplogb  16217  zprmlogbaplem3  16234  birthdaylem2  16243  birthdaylem3  16244  pellexlem1  16246  pellexlem2  16247  pellexlem3  16248  efchtqcl  16263  ppiqval  16265  ppival2  16266  ppival2g  16267  ppiprm  16276  ppinprm  16277  ppiqfl  16283  ppiqp1le  16284  ppidif  16286  ppiqltx  16298  prmorcht  16299  chtublem  16312  chtqub  16313  bcctr  16319  bcmono  16321  bposlem2  16329  bposlem6  16333  bposlem7  16334  bposlem8  16335  bposlem9  16336  lgsval  16345  lgsval2lem  16351  lgsval4a  16363  lgsdi  16378  lgseisenlem3  16413  lgseisenlem4  16414  lgsquadlem1  16418  lgsquadlem2  16419  lgsquadlem3  16420  2lgslem1  16432  2lgslem3a  16434  2lgslem3b  16435  2lgslem3c  16436  2lgslem3d  16437  vtxdgfval  16751  vtxdgfifival  16754  vtxdgop  16755  vtxdgfi0e  16758  vtxdeqd  16759  vtxdfifiun  16760  vtxdumgrfival  16761  1hevtxdg1en  16771  iswlk  16786  2wlklem  16839  wlkres  16842  clwwlkccatlem  16863  clwwlkn2  16884  clwwlkext2edg  16885  umgr2cwwk2dif  16887  clwwlknonex2lem2  16901  eupth2fi  16942  eulerpathprum  16943  depindlem1  16969  depind  16972  nnsf  17271  peano4nninf  17272  peano3nninf  17273  nninfalllem1  17274  nninfall  17275  nninfsellemdc  17276  nninfsellemeq  17280  nninfsellemqall  17281  nninfsellemeqinf  17282  nninfsel  17283  nnnninfex  17288  exmidsbthr  17291  qdencn  17295  refeq  17296  repiecele0  17298  repiecege0  17299  repiecef  17300  isomninnlem  17302  apdifflemr  17320  apdiff  17321  qdiff  17322  ismkvnnlem  17326  nconstwlpolem  17339