Theorem fveq2d 5699

Description: Equality deduction for function value. (Contributed by NM, 29-May-1999.)

Hypothesis

Ref	Expression
fveq2d.1	|- ( ph -> A = B )

Assertion

Ref	Expression
fveq2d	|- ( ph -> ( F ` A ) = ( F ` B ) )

Proof of Theorem fveq2d

Step	Hyp	Ref	Expression
1		fveq2d.1	. 2 |- ( ph -> A = B )
2		fveq2 5695	. 2 |- ( A = B -> ( F ` A ) = ( F ` B ) )
3	1, 2	syl 14	1 |- ( ph -> ( F ` A ) = ( F ` B ) )

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  9419  uzin  9955  cnref1o  10051  fzsuc2  10486  fseq1m1p1  10502  fzoss2  10581  elfzonlteqm1  10628  divfl0  10731  flqzadd  10733  fldiv4p1lem1div2  10740  ceilqval  10743  flqdiv  10758  modqval  10761  modqfrac  10774  modqmulnn  10779  modqid  10786  modqcyc  10796  modqdi  10829  frec2uzuzd  10839  frec2uzrdg  10846  frecuzrdgrcl  10847  frecuzrdgtcl  10849  frecuzrdgsuc  10851  frecuzrdgrclt  10852  frecuzrdgg  10853  frecuzrdgfunlem  10856  frecuzrdgsuctlem  10860  iseqovex  10895  iseqvalcbv  10896  seq3val  10897  seqvalcd  10898  seq3m1  10910  seq3shft2  10918  seqshft2g  10919  monoord  10922  monoord2  10923  iseqf1olemqval  10937  iseqf1olemab  10939  iseqf1olemqk  10944  iseqf1olemjpcl  10945  iseqf1olemqpcl  10946  iseqf1olemfvp  10947  seq3f1olemqsumkj  10948  seq3f1olemqsumk  10949  seq3f1olemqsum  10950  seq3f1olemp  10952  seq3f1oleml  10953  seqf1oglem1  10956  seqf1oglem2  10957  seqf1og  10958  seq3homo  10964  seqhomog  10967  exp3val  10978  expnegap0  10984  facnn2  11172  facwordi  11178  faclbnd6  11182  bcval  11187  bccmpl  11192  bcn0  11193  bcm1k  11198  bcp1n  11199  bcn2  11202  hashinfom  11217  hashennn  11219  hashsng  11237  omgadd  11242  hashprg  11249  fihashssdif  11259  hashdifpr  11261  hashfzo  11263  hashfzp1  11265  hashxp  11267  hashmap  11268  hashfibclem  11282  hashfibc  11283  hashf1lem2  11286  hashf1  11287  hashfac  11288  zfz1isolemiso  11291  zfz1iso  11293  hashtpglem  11298  lsw1  11354  ccatfvalfi  11360  ccatlen  11363  ccatval3  11367  ccatval21sw  11373  ccatlid  11374  ccatass  11376  lswccatn0lsw  11379  lswccat0lsw  11380  ccatalpha  11381  s1leng  11392  ccats1val2  11408  lswccats1  11411  swrdfv0  11426  swrdfv2  11435  swrdsbslen  11438  swrds1  11440  ccatswrd  11442  pfxmpt  11452  pfxfv  11456  pfxtrcfvl  11469  ccatpfx  11473  swrdswrd  11477  lenpfxcctswrd  11483  ccatopth  11488  cats1un  11493  swrdccatin2  11501  pfxccatin12lem2  11503  shftval2  11591  shftval3  11592  shftval4  11593  shftval5  11594  seq3shft  11603  imval  11615  imre  11616  reim  11617  crim  11623  reim0  11626  mulreap  11629  recj  11632  reneg  11633  readd  11634  resub  11635  remullem  11636  redivap  11639  imcj  11640  imneg  11641  imadd  11642  imsub  11643  imdivap  11646  cjsub  11657  cjexp  11658  cjreim2  11670  cjap  11672  cjdivap  11675  cnrecnv  11676  cvg1nlemcau  11750  cvg1nlemres  11751  absval  11767  rennim  11768  sqrtdiv  11808  sqrtmsq  11811  absneg  11816  abscj  11818  absval2  11823  absreim  11834  absmul  11835  absdivap  11836  absid  11837  absre  11843  absexp  11845  absexpzap  11846  absimle  11850  abssub  11867  abs3dif  11871  abs2dif  11872  abs2dif2  11873  recan  11875  cau3lem  11880  max0addsup  11985  minabs  12002  bdtrilem  12005  clim  12047  clim2  12049  clim0  12051  clim0c  12052  climi0  12055  climconst  12056  climshftlemg  12068  climcn1  12074  climcn2  12075  addcn2  12076  subcn2  12077  mulcn2  12078  reccn2ap  12079  cjcn2  12082  recn2  12083  imcn2  12084  iser3shft  12112  climcau  12113  climcvg1nlem  12115  climcvg1n  12116  serf0  12118  fzf1o  12142  summodclem3  12147  summodclem2a  12148  summodc  12150  fsumf1o  12157  sumsnf  12176  fsumm1  12183  fsumcnv  12204  fsumabs  12232  fsumrelem  12238  iserabs  12242  hash2iun1dif1  12247  isumshft  12257  isumsplit  12258  expcnvap0  12269  expcnv  12271  cvgratnnlemseq  12293  cvgratnnlemrate  12297  cvgratz  12299  mertenslemub  12301  mertenslemi1  12302  mertenslem2  12303  mertensabs  12304  prodmodclem3  12342  fprodf1o  12355  prodsnf  12359  fprodm1  12365  fprodabs  12383  fprodcnv  12392  efcllemp  12425  efcj  12440  efaddlem  12441  efcan  12443  efsub  12448  efexp  12449  efzval  12450  efgt0  12451  eftlub  12457  efltim  12465  sinval  12469  cosval  12470  tanval3ap  12481  resinval  12482  recosval  12483  resin4p  12485  recos4p  12486  sinneg  12493  cosneg  12494  efmival  12500  efeul  12501  sinadd  12503  cosadd  12504  sinsub  12507  cossub  12508  addsin  12509  subsin  12510  addcos  12513  subcos  12514  sincossq  12515  sin2t  12516  cos2t  12517  sin01bnd  12524  cos01bnd  12525  sin02gt0  12531  cos12dec  12535  absefi  12536  absef  12537  absefib  12538  efieq1re  12539  demoivre  12540  demoivreALT  12541  flodddiv4  12703  bitsval  12710  bits0  12715  bitsp1  12718  bitsp1e  12719  bitsp1o  12720  bitsmod  12723  nninfctlemfo  12817  alginv  12825  algcvg  12826  eucalgval  12832  eucalginv  12834  eucalglt  12835  eucalgcvga  12836  eucalg  12837  lcmgcd  12856  lcm1  12859  sqpweven  12953  2sqpwodd  12954  sqne2sq  12955  qnumval  12963  qdenval  12964  qden1elz  12983  nn0sqrtelqelz  12984  phival  12991  dfphi2  12998  phiprmpw  13000  phiprm  13001  eulerthlemth  13010  hashgcdeq  13018  phisum  13019  pythagtriplem6  13049  pythagtriplem7  13050  pythagtriplem12  13054  pythagtriplem14  13056  fldivp1  13127  4sqlem11  13180  ballotfilemfval  13229  ballotfilemfp1  13231  ballotfilemfc0  13232  ballotfilemfcc  13233  ballotfilemfmpn  13234  ballotfilemsval  13252  ballotfilemgval  13267  ballotfilemgun  13268  ballotfilemfrc  13270  ballotfilemrinv0  13276  ennnfonelemg  13294  ennnfonelemp1  13297  ennnfonelemkh  13303  ennnfonelemhf1o  13304  ennnfonelemnn0  13313  ctinfomlemom  13318  ctiunctlemu1st  13325  ctiunctlemu2nd  13326  ctiunctlemudc  13328  ctiunctlemfo  13330  isstruct2im  13362  isstruct2r  13363  setsslid  13403  ressbasd  13421  resseqnbasd  13427  ressplusgd  13483  ptex  13618  imasex  13626  imasival  13627  f1ocpbl  13632  f1ovscpbl  13633  imasaddvallemg  13636  qusval  13644  fvprif  13664  xpsff1o  13670  gzsumvalx  13709  imasmnd  13760  ismhm  13768  mhmpropd  13773  mhmlin  13774  mhmf1o  13777  resmhm  13794  mhmco  13797  gzsumwmhm  13803  grpinvsub  13887  imasgrp2  13913  imasgrp  13914  mhmlem  13917  mhmid  13918  mhmmnd  13919  ghmgrp  13921  mulgfvalg  13924  mulgval  13925  mulgnegnn  13935  mulgneg  13943  mulgnegneg  13944  mulgm1  13945  mulginvcom  13950  mulgz  13953  mulgnndir  13954  mulgdir  13957  mulgass  13962  mhmmulg  13966  subgmulg  13991  isnsg  14005  eqgfval  14025  ghmlin  14051  ghmid  14052  ghminv  14053  ghmsub  14054  ghmmulg  14059  resghm  14063  ghmeql  14070  ablsub2inv  14115  ghmcmn  14131  invghm  14133  imasabl  14140  gzsumreidx  14141  gzsummhm  14145  gzsumsplit0  14148  gzsumshift  14149  gsumvalfi  14152  gsump1  14157  gsumf1ofi  14160  gsummhmfi  14164  prdsex  14172  prdsval  14173  prdsbas3  14187  pwsval  14204  pwsbas  14205  pwsplusgval  14208  pwsmulrval  14209  pws0g  14213  pwsinvg  14215  mgpplusgg  14221  mgpbasg  14224  mgpscag  14226  mgptsetg  14227  mgpdsg  14229  rngm2neg  14248  imasrng  14255  isring  14304  ringm2neg  14360  imasring  14369  opprmulfvalg  14375  opprsllem  14379  isunitd  14413  opprunitd  14417  invrfvald  14429  rdivmuldivd  14451  rhmmul  14471  isrhm2d  14472  rhm1  14474  rhmdvdsr  14482  rhmopp  14483  rhmunitinv  14485  islmod  14627  islmodd  14629  scaffvalg  14643  lmodpropd  14686  lsssetm  14693  islssmd  14696  lssats2  14751  lspsnneg  14757  lspsnsub  14758  lspun0  14762  lmodindp1  14765  sralemg  14775  srascag  14779  sravscag  14780  sraipg  14781  rlmscabas  14797  ixpsnbasval  14803  2idlval  14839  2idlvalg  14840  mulgrhm2  14945  zlmlemg  14963  zlmsca  14967  zlmvscag  14968  znval  14971  znle  14972  znbaslemnn  14974  znidomb  14993  isassad  15011  assapropd  15014  asclfval  15021  ressascl  15039  assamulgscmlem2  15042  psrval  15050  psrbasg  15065  psrplusgg  15069  mplvalcoe  15081  mplsubgfileminv  15091  mpl0fi  15093  mplnegfi  15096  istps  15133  tpspropd  15137  eltpsg  15141  txvalex  15355  txval  15356  txbasval  15368  upxp  15373  uptx  15375  txrest  15377  cnmpt11  15384  cnmpt21  15392  hmeontr  15414  txhmeo  15420  psmetxrge0  15433  xmetunirn  15459  mopnval  15543  mopntopon  15544  isxms  15552  isxms2  15553  isms  15554  msrtri  15577  xmspropd  15578  mspropd  15579  setsmsbasg  15580  setsmsdsg  15581  setsmstsetg  15582  comet  15600  metcnpi  15616  metcnpi2  15617  cnbl0  15635  cnblcld  15636  resubmet  15657  mpomulcn  15667  elcncf  15674  cncfi  15679  rescncf  15682  mulc1cncf  15690  cncfco  15692  cncfmptid  15698  addccncf  15701  cdivcncfap  15705  negcncf  15706  mulcncflem  15708  ivthinclemlopn  15737  ivthinclemuopn  15739  limccl  15760  ellimc3apf  15761  limcimolemlt  15765  cnplimclemle  15769  limccnpcntop  15776  reldvg  15780  dvfvalap  15782  dveflem  15827  dvef  15828  plymullem1  15849  plycjlemc  15861  plycj  15862  plyrecj  15864  plyreres  15865  sin0pilem1  15882  ef2kpi  15907  sinperlem  15909  sin2kpi  15912  cos2kpi  15913  sin2pim  15914  cos2pim  15915  ptolemy  15925  sincosq2sgn  15928  sincosq3sgn  15929  sincosq4sgn  15930  sinq12gt0  15931  tangtx  15939  sincosq1eq  15940  abssinper  15947  sinkpi  15948  coskpi  15949  cosq34lt1  15951  relogeftb  15966  relogoprlem  15969  relogexp  15973  logfac  15995  rpcxpef  15996  logcxp  15999  1cxp  16002  ecxp  16003  rpcxpadd  16007  rpmulcxp  16011  cxpmul  16014  abscxp  16017  logsqrt  16025  rpabscxpbnd  16042  rpcxplogb  16066  birthdaylem2  16088  birthdaylem3  16089  pellexlem1  16091  pellexlem2  16092  pellexlem3  16093  lgsval  16123  lgsval2lem  16129  lgsval4a  16141  lgsdi  16156  lgseisenlem3  16191  lgseisenlem4  16192  lgsquadlem1  16196  lgsquadlem2  16197  lgsquadlem3  16198  2lgslem1  16210  2lgslem3a  16212  2lgslem3b  16213  2lgslem3c  16214  2lgslem3d  16215  vtxdgfval  16529  vtxdgfifival  16532  vtxdgop  16533  vtxdgfi0e  16536  vtxdeqd  16537  vtxdfifiun  16538  vtxdumgrfival  16539  1hevtxdg1en  16549  iswlk  16564  2wlklem  16617  wlkres  16620  clwwlkccatlem  16641  clwwlkn2  16662  clwwlkext2edg  16663  umgr2cwwk2dif  16665  clwwlknonex2lem2  16679  eupth2fi  16720  eulerpathprum  16721  depindlem1  16747  depind  16750  nnsf  17048  peano4nninf  17049  peano3nninf  17050  nninfalllem1  17051  nninfall  17052  nninfsellemdc  17053  nninfsellemeq  17057  nninfsellemqall  17058  nninfsellemeqinf  17059  nninfsel  17060  nnnninfex  17065  exmidsbthr  17068  qdencn  17072  refeq  17073  repiecele0  17075  repiecege0  17076  repiecef  17077  isomninnlem  17079  apdifflemr  17096  apdiff  17097  qdiff  17098  ismkvnnlem  17102  nconstwlpolem  17115