Theorem fveq2d 5633

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

Syntax hints:   -> wi 4   = wceq 1395   ` cfv 5318

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 714  ax-5 1493  ax-7 1494  ax-gen 1495  ax-ie1 1539  ax-ie2 1540  ax-8 1550  ax-10 1551  ax-11 1552  ax-i12 1553  ax-bndl 1555  ax-4 1556  ax-17 1572  ax-i9 1576  ax-ial 1580  ax-i5r 1581  ax-ext 2211

This theorem depends on definitions:  df-bi 117  df-3an 1004  df-tru 1398  df-nf 1507  df-sb 1809  df-clab 2216  df-cleq 2222  df-clel 2225  df-nfc 2361  df-rex 2514  df-v 2801  df-un 3201  df-sn 3672  df-pr 3673  df-op 3675  df-uni 3889  df-br 4084  df-iota 5278  df-fv 5326

This theorem is referenced by:  2fveq3  5634  fveq12d  5636  fveqeq2d  5637  csbfvg  5671  fvmptdf  5724  fvmptt  5728  resfvresima  5880  fcof1  5913  oveq1  6014  oveq2  6015  fvoveq1d  6029  caofinvl  6250  op1stg  6302  op2ndg  6303  ot1stg  6304  ot2ndg  6305  eloprabi  6348  1stconst  6373  algrflemg  6382  tfrlem1  6460  tfrlem3ag  6461  tfrlem3a  6462  tfrlem9  6471  tfr0dm  6474  tfrlemisucaccv  6477  tfrlemiubacc  6482  tfrlemiex  6483  tfrlemi1  6484  tfr1onlem3ag  6489  tfr1onlemsucaccv  6493  tfr1onlemubacc  6498  tfr1onlemex  6499  tfr1onlemaccex  6500  tfrcllemsucaccv  6506  tfrcllembxssdm  6508  tfrcllemubacc  6511  tfrcllemex  6512  tfrcllemaccex  6513  tfrcllemres  6514  tfrcldm  6515  rdgivallem  6533  rdgival  6534  rdgss  6535  rdgisuc1  6536  rdgon  6538  rdg0  6539  frec0g  6549  frecabcl  6551  freccllem  6554  frecfcllem  6556  frecsuclem  6558  frecsuc  6559  frecrdg  6560  oav2  6617  omv2  6619  xpdom2  6998  xpmapenlem  7018  xpmapen  7019  ac6sfi  7068  1stinl  7252  2ndinl  7253  1stinr  7254  2ndinr  7255  updjudhcoinlf  7258  updjudhcoinrg  7259  caseinl  7269  caseinr  7270  omp1eomlem  7272  omp1eom  7273  difinfsn  7278  ctmlemr  7286  ctm  7287  ctssdclemn0  7288  ctssdccl  7289  nninfninc  7301  nnnninfeq  7306  nnnninfeq2  7307  enomnilem  7316  enmkvlem  7339  enwomnilem  7347  exmidfodomrlemeldju  7388  exmidfodomrlemreseldju  7389  exmidfodomrlemr  7391  exmidfodomrlemrALT  7392  exmidaclem  7401  cc2  7464  cc3  7465  ltdfpr  7704  genpelvl  7710  genpelvu  7711  recexpr  7836  cauappcvgprlem1  7857  caucvgprlemnkj  7864  caucvgprlemnbj  7865  caucvgprlemm  7866  caucvgprlemdisj  7872  caucvgprlemloc  7873  caucvgprlemcl  7874  caucvgprlemladdfu  7875  caucvgprlemladdrl  7876  caucvgprlem1  7877  caucvgprlem2  7878  caucvgpr  7880  caucvgprprlemell  7883  caucvgprprlemelu  7884  caucvgprprlemcbv  7885  caucvgprprlemval  7886  caucvgprprlemnkeqj  7888  caucvgprprlemmu  7893  caucvgprprlemopl  7895  caucvgprprlemlol  7896  caucvgprprlemopu  7897  caucvgprprlemloc  7901  caucvgprprlemclphr  7903  caucvgprprlemexbt  7904  caucvgprprlem1  7907  caucvgprprlem2  7908  caucvgsr  8000  axcaucvglemval  8095  axcaucvglemres  8097  fv0p1e1  9236  uzin  9767  cnref1o  9858  fzsuc2  10287  fseq1m1p1  10303  fzoss2  10382  elfzonlteqm1  10428  divfl0  10528  flqzadd  10530  fldiv4p1lem1div2  10537  ceilqval  10540  flqdiv  10555  modqval  10558  modqfrac  10571  modqmulnn  10576  modqid  10583  modqcyc  10593  modqdi  10626  frec2uzuzd  10636  frec2uzrdg  10643  frecuzrdgrcl  10644  frecuzrdgtcl  10646  frecuzrdgsuc  10648  frecuzrdgrclt  10649  frecuzrdgg  10650  frecuzrdgfunlem  10653  frecuzrdgsuctlem  10657  iseqovex  10692  iseqvalcbv  10693  seq3val  10694  seqvalcd  10695  seq3m1  10707  seq3shft2  10715  seqshft2g  10716  monoord  10719  monoord2  10720  iseqf1olemqval  10734  iseqf1olemab  10736  iseqf1olemqk  10741  iseqf1olemjpcl  10742  iseqf1olemqpcl  10743  iseqf1olemfvp  10744  seq3f1olemqsumkj  10745  seq3f1olemqsumk  10746  seq3f1olemqsum  10747  seq3f1olemp  10749  seq3f1oleml  10750  seqf1oglem1  10753  seqf1oglem2  10754  seqf1og  10755  seq3homo  10761  seqhomog  10764  exp3val  10775  expnegap0  10781  facnn2  10968  facwordi  10974  faclbnd6  10978  bcval  10983  bccmpl  10988  bcn0  10989  bcm1k  10994  bcp1n  10995  bcn2  10998  hashinfom  11012  hashennn  11014  hashsng  11032  omgadd  11036  hashprg  11043  fihashssdif  11053  hashdifpr  11055  hashfzo  11057  hashfzp1  11059  hashxp  11061  zfz1isolemiso  11074  zfz1iso  11076  lsw1  11134  ccatfvalfi  11140  ccatlen  11143  ccatval3  11147  ccatval21sw  11153  ccatlid  11154  ccatass  11156  lswccatn0lsw  11159  lswccat0lsw  11160  ccatalpha  11161  s1leng  11172  ccats1val2  11187  lswccats1  11190  swrdfv0  11202  swrdfv2  11211  swrdsbslen  11214  swrds1  11216  ccatswrd  11218  pfxmpt  11228  pfxfv  11232  pfxtrcfvl  11245  ccatpfx  11249  swrdswrd  11253  lenpfxcctswrd  11259  ccatopth  11264  cats1un  11269  swrdccatin2  11277  pfxccatin12lem2  11279  shftval2  11353  shftval3  11354  shftval4  11355  shftval5  11356  seq3shft  11365  imval  11377  imre  11378  reim  11379  crim  11385  reim0  11388  mulreap  11391  recj  11394  reneg  11395  readd  11396  resub  11397  remullem  11398  redivap  11401  imcj  11402  imneg  11403  imadd  11404  imsub  11405  imdivap  11408  cjsub  11419  cjexp  11420  cjreim2  11431  cjap  11433  cjdivap  11436  cnrecnv  11437  cvg1nlemcau  11511  cvg1nlemres  11512  absval  11528  rennim  11529  sqrtdiv  11569  sqrtmsq  11572  absneg  11577  abscj  11579  absval2  11584  absreim  11595  absmul  11596  absdivap  11597  absid  11598  absre  11604  absexp  11606  absexpzap  11607  absimle  11611  abssub  11628  abs3dif  11632  abs2dif  11633  abs2dif2  11634  recan  11636  cau3lem  11641  max0addsup  11746  minabs  11763  bdtrilem  11766  clim  11808  clim2  11810  clim0  11812  clim0c  11813  climi0  11816  climconst  11817  climshftlemg  11829  climcn1  11835  climcn2  11836  addcn2  11837  subcn2  11838  mulcn2  11839  reccn2ap  11840  cjcn2  11843  recn2  11844  imcn2  11845  iser3shft  11873  climcau  11874  climcvg1nlem  11876  climcvg1n  11877  serf0  11879  summodclem3  11907  summodclem2a  11908  summodc  11910  fsumf1o  11917  sumsnf  11936  fsumm1  11943  fsumcnv  11964  fsumabs  11992  fsumrelem  11998  iserabs  12002  hash2iun1dif1  12007  isumshft  12017  isumsplit  12018  expcnvap0  12029  expcnv  12031  cvgratnnlemseq  12053  cvgratnnlemrate  12057  cvgratz  12059  mertenslemub  12061  mertenslemi1  12062  mertenslem2  12063  mertensabs  12064  prodmodclem3  12102  fprodf1o  12115  prodsnf  12119  fprodm1  12125  fprodabs  12143  fprodcnv  12152  efcllemp  12185  efcj  12200  efaddlem  12201  efcan  12203  efsub  12208  efexp  12209  efzval  12210  efgt0  12211  eftlub  12217  efltim  12225  sinval  12229  cosval  12230  tanval3ap  12241  resinval  12242  recosval  12243  resin4p  12245  recos4p  12246  sinneg  12253  cosneg  12254  efmival  12260  efeul  12261  sinadd  12263  cosadd  12264  sinsub  12267  cossub  12268  addsin  12269  subsin  12270  addcos  12273  subcos  12274  sincossq  12275  sin2t  12276  cos2t  12277  sin01bnd  12284  cos01bnd  12285  sin02gt0  12291  cos12dec  12295  absefi  12296  absef  12297  absefib  12298  efieq1re  12299  demoivre  12300  demoivreALT  12301  flodddiv4  12463  bitsval  12470  bits0  12475  bitsp1  12478  bitsp1e  12479  bitsp1o  12480  bitsmod  12483  nninfctlemfo  12577  alginv  12585  algcvg  12586  eucalgval  12592  eucalginv  12594  eucalglt  12595  eucalgcvga  12596  eucalg  12597  lcmgcd  12616  lcm1  12619  sqpweven  12713  2sqpwodd  12714  sqne2sq  12715  qnumval  12723  qdenval  12724  qden1elz  12743  nn0sqrtelqelz  12744  phival  12751  dfphi2  12758  phiprmpw  12760  phiprm  12761  eulerthlemth  12770  hashgcdeq  12778  phisum  12779  pythagtriplem6  12809  pythagtriplem7  12810  pythagtriplem12  12814  pythagtriplem14  12816  fldivp1  12887  4sqlem11  12940  ennnfonelemg  12990  ennnfonelemp1  12993  ennnfonelemkh  12999  ennnfonelemhf1o  13000  ennnfonelemnn0  13009  ctinfomlemom  13014  ctiunctlemu1st  13021  ctiunctlemu2nd  13022  ctiunctlemudc  13024  ctiunctlemfo  13026  isstruct2im  13058  isstruct2r  13059  setsslid  13099  ressbasd  13116  resseqnbasd  13122  ressplusgd  13178  ptex  13313  prdsex  13318  prdsval  13322  prdsbas3  13336  pwsval  13340  pwsbas  13341  pwsplusgval  13344  pwsmulrval  13345  imasex  13354  imasival  13355  f1ocpbl  13360  f1ovscpbl  13361  imasaddvallemg  13364  qusval  13372  fvprif  13392  xpsff1o  13398  igsumvalx  13438  gsumprval  13448  pws0g  13500  imasmnd  13502  ismhm  13510  mhmpropd  13515  mhmlin  13516  mhmf1o  13519  resmhm  13536  mhmco  13539  gsumwmhm  13547  grpinvsub  13631  pwsinvg  13661  imasgrp2  13663  imasgrp  13664  mhmlem  13667  mhmid  13668  mhmmnd  13669  ghmgrp  13671  mulgfvalg  13674  mulgval  13675  mulgnegnn  13685  mulgneg  13693  mulgnegneg  13694  mulgm1  13695  mulginvcom  13700  mulgz  13703  mulgnndir  13704  mulgdir  13707  mulgass  13712  mhmmulg  13716  subgmulg  13741  isnsg  13755  eqgfval  13775  ghmlin  13801  ghmid  13802  ghminv  13803  ghmsub  13804  ghmmulg  13809  resghm  13813  ghmeql  13820  ablsub2inv  13864  ghmcmn  13880  invghm  13882  imasabl  13889  gsumfzreidx  13890  gsumfzmhm  13896  mgpplusgg  13903  mgpbasg  13905  mgpscag  13906  mgptsetg  13907  mgpdsg  13909  rngm2neg  13928  imasrng  13935  isring  13979  ringm2neg  14034  imasring  14043  opprmulfvalg  14049  opprsllem  14053  isunitd  14086  opprunitd  14090  invrfvald  14102  rdivmuldivd  14124  rhmmul  14144  isrhm2d  14145  rhm1  14147  rhmdvdsr  14155  rhmopp  14156  rhmunitinv  14158  islmod  14271  islmodd  14273  scaffvalg  14286  lmodpropd  14329  lsssetm  14336  islssmd  14339  lssats2  14394  lspsnneg  14400  lspsnsub  14401  lspun0  14405  lmodindp1  14408  sralemg  14418  srascag  14422  sravscag  14423  sraipg  14424  rlmscabas  14440  ixpsnbasval  14446  2idlval  14482  2idlvalg  14483  mulgrhm2  14590  zlmlemg  14608  zlmsca  14612  zlmvscag  14613  znval  14616  znle  14617  znbaslemnn  14619  znidomb  14638  psrval  14646  psrbasg  14654  psrplusgg  14658  mplvalcoe  14670  mplsubgfileminv  14680  mpl0fi  14682  mplnegfi  14685  istps  14722  tpspropd  14726  eltpsg  14730  txvalex  14944  txval  14945  txbasval  14957  upxp  14962  uptx  14964  txrest  14966  cnmpt11  14973  cnmpt21  14981  hmeontr  15003  txhmeo  15009  psmetxrge0  15022  xmetunirn  15048  mopnval  15132  mopntopon  15133  isxms  15141  isxms2  15142  isms  15143  msrtri  15166  xmspropd  15167  mspropd  15168  setsmsbasg  15169  setsmsdsg  15170  setsmstsetg  15171  comet  15189  metcnpi  15205  metcnpi2  15206  cnbl0  15224  cnblcld  15225  resubmet  15246  mpomulcn  15256  elcncf  15263  cncfi  15268  rescncf  15271  mulc1cncf  15279  cncfco  15281  cncfmptid  15287  addccncf  15290  cdivcncfap  15294  negcncf  15295  mulcncflem  15297  ivthinclemlopn  15326  ivthinclemuopn  15328  limccl  15349  ellimc3apf  15350  limcimolemlt  15354  cnplimclemle  15358  limccnpcntop  15365  reldvg  15369  dvfvalap  15371  dveflem  15416  dvef  15417  plymullem1  15438  plycjlemc  15450  plycj  15451  plyrecj  15453  plyreres  15454  sin0pilem1  15471  ef2kpi  15496  sinperlem  15498  sin2kpi  15501  cos2kpi  15502  sin2pim  15503  cos2pim  15504  ptolemy  15514  sincosq2sgn  15517  sincosq3sgn  15518  sincosq4sgn  15519  sinq12gt0  15520  tangtx  15528  sincosq1eq  15529  abssinper  15536  sinkpi  15537  coskpi  15538  cosq34lt1  15540  relogeftb  15555  relogoprlem  15558  relogexp  15562  rpcxpef  15584  logcxp  15587  1cxp  15590  ecxp  15591  rpcxpadd  15595  rpmulcxp  15599  cxpmul  15602  abscxp  15605  logsqrt  15613  rpabscxpbnd  15630  rpcxplogb  15654  lgsval  15699  lgsval2lem  15705  lgsval4a  15717  lgsdi  15732  lgseisenlem3  15767  lgseisenlem4  15768  lgsquadlem1  15772  lgsquadlem2  15773  lgsquadlem3  15774  2lgslem1  15786  2lgslem3a  15788  2lgslem3b  15789  2lgslem3c  15790  2lgslem3d  15791  vtxdgfval  16048  vtxdgfifival  16051  vtxdgop  16052  vtxdgfi0e  16055  vtxdeqd  16056  vtxdfifiun  16057  vtxdumgrfival  16058  iswlk  16069  2wlklem  16120  wlkres  16123  clwwlkccatlem  16143  clwwlkn2  16163  clwwlkext2edg  16164  umgr2cwwk2dif  16166  nnsf  16459  peano4nninf  16460  peano3nninf  16461  nninfalllem1  16462  nninfall  16463  nninfsellemdc  16464  nninfsellemeq  16468  nninfsellemqall  16469  nninfsellemeqinf  16470  nninfsel  16471  nnnninfex  16476  exmidsbthr  16479  qdencn  16483  refeq  16484  isomninnlem  16486  apdifflemr  16503  apdiff  16504  ismkvnnlem  16508  nconstwlpolem  16521