Theorem fveq2d 5676

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 5672	. 2 |- ( A = B -> ( F ` A ) = ( F ` B ) )
3	1, 2	syl 14	1 |- ( ph -> ( F ` A ) = ( F ` B ) )

Syntax hints:   -> wi 4   = wceq 1398   ` cfv 5354

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 3217  df-sn 3697  df-pr 3698  df-op 3700  df-uni 3917  df-br 4112  df-iota 5314  df-fv 5362

This theorem is referenced by:  2fveq3  5677  fveq12d  5679  fveqeq2d  5680  csbfvg  5714  fvmptdf  5767  fvmptt  5771  resfvresima  5925  fcof1  5958  oveq1  6059  oveq2  6060  fvoveq1d  6074  caofinvl  6294  op1stg  6346  op2ndg  6347  ot1stg  6348  ot2ndg  6349  eloprabi  6394  1stconst  6419  algrflemg  6428  tfrlem1  6541  tfrlem3ag  6542  tfrlem3a  6543  tfrlem9  6552  tfr0dm  6555  tfrlemisucaccv  6558  tfrlemiubacc  6563  tfrlemiex  6564  tfrlemi1  6565  tfr1onlem3ag  6570  tfr1onlemsucaccv  6574  tfr1onlemubacc  6579  tfr1onlemex  6580  tfr1onlemaccex  6581  tfrcllemsucaccv  6587  tfrcllembxssdm  6589  tfrcllemubacc  6592  tfrcllemex  6593  tfrcllemaccex  6594  tfrcllemres  6595  tfrcldm  6596  rdgivallem  6614  rdgival  6615  rdgss  6616  rdgisuc1  6617  rdgon  6619  rdg0  6620  frec0g  6630  frecabcl  6632  freccllem  6635  frecfcllem  6637  frecsuclem  6639  frecsuc  6640  frecrdg  6641  oav2  6698  omv2  6700  xpdom2  7084  xpmapenlem  7104  xpmapen  7105  ac6sfi  7157  1stinl  7367  2ndinl  7368  1stinr  7369  2ndinr  7370  updjudhcoinlf  7373  updjudhcoinrg  7374  caseinl  7384  caseinr  7385  omp1eomlem  7387  omp1eom  7388  difinfsn  7393  ctmlemr  7401  ctm  7402  ctssdclemn0  7403  ctssdccl  7404  nninfninc  7416  nnnninfeq  7421  nnnninfeq2  7422  enomnilem  7431  enmkvlem  7454  enwomnilem  7462  exmidfodomrlemeldju  7504  exmidfodomrlemreseldju  7505  exmidfodomrlemr  7507  exmidfodomrlemrALT  7508  exmidaclem  7517  cc2  7583  cc3  7584  ltdfpr  7823  genpelvl  7829  genpelvu  7830  recexpr  7955  cauappcvgprlem1  7976  caucvgprlemnkj  7983  caucvgprlemnbj  7984  caucvgprlemm  7985  caucvgprlemdisj  7991  caucvgprlemloc  7992  caucvgprlemcl  7993  caucvgprlemladdfu  7994  caucvgprlemladdrl  7995  caucvgprlem1  7996  caucvgprlem2  7997  caucvgpr  7999  caucvgprprlemell  8002  caucvgprprlemelu  8003  caucvgprprlemcbv  8004  caucvgprprlemval  8005  caucvgprprlemnkeqj  8007  caucvgprprlemmu  8012  caucvgprprlemopl  8014  caucvgprprlemlol  8015  caucvgprprlemopu  8016  caucvgprprlemloc  8020  caucvgprprlemclphr  8022  caucvgprprlemexbt  8023  caucvgprprlem1  8026  caucvgprprlem2  8027  caucvgsr  8119  axcaucvglemval  8214  axcaucvglemres  8216  fv0p1e1  9354  uzin  9890  cnref1o  9986  fzsuc2  10417  fseq1m1p1  10433  fzoss2  10512  elfzonlteqm1  10559  divfl0  10660  flqzadd  10662  fldiv4p1lem1div2  10669  ceilqval  10672  flqdiv  10687  modqval  10690  modqfrac  10703  modqmulnn  10708  modqid  10715  modqcyc  10725  modqdi  10758  frec2uzuzd  10768  frec2uzrdg  10775  frecuzrdgrcl  10776  frecuzrdgtcl  10778  frecuzrdgsuc  10780  frecuzrdgrclt  10781  frecuzrdgg  10782  frecuzrdgfunlem  10785  frecuzrdgsuctlem  10789  iseqovex  10824  iseqvalcbv  10825  seq3val  10826  seqvalcd  10827  seq3m1  10839  seq3shft2  10847  seqshft2g  10848  monoord  10851  monoord2  10852  iseqf1olemqval  10866  iseqf1olemab  10868  iseqf1olemqk  10873  iseqf1olemjpcl  10874  iseqf1olemqpcl  10875  iseqf1olemfvp  10876  seq3f1olemqsumkj  10877  seq3f1olemqsumk  10878  seq3f1olemqsum  10879  seq3f1olemp  10881  seq3f1oleml  10882  seqf1oglem1  10885  seqf1oglem2  10886  seqf1og  10887  seq3homo  10893  seqhomog  10896  exp3val  10907  expnegap0  10913  facnn2  11100  facwordi  11106  faclbnd6  11110  bcval  11115  bccmpl  11120  bcn0  11121  bcm1k  11126  bcp1n  11127  bcn2  11130  hashinfom  11145  hashennn  11147  hashsng  11165  omgadd  11170  hashprg  11177  fihashssdif  11187  hashdifpr  11189  hashfzo  11191  hashfzp1  11193  hashxp  11195  hashmap  11196  hashfibclem  11210  hashfibc  11211  zfz1isolemiso  11215  zfz1iso  11217  hashtpglem  11222  lsw1  11278  ccatfvalfi  11284  ccatlen  11287  ccatval3  11291  ccatval21sw  11297  ccatlid  11298  ccatass  11300  lswccatn0lsw  11303  lswccat0lsw  11304  ccatalpha  11305  s1leng  11316  ccats1val2  11332  lswccats1  11335  swrdfv0  11350  swrdfv2  11359  swrdsbslen  11362  swrds1  11364  ccatswrd  11366  pfxmpt  11376  pfxfv  11380  pfxtrcfvl  11393  ccatpfx  11397  swrdswrd  11401  lenpfxcctswrd  11407  ccatopth  11412  cats1un  11417  swrdccatin2  11425  pfxccatin12lem2  11427  shftval2  11515  shftval3  11516  shftval4  11517  shftval5  11518  seq3shft  11527  imval  11539  imre  11540  reim  11541  crim  11547  reim0  11550  mulreap  11553  recj  11556  reneg  11557  readd  11558  resub  11559  remullem  11560  redivap  11563  imcj  11564  imneg  11565  imadd  11566  imsub  11567  imdivap  11570  cjsub  11581  cjexp  11582  cjreim2  11593  cjap  11595  cjdivap  11598  cnrecnv  11599  cvg1nlemcau  11673  cvg1nlemres  11674  absval  11690  rennim  11691  sqrtdiv  11731  sqrtmsq  11734  absneg  11739  abscj  11741  absval2  11746  absreim  11757  absmul  11758  absdivap  11759  absid  11760  absre  11766  absexp  11768  absexpzap  11769  absimle  11773  abssub  11790  abs3dif  11794  abs2dif  11795  abs2dif2  11796  recan  11798  cau3lem  11803  max0addsup  11908  minabs  11925  bdtrilem  11928  clim  11970  clim2  11972  clim0  11974  clim0c  11975  climi0  11978  climconst  11979  climshftlemg  11991  climcn1  11997  climcn2  11998  addcn2  11999  subcn2  12000  mulcn2  12001  reccn2ap  12002  cjcn2  12005  recn2  12006  imcn2  12007  iser3shft  12035  climcau  12036  climcvg1nlem  12038  climcvg1n  12039  serf0  12041  fzf1o  12065  summodclem3  12070  summodclem2a  12071  summodc  12073  fsumf1o  12080  sumsnf  12099  fsumm1  12106  fsumcnv  12127  fsumabs  12155  fsumrelem  12161  iserabs  12165  hash2iun1dif1  12170  isumshft  12180  isumsplit  12181  expcnvap0  12192  expcnv  12194  cvgratnnlemseq  12216  cvgratnnlemrate  12220  cvgratz  12222  mertenslemub  12224  mertenslemi1  12225  mertenslem2  12226  mertensabs  12227  prodmodclem3  12265  fprodf1o  12278  prodsnf  12282  fprodm1  12288  fprodabs  12306  fprodcnv  12315  efcllemp  12348  efcj  12363  efaddlem  12364  efcan  12366  efsub  12371  efexp  12372  efzval  12373  efgt0  12374  eftlub  12380  efltim  12388  sinval  12392  cosval  12393  tanval3ap  12404  resinval  12405  recosval  12406  resin4p  12408  recos4p  12409  sinneg  12416  cosneg  12417  efmival  12423  efeul  12424  sinadd  12426  cosadd  12427  sinsub  12430  cossub  12431  addsin  12432  subsin  12433  addcos  12436  subcos  12437  sincossq  12438  sin2t  12439  cos2t  12440  sin01bnd  12447  cos01bnd  12448  sin02gt0  12454  cos12dec  12458  absefi  12459  absef  12460  absefib  12461  efieq1re  12462  demoivre  12463  demoivreALT  12464  flodddiv4  12626  bitsval  12633  bits0  12638  bitsp1  12641  bitsp1e  12642  bitsp1o  12643  bitsmod  12646  nninfctlemfo  12740  alginv  12748  algcvg  12749  eucalgval  12755  eucalginv  12757  eucalglt  12758  eucalgcvga  12759  eucalg  12760  lcmgcd  12779  lcm1  12782  sqpweven  12876  2sqpwodd  12877  sqne2sq  12878  qnumval  12886  qdenval  12887  qden1elz  12906  nn0sqrtelqelz  12907  phival  12914  dfphi2  12921  phiprmpw  12923  phiprm  12924  eulerthlemth  12933  hashgcdeq  12941  phisum  12942  pythagtriplem6  12972  pythagtriplem7  12973  pythagtriplem12  12977  pythagtriplem14  12979  fldivp1  13050  4sqlem11  13103  ballotfilemfval  13150  ballotfilemfp1  13152  ballotfilemfc0  13153  ballotfilemfcc  13154  ballotfilemfmpn  13155  ennnfonelemg  13171  ennnfonelemp1  13174  ennnfonelemkh  13180  ennnfonelemhf1o  13181  ennnfonelemnn0  13190  ctinfomlemom  13195  ctiunctlemu1st  13202  ctiunctlemu2nd  13203  ctiunctlemudc  13205  ctiunctlemfo  13207  isstruct2im  13239  isstruct2r  13240  setsslid  13280  ressbasd  13297  resseqnbasd  13303  ressplusgd  13359  ptex  13494  prdsex  13499  prdsval  13503  prdsbas3  13517  pwsval  13521  pwsbas  13522  pwsplusgval  13525  pwsmulrval  13526  imasex  13535  imasival  13536  f1ocpbl  13541  f1ovscpbl  13542  imasaddvallemg  13545  qusval  13553  fvprif  13573  xpsff1o  13579  igsumvalx  13619  gsumprval  13629  pws0g  13681  imasmnd  13683  ismhm  13691  mhmpropd  13696  mhmlin  13697  mhmf1o  13700  resmhm  13717  mhmco  13720  gsumwmhm  13728  grpinvsub  13812  pwsinvg  13842  imasgrp2  13844  imasgrp  13845  mhmlem  13848  mhmid  13849  mhmmnd  13850  ghmgrp  13852  mulgfvalg  13855  mulgval  13856  mulgnegnn  13866  mulgneg  13874  mulgnegneg  13875  mulgm1  13876  mulginvcom  13881  mulgz  13884  mulgnndir  13885  mulgdir  13888  mulgass  13893  mhmmulg  13897  subgmulg  13922  isnsg  13936  eqgfval  13956  ghmlin  13982  ghmid  13983  ghminv  13984  ghmsub  13985  ghmmulg  13990  resghm  13994  ghmeql  14001  ablsub2inv  14045  ghmcmn  14061  invghm  14063  imasabl  14070  gsumfzreidx  14071  gsumfzmhm  14077  gsumsplit0  14080  mgpplusgg  14085  mgpbasg  14087  mgpscag  14088  mgptsetg  14089  mgpdsg  14091  rngm2neg  14110  imasrng  14117  isring  14161  ringm2neg  14216  imasring  14225  opprmulfvalg  14231  opprsllem  14235  isunitd  14268  opprunitd  14272  invrfvald  14284  rdivmuldivd  14306  rhmmul  14326  isrhm2d  14327  rhm1  14329  rhmdvdsr  14337  rhmopp  14338  rhmunitinv  14340  islmod  14456  islmodd  14458  scaffvalg  14471  lmodpropd  14514  lsssetm  14521  islssmd  14524  lssats2  14579  lspsnneg  14585  lspsnsub  14586  lspun0  14590  lmodindp1  14593  sralemg  14603  srascag  14607  sravscag  14608  sraipg  14609  rlmscabas  14625  ixpsnbasval  14631  2idlval  14667  2idlvalg  14668  mulgrhm2  14775  zlmlemg  14793  zlmsca  14797  zlmvscag  14798  znval  14801  znle  14802  znbaslemnn  14804  znidomb  14823  psrval  14831  psrbasg  14846  psrplusgg  14850  mplvalcoe  14862  mplsubgfileminv  14872  mpl0fi  14874  mplnegfi  14877  istps  14914  tpspropd  14918  eltpsg  14922  txvalex  15136  txval  15137  txbasval  15149  upxp  15154  uptx  15156  txrest  15158  cnmpt11  15165  cnmpt21  15173  hmeontr  15195  txhmeo  15201  psmetxrge0  15214  xmetunirn  15240  mopnval  15324  mopntopon  15325  isxms  15333  isxms2  15334  isms  15335  msrtri  15358  xmspropd  15359  mspropd  15360  setsmsbasg  15361  setsmsdsg  15362  setsmstsetg  15363  comet  15381  metcnpi  15397  metcnpi2  15398  cnbl0  15416  cnblcld  15417  resubmet  15438  mpomulcn  15448  elcncf  15455  cncfi  15460  rescncf  15463  mulc1cncf  15471  cncfco  15473  cncfmptid  15479  addccncf  15482  cdivcncfap  15486  negcncf  15487  mulcncflem  15489  ivthinclemlopn  15518  ivthinclemuopn  15520  limccl  15541  ellimc3apf  15542  limcimolemlt  15546  cnplimclemle  15550  limccnpcntop  15557  reldvg  15561  dvfvalap  15563  dveflem  15608  dvef  15609  plymullem1  15630  plycjlemc  15642  plycj  15643  plyrecj  15645  plyreres  15646  sin0pilem1  15663  ef2kpi  15688  sinperlem  15690  sin2kpi  15693  cos2kpi  15694  sin2pim  15695  cos2pim  15696  ptolemy  15706  sincosq2sgn  15709  sincosq3sgn  15710  sincosq4sgn  15711  sinq12gt0  15712  tangtx  15720  sincosq1eq  15721  abssinper  15728  sinkpi  15729  coskpi  15730  cosq34lt1  15732  relogeftb  15747  relogoprlem  15750  relogexp  15754  rpcxpef  15776  logcxp  15779  1cxp  15782  ecxp  15783  rpcxpadd  15787  rpmulcxp  15791  cxpmul  15794  abscxp  15797  logsqrt  15805  rpabscxpbnd  15822  rpcxplogb  15846  pellexlem1  15862  pellexlem2  15863  pellexlem3  15864  lgsval  15894  lgsval2lem  15900  lgsval4a  15912  lgsdi  15927  lgseisenlem3  15962  lgseisenlem4  15963  lgsquadlem1  15967  lgsquadlem2  15968  lgsquadlem3  15969  2lgslem1  15981  2lgslem3a  15983  2lgslem3b  15984  2lgslem3c  15985  2lgslem3d  15986  vtxdgfval  16300  vtxdgfifival  16303  vtxdgop  16304  vtxdgfi0e  16307  vtxdeqd  16308  vtxdfifiun  16309  vtxdumgrfival  16310  1hevtxdg1en  16320  iswlk  16335  2wlklem  16388  wlkres  16391  clwwlkccatlem  16412  clwwlkn2  16433  clwwlkext2edg  16434  umgr2cwwk2dif  16436  clwwlknonex2lem2  16450  eupth2fi  16491  eulerpathprum  16492  depindlem1  16518  depind  16521  nnsf  16800  peano4nninf  16801  peano3nninf  16802  nninfalllem1  16803  nninfall  16804  nninfsellemdc  16805  nninfsellemeq  16809  nninfsellemqall  16810  nninfsellemeqinf  16811  nninfsel  16812  nnnninfex  16817  exmidsbthr  16820  qdencn  16824  refeq  16825  repiecele0  16827  repiecege0  16828  repiecef  16829  isomninnlem  16831  apdifflemr  16848  apdiff  16849  qdiff  16850  ismkvnnlem  16854  nconstwlpolem  16868  gfsumval  16879  gsumgfsumlem  16882  gfsump1  16885