Theorem fveq2d 5636

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 5632	. 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 5321

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 5281  df-fv 5329

This theorem is referenced by:  2fveq3  5637  fveq12d  5639  fveqeq2d  5640  csbfvg  5674  fvmptdf  5727  fvmptt  5731  resfvresima  5883  fcof1  5916  oveq1  6017  oveq2  6018  fvoveq1d  6032  caofinvl  6253  op1stg  6305  op2ndg  6306  ot1stg  6307  ot2ndg  6308  eloprabi  6353  1stconst  6378  algrflemg  6387  tfrlem1  6465  tfrlem3ag  6466  tfrlem3a  6467  tfrlem9  6476  tfr0dm  6479  tfrlemisucaccv  6482  tfrlemiubacc  6487  tfrlemiex  6488  tfrlemi1  6489  tfr1onlem3ag  6494  tfr1onlemsucaccv  6498  tfr1onlemubacc  6503  tfr1onlemex  6504  tfr1onlemaccex  6505  tfrcllemsucaccv  6511  tfrcllembxssdm  6513  tfrcllemubacc  6516  tfrcllemex  6517  tfrcllemaccex  6518  tfrcllemres  6519  tfrcldm  6520  rdgivallem  6538  rdgival  6539  rdgss  6540  rdgisuc1  6541  rdgon  6543  rdg0  6544  frec0g  6554  frecabcl  6556  freccllem  6559  frecfcllem  6561  frecsuclem  6563  frecsuc  6564  frecrdg  6565  oav2  6622  omv2  6624  xpdom2  7003  xpmapenlem  7023  xpmapen  7024  ac6sfi  7073  1stinl  7257  2ndinl  7258  1stinr  7259  2ndinr  7260  updjudhcoinlf  7263  updjudhcoinrg  7264  caseinl  7274  caseinr  7275  omp1eomlem  7277  omp1eom  7278  difinfsn  7283  ctmlemr  7291  ctm  7292  ctssdclemn0  7293  ctssdccl  7294  nninfninc  7306  nnnninfeq  7311  nnnninfeq2  7312  enomnilem  7321  enmkvlem  7344  enwomnilem  7352  exmidfodomrlemeldju  7393  exmidfodomrlemreseldju  7394  exmidfodomrlemr  7396  exmidfodomrlemrALT  7397  exmidaclem  7406  cc2  7469  cc3  7470  ltdfpr  7709  genpelvl  7715  genpelvu  7716  recexpr  7841  cauappcvgprlem1  7862  caucvgprlemnkj  7869  caucvgprlemnbj  7870  caucvgprlemm  7871  caucvgprlemdisj  7877  caucvgprlemloc  7878  caucvgprlemcl  7879  caucvgprlemladdfu  7880  caucvgprlemladdrl  7881  caucvgprlem1  7882  caucvgprlem2  7883  caucvgpr  7885  caucvgprprlemell  7888  caucvgprprlemelu  7889  caucvgprprlemcbv  7890  caucvgprprlemval  7891  caucvgprprlemnkeqj  7893  caucvgprprlemmu  7898  caucvgprprlemopl  7900  caucvgprprlemlol  7901  caucvgprprlemopu  7902  caucvgprprlemloc  7906  caucvgprprlemclphr  7908  caucvgprprlemexbt  7909  caucvgprprlem1  7912  caucvgprprlem2  7913  caucvgsr  8005  axcaucvglemval  8100  axcaucvglemres  8102  fv0p1e1  9241  uzin  9772  cnref1o  9863  fzsuc2  10292  fseq1m1p1  10308  fzoss2  10387  elfzonlteqm1  10433  divfl0  10533  flqzadd  10535  fldiv4p1lem1div2  10542  ceilqval  10545  flqdiv  10560  modqval  10563  modqfrac  10576  modqmulnn  10581  modqid  10588  modqcyc  10598  modqdi  10631  frec2uzuzd  10641  frec2uzrdg  10648  frecuzrdgrcl  10649  frecuzrdgtcl  10651  frecuzrdgsuc  10653  frecuzrdgrclt  10654  frecuzrdgg  10655  frecuzrdgfunlem  10658  frecuzrdgsuctlem  10662  iseqovex  10697  iseqvalcbv  10698  seq3val  10699  seqvalcd  10700  seq3m1  10712  seq3shft2  10720  seqshft2g  10721  monoord  10724  monoord2  10725  iseqf1olemqval  10739  iseqf1olemab  10741  iseqf1olemqk  10746  iseqf1olemjpcl  10747  iseqf1olemqpcl  10748  iseqf1olemfvp  10749  seq3f1olemqsumkj  10750  seq3f1olemqsumk  10751  seq3f1olemqsum  10752  seq3f1olemp  10754  seq3f1oleml  10755  seqf1oglem1  10758  seqf1oglem2  10759  seqf1og  10760  seq3homo  10766  seqhomog  10769  exp3val  10780  expnegap0  10786  facnn2  10973  facwordi  10979  faclbnd6  10983  bcval  10988  bccmpl  10993  bcn0  10994  bcm1k  10999  bcp1n  11000  bcn2  11003  hashinfom  11017  hashennn  11019  hashsng  11037  omgadd  11041  hashprg  11048  fihashssdif  11058  hashdifpr  11060  hashfzo  11062  hashfzp1  11064  hashxp  11066  zfz1isolemiso  11079  zfz1iso  11081  lsw1  11139  ccatfvalfi  11145  ccatlen  11148  ccatval3  11152  ccatval21sw  11158  ccatlid  11159  ccatass  11161  lswccatn0lsw  11164  lswccat0lsw  11165  ccatalpha  11166  s1leng  11177  ccats1val2  11192  lswccats1  11195  swrdfv0  11207  swrdfv2  11216  swrdsbslen  11219  swrds1  11221  ccatswrd  11223  pfxmpt  11233  pfxfv  11237  pfxtrcfvl  11250  ccatpfx  11254  swrdswrd  11258  lenpfxcctswrd  11264  ccatopth  11269  cats1un  11274  swrdccatin2  11282  pfxccatin12lem2  11284  shftval2  11358  shftval3  11359  shftval4  11360  shftval5  11361  seq3shft  11370  imval  11382  imre  11383  reim  11384  crim  11390  reim0  11393  mulreap  11396  recj  11399  reneg  11400  readd  11401  resub  11402  remullem  11403  redivap  11406  imcj  11407  imneg  11408  imadd  11409  imsub  11410  imdivap  11413  cjsub  11424  cjexp  11425  cjreim2  11436  cjap  11438  cjdivap  11441  cnrecnv  11442  cvg1nlemcau  11516  cvg1nlemres  11517  absval  11533  rennim  11534  sqrtdiv  11574  sqrtmsq  11577  absneg  11582  abscj  11584  absval2  11589  absreim  11600  absmul  11601  absdivap  11602  absid  11603  absre  11609  absexp  11611  absexpzap  11612  absimle  11616  abssub  11633  abs3dif  11637  abs2dif  11638  abs2dif2  11639  recan  11641  cau3lem  11646  max0addsup  11751  minabs  11768  bdtrilem  11771  clim  11813  clim2  11815  clim0  11817  clim0c  11818  climi0  11821  climconst  11822  climshftlemg  11834  climcn1  11840  climcn2  11841  addcn2  11842  subcn2  11843  mulcn2  11844  reccn2ap  11845  cjcn2  11848  recn2  11849  imcn2  11850  iser3shft  11878  climcau  11879  climcvg1nlem  11881  climcvg1n  11882  serf0  11884  summodclem3  11912  summodclem2a  11913  summodc  11915  fsumf1o  11922  sumsnf  11941  fsumm1  11948  fsumcnv  11969  fsumabs  11997  fsumrelem  12003  iserabs  12007  hash2iun1dif1  12012  isumshft  12022  isumsplit  12023  expcnvap0  12034  expcnv  12036  cvgratnnlemseq  12058  cvgratnnlemrate  12062  cvgratz  12064  mertenslemub  12066  mertenslemi1  12067  mertenslem2  12068  mertensabs  12069  prodmodclem3  12107  fprodf1o  12120  prodsnf  12124  fprodm1  12130  fprodabs  12148  fprodcnv  12157  efcllemp  12190  efcj  12205  efaddlem  12206  efcan  12208  efsub  12213  efexp  12214  efzval  12215  efgt0  12216  eftlub  12222  efltim  12230  sinval  12234  cosval  12235  tanval3ap  12246  resinval  12247  recosval  12248  resin4p  12250  recos4p  12251  sinneg  12258  cosneg  12259  efmival  12265  efeul  12266  sinadd  12268  cosadd  12269  sinsub  12272  cossub  12273  addsin  12274  subsin  12275  addcos  12278  subcos  12279  sincossq  12280  sin2t  12281  cos2t  12282  sin01bnd  12289  cos01bnd  12290  sin02gt0  12296  cos12dec  12300  absefi  12301  absef  12302  absefib  12303  efieq1re  12304  demoivre  12305  demoivreALT  12306  flodddiv4  12468  bitsval  12475  bits0  12480  bitsp1  12483  bitsp1e  12484  bitsp1o  12485  bitsmod  12488  nninfctlemfo  12582  alginv  12590  algcvg  12591  eucalgval  12597  eucalginv  12599  eucalglt  12600  eucalgcvga  12601  eucalg  12602  lcmgcd  12621  lcm1  12624  sqpweven  12718  2sqpwodd  12719  sqne2sq  12720  qnumval  12728  qdenval  12729  qden1elz  12748  nn0sqrtelqelz  12749  phival  12756  dfphi2  12763  phiprmpw  12765  phiprm  12766  eulerthlemth  12775  hashgcdeq  12783  phisum  12784  pythagtriplem6  12814  pythagtriplem7  12815  pythagtriplem12  12819  pythagtriplem14  12821  fldivp1  12892  4sqlem11  12945  ennnfonelemg  12995  ennnfonelemp1  12998  ennnfonelemkh  13004  ennnfonelemhf1o  13005  ennnfonelemnn0  13014  ctinfomlemom  13019  ctiunctlemu1st  13026  ctiunctlemu2nd  13027  ctiunctlemudc  13029  ctiunctlemfo  13031  isstruct2im  13063  isstruct2r  13064  setsslid  13104  ressbasd  13121  resseqnbasd  13127  ressplusgd  13183  ptex  13318  prdsex  13323  prdsval  13327  prdsbas3  13341  pwsval  13345  pwsbas  13346  pwsplusgval  13349  pwsmulrval  13350  imasex  13359  imasival  13360  f1ocpbl  13365  f1ovscpbl  13366  imasaddvallemg  13369  qusval  13377  fvprif  13397  xpsff1o  13403  igsumvalx  13443  gsumprval  13453  pws0g  13505  imasmnd  13507  ismhm  13515  mhmpropd  13520  mhmlin  13521  mhmf1o  13524  resmhm  13541  mhmco  13544  gsumwmhm  13552  grpinvsub  13636  pwsinvg  13666  imasgrp2  13668  imasgrp  13669  mhmlem  13672  mhmid  13673  mhmmnd  13674  ghmgrp  13676  mulgfvalg  13679  mulgval  13680  mulgnegnn  13690  mulgneg  13698  mulgnegneg  13699  mulgm1  13700  mulginvcom  13705  mulgz  13708  mulgnndir  13709  mulgdir  13712  mulgass  13717  mhmmulg  13721  subgmulg  13746  isnsg  13760  eqgfval  13780  ghmlin  13806  ghmid  13807  ghminv  13808  ghmsub  13809  ghmmulg  13814  resghm  13818  ghmeql  13825  ablsub2inv  13869  ghmcmn  13885  invghm  13887  imasabl  13894  gsumfzreidx  13895  gsumfzmhm  13901  mgpplusgg  13908  mgpbasg  13910  mgpscag  13911  mgptsetg  13912  mgpdsg  13914  rngm2neg  13933  imasrng  13940  isring  13984  ringm2neg  14039  imasring  14048  opprmulfvalg  14054  opprsllem  14058  isunitd  14091  opprunitd  14095  invrfvald  14107  rdivmuldivd  14129  rhmmul  14149  isrhm2d  14150  rhm1  14152  rhmdvdsr  14160  rhmopp  14161  rhmunitinv  14163  islmod  14276  islmodd  14278  scaffvalg  14291  lmodpropd  14334  lsssetm  14341  islssmd  14344  lssats2  14399  lspsnneg  14405  lspsnsub  14406  lspun0  14410  lmodindp1  14413  sralemg  14423  srascag  14427  sravscag  14428  sraipg  14429  rlmscabas  14445  ixpsnbasval  14451  2idlval  14487  2idlvalg  14488  mulgrhm2  14595  zlmlemg  14613  zlmsca  14617  zlmvscag  14618  znval  14621  znle  14622  znbaslemnn  14624  znidomb  14643  psrval  14651  psrbasg  14659  psrplusgg  14663  mplvalcoe  14675  mplsubgfileminv  14685  mpl0fi  14687  mplnegfi  14690  istps  14727  tpspropd  14731  eltpsg  14735  txvalex  14949  txval  14950  txbasval  14962  upxp  14967  uptx  14969  txrest  14971  cnmpt11  14978  cnmpt21  14986  hmeontr  15008  txhmeo  15014  psmetxrge0  15027  xmetunirn  15053  mopnval  15137  mopntopon  15138  isxms  15146  isxms2  15147  isms  15148  msrtri  15171  xmspropd  15172  mspropd  15173  setsmsbasg  15174  setsmsdsg  15175  setsmstsetg  15176  comet  15194  metcnpi  15210  metcnpi2  15211  cnbl0  15229  cnblcld  15230  resubmet  15251  mpomulcn  15261  elcncf  15268  cncfi  15273  rescncf  15276  mulc1cncf  15284  cncfco  15286  cncfmptid  15292  addccncf  15295  cdivcncfap  15299  negcncf  15300  mulcncflem  15302  ivthinclemlopn  15331  ivthinclemuopn  15333  limccl  15354  ellimc3apf  15355  limcimolemlt  15359  cnplimclemle  15363  limccnpcntop  15370  reldvg  15374  dvfvalap  15376  dveflem  15421  dvef  15422  plymullem1  15443  plycjlemc  15455  plycj  15456  plyrecj  15458  plyreres  15459  sin0pilem1  15476  ef2kpi  15501  sinperlem  15503  sin2kpi  15506  cos2kpi  15507  sin2pim  15508  cos2pim  15509  ptolemy  15519  sincosq2sgn  15522  sincosq3sgn  15523  sincosq4sgn  15524  sinq12gt0  15525  tangtx  15533  sincosq1eq  15534  abssinper  15541  sinkpi  15542  coskpi  15543  cosq34lt1  15545  relogeftb  15560  relogoprlem  15563  relogexp  15567  rpcxpef  15589  logcxp  15592  1cxp  15595  ecxp  15596  rpcxpadd  15600  rpmulcxp  15604  cxpmul  15607  abscxp  15610  logsqrt  15618  rpabscxpbnd  15635  rpcxplogb  15659  lgsval  15704  lgsval2lem  15710  lgsval4a  15722  lgsdi  15737  lgseisenlem3  15772  lgseisenlem4  15773  lgsquadlem1  15777  lgsquadlem2  15778  lgsquadlem3  15779  2lgslem1  15791  2lgslem3a  15793  2lgslem3b  15794  2lgslem3c  15795  2lgslem3d  15796  vtxdgfval  16074  vtxdgfifival  16077  vtxdgop  16078  vtxdgfi0e  16081  vtxdeqd  16082  vtxdfifiun  16083  vtxdumgrfival  16084  iswlk  16095  2wlklem  16146  wlkres  16149  clwwlkccatlem  16169  clwwlkn2  16189  clwwlkext2edg  16190  umgr2cwwk2dif  16192  nnsf  16485  peano4nninf  16486  peano3nninf  16487  nninfalllem1  16488  nninfall  16489  nninfsellemdc  16490  nninfsellemeq  16494  nninfsellemqall  16495  nninfsellemeqinf  16496  nninfsel  16497  nnnninfex  16502  exmidsbthr  16505  qdencn  16509  refeq  16510  isomninnlem  16512  apdifflemr  16529  apdiff  16530  ismkvnnlem  16534  nconstwlpolem  16547