Theorem fveq2d 5643

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

Syntax hints:   -> wi 4   = wceq 1397   ` cfv 5326

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 716  ax-5 1495  ax-7 1496  ax-gen 1497  ax-ie1 1541  ax-ie2 1542  ax-8 1552  ax-10 1553  ax-11 1554  ax-i12 1555  ax-bndl 1557  ax-4 1558  ax-17 1574  ax-i9 1578  ax-ial 1582  ax-i5r 1583  ax-ext 2213

This theorem depends on definitions:  df-bi 117  df-3an 1006  df-tru 1400  df-nf 1509  df-sb 1811  df-clab 2218  df-cleq 2224  df-clel 2227  df-nfc 2363  df-rex 2516  df-v 2804  df-un 3204  df-sn 3675  df-pr 3676  df-op 3678  df-uni 3894  df-br 4089  df-iota 5286  df-fv 5334

This theorem is referenced by:  2fveq3  5644  fveq12d  5646  fveqeq2d  5647  csbfvg  5681  fvmptdf  5734  fvmptt  5738  resfvresima  5891  fcof1  5924  oveq1  6025  oveq2  6026  fvoveq1d  6040  caofinvl  6261  op1stg  6313  op2ndg  6314  ot1stg  6315  ot2ndg  6316  eloprabi  6361  1stconst  6386  algrflemg  6395  tfrlem1  6474  tfrlem3ag  6475  tfrlem3a  6476  tfrlem9  6485  tfr0dm  6488  tfrlemisucaccv  6491  tfrlemiubacc  6496  tfrlemiex  6497  tfrlemi1  6498  tfr1onlem3ag  6503  tfr1onlemsucaccv  6507  tfr1onlemubacc  6512  tfr1onlemex  6513  tfr1onlemaccex  6514  tfrcllemsucaccv  6520  tfrcllembxssdm  6522  tfrcllemubacc  6525  tfrcllemex  6526  tfrcllemaccex  6527  tfrcllemres  6528  tfrcldm  6529  rdgivallem  6547  rdgival  6548  rdgss  6549  rdgisuc1  6550  rdgon  6552  rdg0  6553  frec0g  6563  frecabcl  6565  freccllem  6568  frecfcllem  6570  frecsuclem  6572  frecsuc  6573  frecrdg  6574  oav2  6631  omv2  6633  xpdom2  7015  xpmapenlem  7035  xpmapen  7036  ac6sfi  7087  1stinl  7273  2ndinl  7274  1stinr  7275  2ndinr  7276  updjudhcoinlf  7279  updjudhcoinrg  7280  caseinl  7290  caseinr  7291  omp1eomlem  7293  omp1eom  7294  difinfsn  7299  ctmlemr  7307  ctm  7308  ctssdclemn0  7309  ctssdccl  7310  nninfninc  7322  nnnninfeq  7327  nnnninfeq2  7328  enomnilem  7337  enmkvlem  7360  enwomnilem  7368  exmidfodomrlemeldju  7410  exmidfodomrlemreseldju  7411  exmidfodomrlemr  7413  exmidfodomrlemrALT  7414  exmidaclem  7423  cc2  7486  cc3  7487  ltdfpr  7726  genpelvl  7732  genpelvu  7733  recexpr  7858  cauappcvgprlem1  7879  caucvgprlemnkj  7886  caucvgprlemnbj  7887  caucvgprlemm  7888  caucvgprlemdisj  7894  caucvgprlemloc  7895  caucvgprlemcl  7896  caucvgprlemladdfu  7897  caucvgprlemladdrl  7898  caucvgprlem1  7899  caucvgprlem2  7900  caucvgpr  7902  caucvgprprlemell  7905  caucvgprprlemelu  7906  caucvgprprlemcbv  7907  caucvgprprlemval  7908  caucvgprprlemnkeqj  7910  caucvgprprlemmu  7915  caucvgprprlemopl  7917  caucvgprprlemlol  7918  caucvgprprlemopu  7919  caucvgprprlemloc  7923  caucvgprprlemclphr  7925  caucvgprprlemexbt  7926  caucvgprprlem1  7929  caucvgprprlem2  7930  caucvgsr  8022  axcaucvglemval  8117  axcaucvglemres  8119  fv0p1e1  9258  uzin  9789  cnref1o  9885  fzsuc2  10314  fseq1m1p1  10330  fzoss2  10409  elfzonlteqm1  10456  divfl0  10557  flqzadd  10559  fldiv4p1lem1div2  10566  ceilqval  10569  flqdiv  10584  modqval  10587  modqfrac  10600  modqmulnn  10605  modqid  10612  modqcyc  10622  modqdi  10655  frec2uzuzd  10665  frec2uzrdg  10672  frecuzrdgrcl  10673  frecuzrdgtcl  10675  frecuzrdgsuc  10677  frecuzrdgrclt  10678  frecuzrdgg  10679  frecuzrdgfunlem  10682  frecuzrdgsuctlem  10686  iseqovex  10721  iseqvalcbv  10722  seq3val  10723  seqvalcd  10724  seq3m1  10736  seq3shft2  10744  seqshft2g  10745  monoord  10748  monoord2  10749  iseqf1olemqval  10763  iseqf1olemab  10765  iseqf1olemqk  10770  iseqf1olemjpcl  10771  iseqf1olemqpcl  10772  iseqf1olemfvp  10773  seq3f1olemqsumkj  10774  seq3f1olemqsumk  10775  seq3f1olemqsum  10776  seq3f1olemp  10778  seq3f1oleml  10779  seqf1oglem1  10782  seqf1oglem2  10783  seqf1og  10784  seq3homo  10790  seqhomog  10793  exp3val  10804  expnegap0  10810  facnn2  10997  facwordi  11003  faclbnd6  11007  bcval  11012  bccmpl  11017  bcn0  11018  bcm1k  11023  bcp1n  11024  bcn2  11027  hashinfom  11041  hashennn  11043  hashsng  11061  omgadd  11066  hashprg  11073  fihashssdif  11083  hashdifpr  11085  hashfzo  11087  hashfzp1  11089  hashxp  11091  zfz1isolemiso  11104  zfz1iso  11106  hashtpglem  11111  lsw1  11167  ccatfvalfi  11173  ccatlen  11176  ccatval3  11180  ccatval21sw  11186  ccatlid  11187  ccatass  11189  lswccatn0lsw  11192  lswccat0lsw  11193  ccatalpha  11194  s1leng  11205  ccats1val2  11221  lswccats1  11224  swrdfv0  11239  swrdfv2  11248  swrdsbslen  11251  swrds1  11253  ccatswrd  11255  pfxmpt  11265  pfxfv  11269  pfxtrcfvl  11282  ccatpfx  11286  swrdswrd  11290  lenpfxcctswrd  11296  ccatopth  11301  cats1un  11306  swrdccatin2  11314  pfxccatin12lem2  11316  shftval2  11404  shftval3  11405  shftval4  11406  shftval5  11407  seq3shft  11416  imval  11428  imre  11429  reim  11430  crim  11436  reim0  11439  mulreap  11442  recj  11445  reneg  11446  readd  11447  resub  11448  remullem  11449  redivap  11452  imcj  11453  imneg  11454  imadd  11455  imsub  11456  imdivap  11459  cjsub  11470  cjexp  11471  cjreim2  11482  cjap  11484  cjdivap  11487  cnrecnv  11488  cvg1nlemcau  11562  cvg1nlemres  11563  absval  11579  rennim  11580  sqrtdiv  11620  sqrtmsq  11623  absneg  11628  abscj  11630  absval2  11635  absreim  11646  absmul  11647  absdivap  11648  absid  11649  absre  11655  absexp  11657  absexpzap  11658  absimle  11662  abssub  11679  abs3dif  11683  abs2dif  11684  abs2dif2  11685  recan  11687  cau3lem  11692  max0addsup  11797  minabs  11814  bdtrilem  11817  clim  11859  clim2  11861  clim0  11863  clim0c  11864  climi0  11867  climconst  11868  climshftlemg  11880  climcn1  11886  climcn2  11887  addcn2  11888  subcn2  11889  mulcn2  11890  reccn2ap  11891  cjcn2  11894  recn2  11895  imcn2  11896  iser3shft  11924  climcau  11925  climcvg1nlem  11927  climcvg1n  11928  serf0  11930  fzf1o  11954  summodclem3  11959  summodclem2a  11960  summodc  11962  fsumf1o  11969  sumsnf  11988  fsumm1  11995  fsumcnv  12016  fsumabs  12044  fsumrelem  12050  iserabs  12054  hash2iun1dif1  12059  isumshft  12069  isumsplit  12070  expcnvap0  12081  expcnv  12083  cvgratnnlemseq  12105  cvgratnnlemrate  12109  cvgratz  12111  mertenslemub  12113  mertenslemi1  12114  mertenslem2  12115  mertensabs  12116  prodmodclem3  12154  fprodf1o  12167  prodsnf  12171  fprodm1  12177  fprodabs  12195  fprodcnv  12204  efcllemp  12237  efcj  12252  efaddlem  12253  efcan  12255  efsub  12260  efexp  12261  efzval  12262  efgt0  12263  eftlub  12269  efltim  12277  sinval  12281  cosval  12282  tanval3ap  12293  resinval  12294  recosval  12295  resin4p  12297  recos4p  12298  sinneg  12305  cosneg  12306  efmival  12312  efeul  12313  sinadd  12315  cosadd  12316  sinsub  12319  cossub  12320  addsin  12321  subsin  12322  addcos  12325  subcos  12326  sincossq  12327  sin2t  12328  cos2t  12329  sin01bnd  12336  cos01bnd  12337  sin02gt0  12343  cos12dec  12347  absefi  12348  absef  12349  absefib  12350  efieq1re  12351  demoivre  12352  demoivreALT  12353  flodddiv4  12515  bitsval  12522  bits0  12527  bitsp1  12530  bitsp1e  12531  bitsp1o  12532  bitsmod  12535  nninfctlemfo  12629  alginv  12637  algcvg  12638  eucalgval  12644  eucalginv  12646  eucalglt  12647  eucalgcvga  12648  eucalg  12649  lcmgcd  12668  lcm1  12671  sqpweven  12765  2sqpwodd  12766  sqne2sq  12767  qnumval  12775  qdenval  12776  qden1elz  12795  nn0sqrtelqelz  12796  phival  12803  dfphi2  12810  phiprmpw  12812  phiprm  12813  eulerthlemth  12822  hashgcdeq  12830  phisum  12831  pythagtriplem6  12861  pythagtriplem7  12862  pythagtriplem12  12866  pythagtriplem14  12868  fldivp1  12939  4sqlem11  12992  ennnfonelemg  13042  ennnfonelemp1  13045  ennnfonelemkh  13051  ennnfonelemhf1o  13052  ennnfonelemnn0  13061  ctinfomlemom  13066  ctiunctlemu1st  13073  ctiunctlemu2nd  13074  ctiunctlemudc  13076  ctiunctlemfo  13078  isstruct2im  13110  isstruct2r  13111  setsslid  13151  ressbasd  13168  resseqnbasd  13174  ressplusgd  13230  ptex  13365  prdsex  13370  prdsval  13374  prdsbas3  13388  pwsval  13392  pwsbas  13393  pwsplusgval  13396  pwsmulrval  13397  imasex  13406  imasival  13407  f1ocpbl  13412  f1ovscpbl  13413  imasaddvallemg  13416  qusval  13424  fvprif  13444  xpsff1o  13450  igsumvalx  13490  gsumprval  13500  pws0g  13552  imasmnd  13554  ismhm  13562  mhmpropd  13567  mhmlin  13568  mhmf1o  13571  resmhm  13588  mhmco  13591  gsumwmhm  13599  grpinvsub  13683  pwsinvg  13713  imasgrp2  13715  imasgrp  13716  mhmlem  13719  mhmid  13720  mhmmnd  13721  ghmgrp  13723  mulgfvalg  13726  mulgval  13727  mulgnegnn  13737  mulgneg  13745  mulgnegneg  13746  mulgm1  13747  mulginvcom  13752  mulgz  13755  mulgnndir  13756  mulgdir  13759  mulgass  13764  mhmmulg  13768  subgmulg  13793  isnsg  13807  eqgfval  13827  ghmlin  13853  ghmid  13854  ghminv  13855  ghmsub  13856  ghmmulg  13861  resghm  13865  ghmeql  13872  ablsub2inv  13916  ghmcmn  13932  invghm  13934  imasabl  13941  gsumfzreidx  13942  gsumfzmhm  13948  gsumsplit0  13951  mgpplusgg  13956  mgpbasg  13958  mgpscag  13959  mgptsetg  13960  mgpdsg  13962  rngm2neg  13981  imasrng  13988  isring  14032  ringm2neg  14087  imasring  14096  opprmulfvalg  14102  opprsllem  14106  isunitd  14139  opprunitd  14143  invrfvald  14155  rdivmuldivd  14177  rhmmul  14197  isrhm2d  14198  rhm1  14200  rhmdvdsr  14208  rhmopp  14209  rhmunitinv  14211  islmod  14324  islmodd  14326  scaffvalg  14339  lmodpropd  14382  lsssetm  14389  islssmd  14392  lssats2  14447  lspsnneg  14453  lspsnsub  14454  lspun0  14458  lmodindp1  14461  sralemg  14471  srascag  14475  sravscag  14476  sraipg  14477  rlmscabas  14493  ixpsnbasval  14499  2idlval  14535  2idlvalg  14536  mulgrhm2  14643  zlmlemg  14661  zlmsca  14665  zlmvscag  14666  znval  14669  znle  14670  znbaslemnn  14672  znidomb  14691  psrval  14699  psrbasg  14707  psrplusgg  14711  mplvalcoe  14723  mplsubgfileminv  14733  mpl0fi  14735  mplnegfi  14738  istps  14775  tpspropd  14779  eltpsg  14783  txvalex  14997  txval  14998  txbasval  15010  upxp  15015  uptx  15017  txrest  15019  cnmpt11  15026  cnmpt21  15034  hmeontr  15056  txhmeo  15062  psmetxrge0  15075  xmetunirn  15101  mopnval  15185  mopntopon  15186  isxms  15194  isxms2  15195  isms  15196  msrtri  15219  xmspropd  15220  mspropd  15221  setsmsbasg  15222  setsmsdsg  15223  setsmstsetg  15224  comet  15242  metcnpi  15258  metcnpi2  15259  cnbl0  15277  cnblcld  15278  resubmet  15299  mpomulcn  15309  elcncf  15316  cncfi  15321  rescncf  15324  mulc1cncf  15332  cncfco  15334  cncfmptid  15340  addccncf  15343  cdivcncfap  15347  negcncf  15348  mulcncflem  15350  ivthinclemlopn  15379  ivthinclemuopn  15381  limccl  15402  ellimc3apf  15403  limcimolemlt  15407  cnplimclemle  15411  limccnpcntop  15418  reldvg  15422  dvfvalap  15424  dveflem  15469  dvef  15470  plymullem1  15491  plycjlemc  15503  plycj  15504  plyrecj  15506  plyreres  15507  sin0pilem1  15524  ef2kpi  15549  sinperlem  15551  sin2kpi  15554  cos2kpi  15555  sin2pim  15556  cos2pim  15557  ptolemy  15567  sincosq2sgn  15570  sincosq3sgn  15571  sincosq4sgn  15572  sinq12gt0  15573  tangtx  15581  sincosq1eq  15582  abssinper  15589  sinkpi  15590  coskpi  15591  cosq34lt1  15593  relogeftb  15608  relogoprlem  15611  relogexp  15615  rpcxpef  15637  logcxp  15640  1cxp  15643  ecxp  15644  rpcxpadd  15648  rpmulcxp  15652  cxpmul  15655  abscxp  15658  logsqrt  15666  rpabscxpbnd  15683  rpcxplogb  15707  lgsval  15752  lgsval2lem  15758  lgsval4a  15770  lgsdi  15785  lgseisenlem3  15820  lgseisenlem4  15821  lgsquadlem1  15825  lgsquadlem2  15826  lgsquadlem3  15827  2lgslem1  15839  2lgslem3a  15841  2lgslem3b  15842  2lgslem3c  15843  2lgslem3d  15844  vtxdgfval  16158  vtxdgfifival  16161  vtxdgop  16162  vtxdgfi0e  16165  vtxdeqd  16166  vtxdfifiun  16167  vtxdumgrfival  16168  1hevtxdg1en  16178  iswlk  16193  2wlklem  16246  wlkres  16249  clwwlkccatlem  16270  clwwlkn2  16291  clwwlkext2edg  16292  umgr2cwwk2dif  16294  clwwlknonex2lem2  16308  eupth2fi  16349  eulerpathprum  16350  depindlem1  16376  depind  16379  nnsf  16658  peano4nninf  16659  peano3nninf  16660  nninfalllem1  16661  nninfall  16662  nninfsellemdc  16663  nninfsellemeq  16667  nninfsellemqall  16668  nninfsellemeqinf  16669  nninfsel  16670  nnnninfex  16675  exmidsbthr  16678  qdencn  16682  refeq  16683  isomninnlem  16685  apdifflemr  16702  apdiff  16703  qdiff  16704  ismkvnnlem  16708  nconstwlpolem  16721  gfsumval  16732  gsumgfsumlem  16735  gfsump1  16738