Theorem fveq2d 5699

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

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

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 4131  df-iota 5337  df-fv 5385

This theorem is used by:  2fveq3  5700  fveq12d  5702  fveqeq2d  5703  csbfvg  5738  fvmptdf  5793  fvmptt  5797  resfvresima  5956  fcof1  5989  oveq1  6092  oveq2  6093  fvoveq1d  6107  caofinvl  6328  op1stg  6384  op2ndg  6385  ot1stg  6386  ot2ndg  6387  eloprabi  6432  1stconst  6457  algrflemg  6466  tfrlem1  6579  tfrlem3ag  6580  tfrlem3a  6581  tfrlem9  6590  tfr0dm  6593  tfrlemisucaccv  6596  tfrlemiubacc  6601  tfrlemiex  6602  tfrlemi1  6603  tfr1onlem3ag  6608  tfr1onlemsucaccv  6612  tfr1onlemubacc  6617  tfr1onlemex  6618  tfr1onlemaccex  6619  tfrcllemsucaccv  6625  tfrcllembxssdm  6627  tfrcllemubacc  6630  tfrcllemex  6631  tfrcllemaccex  6632  tfrcllemres  6633  tfrcldm  6634  rdgivallem  6652  rdgival  6653  rdgss  6654  rdgisuc1  6655  rdgon  6657  rdg0  6658  frec0g  6668  frecabcl  6670  freccllem  6673  frecfcllem  6675  frecsuclem  6677  frecsuc  6678  frecrdg  6679  oav2  6736  omv2  6738  xpdom2  7129  xpmapenlem  7149  xpmapen  7150  ac6sfi  7202  1stinl  7414  2ndinl  7415  1stinr  7416  2ndinr  7417  updjudhcoinlf  7420  updjudhcoinrg  7421  caseinl  7431  caseinr  7432  omp1eomlem  7434  omp1eom  7435  difinfsn  7440  ctmlemr  7448  ctm  7449  ctssdclemn0  7450  ctssdccl  7451  nninfninc  7463  nnnninfeq  7468  nnnninfeq2  7469  enomnilem  7478  enmkvlem  7501  enwomnilem  7509  exmidfodomrlemeldju  7551  exmidfodomrlemreseldju  7552  exmidfodomrlemr  7554  exmidfodomrlemrALT  7555  exmidaclem  7564  cc2  7633  cc3  7634  ltdfpr  7873  genpelvl  7879  genpelvu  7880  recexpr  8005  cauappcvgprlem1  8026  caucvgprlemnkj  8033  caucvgprlemnbj  8034  caucvgprlemm  8035  caucvgprlemdisj  8041  caucvgprlemloc  8042  caucvgprlemcl  8043  caucvgprlemladdfu  8044  caucvgprlemladdrl  8045  caucvgprlem1  8046  caucvgprlem2  8047  caucvgpr  8049  caucvgprprlemell  8052  caucvgprprlemelu  8053  caucvgprprlemcbv  8054  caucvgprprlemval  8055  caucvgprprlemnkeqj  8057  caucvgprprlemmu  8062  caucvgprprlemopl  8064  caucvgprprlemlol  8065  caucvgprprlemopu  8066  caucvgprprlemloc  8070  caucvgprprlemclphr  8072  caucvgprprlemexbt  8073  caucvgprprlem1  8076  caucvgprprlem2  8077  caucvgsr  8169  axcaucvglemval  8264  axcaucvglemres  8266  fv0p1e1  9421  uzin  9964  cnref1o  10061  fzsuc2  10496  fseq1m1p1  10512  fzoss2  10591  elfzonlteqm1  10638  divfl0  10744  flqzadd  10746  fldiv4p1lem1div2  10753  ceilqval  10756  flqdiv  10771  modqval  10774  modqfrac  10787  modqmulnn  10792  modqid  10799  modqcyc  10809  modqdi  10842  frec2uzuzd  10852  frec2uzrdg  10859  frecuzrdgrcl  10860  frecuzrdgtcl  10862  frecuzrdgsuc  10864  frecuzrdgrclt  10865  frecuzrdgg  10866  frecuzrdgfunlem  10869  frecuzrdgsuctlem  10873  iseqovex  10908  iseqvalcbv  10909  seq3val  10910  seqvalcd  10911  seq3m1  10923  seq3shft2  10931  seqshft2g  10932  monoord  10935  monoord2  10936  iseqf1olemqval  10950  iseqf1olemab  10952  iseqf1olemqk  10957  iseqf1olemjpcl  10958  iseqf1olemqpcl  10959  iseqf1olemfvp  10960  seq3f1olemqsumkj  10961  seq3f1olemqsumk  10962  seq3f1olemqsum  10963  seq3f1olemp  10965  seq3f1oleml  10966  seqf1oglem1  10969  seqf1oglem2  10970  seqf1og  10971  seq3homo  10977  seqhomog  10980  exp3val  10991  expnegap0  10997  facnn2  11186  facwordi  11192  faclbnd6  11196  bcval  11201  bccmpl  11206  bcn0  11207  bcm1k  11212  bcp1n  11213  bcn2  11216  hashinfom  11231  hashennn  11233  hashsng  11251  omgadd  11256  hashprg  11263  fihashssdif  11273  hashdifpr  11275  hashfzo  11277  hashfzp1  11279  hashxp  11281  hashmap  11282  hashfibclem  11296  hashfibc  11297  hashf1lem2  11300  hashf1  11301  hashfac  11302  zfz1isolemiso  11305  zfz1iso  11307  hashtpglem  11312  lsw1  11368  ccatfvalfi  11374  ccatlen  11377  ccatval3  11381  ccatval21sw  11387  ccatlid  11388  ccatass  11390  lswccatn0lsw  11393  lswccat0lsw  11394  ccatalpha  11395  s1leng  11406  ccats1val2  11422  lswccats1  11425  swrdfv0  11440  swrdfv2  11449  swrdsbslen  11452  swrds1  11454  ccatswrd  11456  pfxmpt  11466  pfxfv  11470  pfxtrcfvl  11483  ccatpfx  11487  swrdswrd  11491  lenpfxcctswrd  11497  ccatopth  11502  cats1un  11507  swrdccatin2  11515  pfxccatin12lem2  11517  shftval2  11605  shftval3  11606  shftval4  11607  shftval5  11608  seq3shft  11617  imval  11629  imre  11630  reim  11631  crim  11637  reim0  11640  mulreap  11643  recj  11646  reneg  11647  readd  11648  resub  11649  remullem  11650  redivap  11653  imcj  11654  imneg  11655  imadd  11656  imsub  11657  imdivap  11660  cjsub  11671  cjexp  11672  cjreim2  11684  cjap  11686  cjdivap  11689  cnrecnv  11690  cvg1nlemcau  11764  cvg1nlemres  11765  absval  11781  rennim  11782  sqrtdiv  11822  sqrtmsq  11825  absneg  11830  abscj  11832  absval2  11837  absreim  11848  absmul  11849  absdivap  11850  absid  11851  absre  11858  absexp  11860  absexpzap  11861  absimle  11865  abssub  11882  abs3dif  11886  abs2dif  11887  abs2dif2  11888  recan  11890  cau3lem  11895  max0addsup  12000  minabs  12017  bdtrilem  12021  clim  12063  clim2  12065  clim0  12067  clim0c  12068  climi0  12071  climconst  12072  climshftlemg  12084  climcn1  12090  climcn2  12091  addcn2  12092  subcn2  12093  mulcn2  12094  reccn2ap  12095  cjcn2  12098  recn2  12099  imcn2  12100  iser3shft  12128  climcau  12129  climcvg1nlem  12131  climcvg1n  12132  serf0  12134  fzf1o  12158  summodclem3  12163  summodclem2a  12164  summodc  12166  fsumf1o  12173  sumsnf  12192  fsumm1  12199  fsumcnv  12220  fsumabs  12248  fsumrelem  12254  iserabs  12258  hash2iun1dif1  12263  isumshft  12273  isumsplit  12274  expcnvap0  12285  expcnv  12287  cvgratnnlemseq  12309  cvgratnnlemrate  12313  cvgratz  12315  mertenslemub  12317  mertenslemi1  12318  mertenslem2  12319  mertensabs  12320  prodmodclem3  12358  fprodf1o  12371  prodsnf  12375  fprodm1  12381  fprodabs  12399  fprodcnv  12408  efcllemp  12441  efcj  12456  efaddlem  12457  efcan  12459  efsub  12464  efexp  12465  efzval  12466  efgt0  12467  eftlub  12473  efltim  12481  sinval  12485  cosval  12486  tanval3ap  12497  resinval  12498  recosval  12499  resin4p  12501  recos4p  12502  sinneg  12509  cosneg  12510  efmival  12516  efeul  12517  sinadd  12519  cosadd  12520  sinsub  12523  cossub  12524  addsin  12525  subsin  12526  addcos  12529  subcos  12530  sincossq  12531  sin2t  12532  cos2t  12533  sin01bnd  12540  cos01bnd  12541  sin02gt0  12547  cos12dec  12551  absefi  12552  absef  12553  absefib  12554  efieq1re  12555  demoivre  12556  demoivreALT  12557  flodddiv4  12719  bitsval  12726  bits0  12731  bitsp1  12734  bitsp1e  12735  bitsp1o  12736  bitsmod  12739  nninfctlemfo  12833  alginv  12841  algcvg  12842  eucalgval  12848  eucalginv  12850  eucalglt  12851  eucalgcvga  12852  eucalg  12853  lcmgcd  12872  lcm1  12875  sqpweven  12971  2sqpwodd  12972  sqne2sq  12973  qnumval  12981  qdenval  12982  qden1elz  13001  nn0sqrtelqelz  13002  nn0sqdcq  13004  sqrtrirr  13005  phival  13011  dfphi2  13018  phiprmpw  13020  phiprm  13021  eulerthlemth  13030  hashgcdeq  13038  phisum  13039  pythagtriplem6  13069  pythagtriplem7  13070  pythagtriplem12  13074  pythagtriplem14  13076  fldivp1  13147  4sqlem11  13200  prmlem0  13240  ballotfilemfval  13278  ballotfilemfp1  13280  ballotfilemfc0  13281  ballotfilemfcc  13282  ballotfilemfmpn  13283  ballotfilemsval  13301  ballotfilemgval  13316  ballotfilemgun  13317  ballotfilemfrc  13319  ballotfilemrinv0  13325  ennnfonelemg  13343  ennnfonelemp1  13346  ennnfonelemkh  13352  ennnfonelemhf1o  13353  ennnfonelemnn0  13362  ctinfomlemom  13367  ctiunctlemu1st  13374  ctiunctlemu2nd  13375  ctiunctlemudc  13377  ctiunctlemfo  13379  isstruct2im  13411  isstruct2r  13412  setsslid  13452  ressbasd  13470  resseqnbasd  13476  ressplusgd  13532  ptex  13667  imasex  13675  imasival  13676  f1ocpbl  13681  f1ovscpbl  13682  imasaddvallemg  13685  qusval  13693  fvprif  13713  xpsff1o  13719  gzsumvalx  13758  imasmnd  13809  ismhm  13817  mhmpropd  13822  mhmlin  13823  mhmf1o  13826  resmhm  13843  mhmco  13846  gzsumwmhm  13852  grpinvsub  13936  imasgrp2  13962  imasgrp  13963  mhmlem  13966  mhmid  13967  mhmmnd  13968  ghmgrp  13970  mulgfvalg  13973  mulgval  13974  mulgnegnn  13984  mulgneg  13992  mulgnegneg  13993  mulgm1  13994  mulginvcom  13999  mulgz  14002  mulgnndir  14003  mulgdir  14006  mulgass  14011  mhmmulg  14015  subgmulg  14040  isnsg  14054  eqgfval  14074  ghmlin  14100  ghmid  14101  ghminv  14102  ghmsub  14103  ghmmulg  14108  resghm  14112  ghmeql  14119  ablsub2inv  14164  ghmcmn  14180  invghm  14182  imasabl  14189  gzsumreidx  14190  gzsummhm  14194  gzsumsplit0  14197  gzsumshift  14198  gsumvalfi  14201  gsump1  14206  gsumf1ofi  14209  gsummhmfi  14213  prdsex  14221  prdsval  14222  prdsbas3  14236  pwsval  14253  pwsbas  14254  pwsplusgval  14257  pwsmulrval  14258  pws0g  14262  pwsinvg  14264  mgpplusgg  14270  mgpbasg  14273  mgpscag  14275  mgptsetg  14276  mgpdsg  14278  rngm2neg  14297  imasrng  14304  isring  14353  ringm2neg  14409  imasring  14418  opprmulfvalg  14424  opprsllem  14428  isunitd  14462  opprunitd  14466  invrfvald  14478  rdivmuldivd  14500  rhmmul  14520  isrhm2d  14521  rhm1  14523  rhmdvdsr  14531  rhmopp  14532  rhmunitinv  14534  islmod  14676  islmodd  14678  scaffvalg  14692  lmodpropd  14735  lsssetm  14742  islssmd  14745  lssats2  14800  lspsnneg  14806  lspsnsub  14807  lspun0  14811  lmodindp1  14814  sralemg  14824  srascag  14828  sravscag  14829  sraipg  14830  rlmscabas  14846  ixpsnbasval  14852  2idlval  14888  2idlvalg  14889  mulgrhm2  14994  zlmlemg  15012  zlmsca  15016  zlmvscag  15017  znval  15020  znle  15021  znbaslemnn  15023  znidomb  15042  isassad  15060  assapropd  15063  asclfval  15070  ressascl  15088  assamulgscmlem2  15091  psrval  15099  psrbasg  15114  psrplusgg  15118  mplvalcoe  15130  mplsubgfileminv  15140  mpl0fi  15142  mplnegfi  15145  istps  15182  tpspropd  15186  eltpsg  15190  txvalex  15404  txval  15405  txbasval  15417  upxp  15422  uptx  15424  txrest  15426  cnmpt11  15433  cnmpt21  15441  hmeontr  15463  txhmeo  15469  psmetxrge0  15482  xmetunirn  15508  mopnval  15592  mopntopon  15593  isxms  15601  isxms2  15602  isms  15603  msrtri  15626  xmspropd  15627  mspropd  15628  setsmsbasg  15629  setsmsdsg  15630  setsmstsetg  15631  comet  15649  metcnpi  15665  metcnpi2  15666  cnbl0  15684  cnblcld  15685  resubmet  15706  mpomulcn  15716  elcncf  15723  cncfi  15728  rescncf  15731  mulc1cncf  15739  cncfco  15741  cncfmptid  15747  addccncf  15750  cdivcncfap  15754  negcncf  15755  mulcncflem  15757  ivthinclemlopn  15786  ivthinclemuopn  15788  limccl  15809  ellimc3apf  15810  limcimolemlt  15814  cnplimclemle  15818  limccnpcntop  15825  reldvg  15829  dvfvalap  15831  dveflem  15876  dvef  15877  plymullem1  15898  plycjlemc  15910  plycj  15911  plyrecj  15913  plyreres  15914  sin0pilem1  15932  ef2kpi  15957  sinperlem  15959  sin2kpi  15962  cos2kpi  15963  sin2pim  15964  cos2pim  15965  ptolemy  15975  sincosq2sgn  15978  sincosq3sgn  15979  sincosq4sgn  15980  sinq12gt0  15981  tangtx  15989  sincosq1eq  15990  abssinper  15997  sinkpi  15998  coskpi  15999  cosq34lt1  16001  relogeftb  16016  relogoprlem  16020  relogexp  16024  logfac  16048  rpcxpef  16049  logcxp  16052  1cxp  16055  ecxp  16056  rpcxpadd  16060  rpmulcxp  16064  cxpmul  16067  abscxp  16070  logsqrt  16078  rpabscxpbnd  16095  rpcxplogb  16119  zprmlogbaplem3  16136  birthdaylem2  16145  birthdaylem3  16146  pellexlem1  16148  pellexlem2  16149  pellexlem3  16150  ppiqval  16160  ppival2  16161  ppival2g  16162  ppiprm  16170  ppinprm  16171  ppiqfl  16172  ppiqp1le  16173  ppidif  16175  ppiqltx  16183  bcctr  16200  bcmono  16202  bposlem2  16210  lgsval  16221  lgsval2lem  16227  lgsval4a  16239  lgsdi  16254  lgseisenlem3  16289  lgseisenlem4  16290  lgsquadlem1  16294  lgsquadlem2  16295  lgsquadlem3  16296  2lgslem1  16308  2lgslem3a  16310  2lgslem3b  16311  2lgslem3c  16312  2lgslem3d  16313  vtxdgfval  16627  vtxdgfifival  16630  vtxdgop  16631  vtxdgfi0e  16634  vtxdeqd  16635  vtxdfifiun  16636  vtxdumgrfival  16637  1hevtxdg1en  16647  iswlk  16662  2wlklem  16715  wlkres  16718  clwwlkccatlem  16739  clwwlkn2  16760  clwwlkext2edg  16761  umgr2cwwk2dif  16763  clwwlknonex2lem2  16777  eupth2fi  16818  eulerpathprum  16819  depindlem1  16845  depind  16848  nnsf  17146  peano4nninf  17147  peano3nninf  17148  nninfalllem1  17149  nninfall  17150  nninfsellemdc  17151  nninfsellemeq  17155  nninfsellemqall  17156  nninfsellemeqinf  17157  nninfsel  17158  nnnninfex  17163  exmidsbthr  17166  qdencn  17170  refeq  17171  repiecele0  17173  repiecege0  17174  repiecef  17175  isomninnlem  17177  apdifflemr  17194  apdiff  17195  qdiff  17196  ismkvnnlem  17200  nconstwlpolem  17213