Theorem fveq2d 5580

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

Syntax hints:   -> wi 4   = wceq 1373   ` cfv 5271

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 711  ax-5 1470  ax-7 1471  ax-gen 1472  ax-ie1 1516  ax-ie2 1517  ax-8 1527  ax-10 1528  ax-11 1529  ax-i12 1530  ax-bndl 1532  ax-4 1533  ax-17 1549  ax-i9 1553  ax-ial 1557  ax-i5r 1558  ax-ext 2187

This theorem depends on definitions:  df-bi 117  df-3an 983  df-tru 1376  df-nf 1484  df-sb 1786  df-clab 2192  df-cleq 2198  df-clel 2201  df-nfc 2337  df-rex 2490  df-v 2774  df-un 3170  df-sn 3639  df-pr 3640  df-op 3642  df-uni 3851  df-br 4045  df-iota 5232  df-fv 5279

This theorem is referenced by:  2fveq3  5581  fveq12d  5583  fveqeq2d  5584  csbfvg  5616  fvmptdf  5667  fvmptt  5671  fcof1  5852  oveq1  5951  oveq2  5952  fvoveq1d  5966  caofinvl  6184  op1stg  6236  op2ndg  6237  ot1stg  6238  ot2ndg  6239  eloprabi  6282  1stconst  6307  algrflemg  6316  tfrlem1  6394  tfrlem3ag  6395  tfrlem3a  6396  tfrlem9  6405  tfr0dm  6408  tfrlemisucaccv  6411  tfrlemiubacc  6416  tfrlemiex  6417  tfrlemi1  6418  tfr1onlem3ag  6423  tfr1onlemsucaccv  6427  tfr1onlemubacc  6432  tfr1onlemex  6433  tfr1onlemaccex  6434  tfrcllemsucaccv  6440  tfrcllembxssdm  6442  tfrcllemubacc  6445  tfrcllemex  6446  tfrcllemaccex  6447  tfrcllemres  6448  tfrcldm  6449  rdgivallem  6467  rdgival  6468  rdgss  6469  rdgisuc1  6470  rdgon  6472  rdg0  6473  frec0g  6483  frecabcl  6485  freccllem  6488  frecfcllem  6490  frecsuclem  6492  frecsuc  6493  frecrdg  6494  oav2  6549  omv2  6551  xpdom2  6926  xpmapenlem  6946  xpmapen  6947  ac6sfi  6995  1stinl  7176  2ndinl  7177  1stinr  7178  2ndinr  7179  updjudhcoinlf  7182  updjudhcoinrg  7183  caseinl  7193  caseinr  7194  omp1eomlem  7196  omp1eom  7197  difinfsn  7202  ctmlemr  7210  ctm  7211  ctssdclemn0  7212  ctssdccl  7213  nninfninc  7225  nnnninfeq  7230  nnnninfeq2  7231  enomnilem  7240  enmkvlem  7263  enwomnilem  7271  exmidfodomrlemeldju  7307  exmidfodomrlemreseldju  7308  exmidfodomrlemr  7310  exmidfodomrlemrALT  7311  exmidaclem  7320  cc2  7379  cc3  7380  ltdfpr  7619  genpelvl  7625  genpelvu  7626  recexpr  7751  cauappcvgprlem1  7772  caucvgprlemnkj  7779  caucvgprlemnbj  7780  caucvgprlemm  7781  caucvgprlemdisj  7787  caucvgprlemloc  7788  caucvgprlemcl  7789  caucvgprlemladdfu  7790  caucvgprlemladdrl  7791  caucvgprlem1  7792  caucvgprlem2  7793  caucvgpr  7795  caucvgprprlemell  7798  caucvgprprlemelu  7799  caucvgprprlemcbv  7800  caucvgprprlemval  7801  caucvgprprlemnkeqj  7803  caucvgprprlemmu  7808  caucvgprprlemopl  7810  caucvgprprlemlol  7811  caucvgprprlemopu  7812  caucvgprprlemloc  7816  caucvgprprlemclphr  7818  caucvgprprlemexbt  7819  caucvgprprlem1  7822  caucvgprprlem2  7823  caucvgsr  7915  axcaucvglemval  8010  axcaucvglemres  8012  fv0p1e1  9151  uzin  9681  cnref1o  9772  fzsuc2  10201  fseq1m1p1  10217  fzoss2  10296  elfzonlteqm1  10339  divfl0  10439  flqzadd  10441  fldiv4p1lem1div2  10448  ceilqval  10451  flqdiv  10466  modqval  10469  modqfrac  10482  modqmulnn  10487  modqid  10494  modqcyc  10504  modqdi  10537  frec2uzuzd  10547  frec2uzrdg  10554  frecuzrdgrcl  10555  frecuzrdgtcl  10557  frecuzrdgsuc  10559  frecuzrdgrclt  10560  frecuzrdgg  10561  frecuzrdgfunlem  10564  frecuzrdgsuctlem  10568  iseqovex  10603  iseqvalcbv  10604  seq3val  10605  seqvalcd  10606  seq3m1  10618  seq3shft2  10626  seqshft2g  10627  monoord  10630  monoord2  10631  iseqf1olemqval  10645  iseqf1olemab  10647  iseqf1olemqk  10652  iseqf1olemjpcl  10653  iseqf1olemqpcl  10654  iseqf1olemfvp  10655  seq3f1olemqsumkj  10656  seq3f1olemqsumk  10657  seq3f1olemqsum  10658  seq3f1olemp  10660  seq3f1oleml  10661  seqf1oglem1  10664  seqf1oglem2  10665  seqf1og  10666  seq3homo  10672  seqhomog  10675  exp3val  10686  expnegap0  10692  facnn2  10879  facwordi  10885  faclbnd6  10889  bcval  10894  bccmpl  10899  bcn0  10900  bcm1k  10905  bcp1n  10906  bcn2  10909  hashinfom  10923  hashennn  10925  hashsng  10943  omgadd  10947  hashprg  10953  fihashssdif  10963  hashdifpr  10965  hashfzo  10967  hashfzp1  10969  hashxp  10971  zfz1isolemiso  10984  zfz1iso  10986  lsw1  11043  ccatfvalfi  11048  ccatlen  11051  ccatval3  11055  ccatval21sw  11061  ccatlid  11062  ccatass  11064  lswccatn0lsw  11067  lswccat0lsw  11068  s1leng  11078  ccats1val2  11092  lswccats1  11095  swrdfv0  11107  swrdfv2  11116  swrdsbslen  11119  swrds1  11121  ccatswrd  11123  shftval2  11137  shftval3  11138  shftval4  11139  shftval5  11140  seq3shft  11149  imval  11161  imre  11162  reim  11163  crim  11169  reim0  11172  mulreap  11175  recj  11178  reneg  11179  readd  11180  resub  11181  remullem  11182  redivap  11185  imcj  11186  imneg  11187  imadd  11188  imsub  11189  imdivap  11192  cjsub  11203  cjexp  11204  cjreim2  11215  cjap  11217  cjdivap  11220  cnrecnv  11221  cvg1nlemcau  11295  cvg1nlemres  11296  absval  11312  rennim  11313  sqrtdiv  11353  sqrtmsq  11356  absneg  11361  abscj  11363  absval2  11368  absreim  11379  absmul  11380  absdivap  11381  absid  11382  absre  11388  absexp  11390  absexpzap  11391  absimle  11395  abssub  11412  abs3dif  11416  abs2dif  11417  abs2dif2  11418  recan  11420  cau3lem  11425  max0addsup  11530  minabs  11547  bdtrilem  11550  clim  11592  clim2  11594  clim0  11596  clim0c  11597  climi0  11600  climconst  11601  climshftlemg  11613  climcn1  11619  climcn2  11620  addcn2  11621  subcn2  11622  mulcn2  11623  reccn2ap  11624  cjcn2  11627  recn2  11628  imcn2  11629  iser3shft  11657  climcau  11658  climcvg1nlem  11660  climcvg1n  11661  serf0  11663  summodclem3  11691  summodclem2a  11692  summodc  11694  fsumf1o  11701  sumsnf  11720  fsumm1  11727  fsumcnv  11748  fsumabs  11776  fsumrelem  11782  iserabs  11786  hash2iun1dif1  11791  isumshft  11801  isumsplit  11802  expcnvap0  11813  expcnv  11815  cvgratnnlemseq  11837  cvgratnnlemrate  11841  cvgratz  11843  mertenslemub  11845  mertenslemi1  11846  mertenslem2  11847  mertensabs  11848  prodmodclem3  11886  fprodf1o  11899  prodsnf  11903  fprodm1  11909  fprodabs  11927  fprodcnv  11936  efcllemp  11969  efcj  11984  efaddlem  11985  efcan  11987  efsub  11992  efexp  11993  efzval  11994  efgt0  11995  eftlub  12001  efltim  12009  sinval  12013  cosval  12014  tanval3ap  12025  resinval  12026  recosval  12027  resin4p  12029  recos4p  12030  sinneg  12037  cosneg  12038  efmival  12044  efeul  12045  sinadd  12047  cosadd  12048  sinsub  12051  cossub  12052  addsin  12053  subsin  12054  addcos  12057  subcos  12058  sincossq  12059  sin2t  12060  cos2t  12061  sin01bnd  12068  cos01bnd  12069  sin02gt0  12075  cos12dec  12079  absefi  12080  absef  12081  absefib  12082  efieq1re  12083  demoivre  12084  demoivreALT  12085  flodddiv4  12247  bitsval  12254  bits0  12259  bitsp1  12262  bitsp1e  12263  bitsp1o  12264  bitsmod  12267  nninfctlemfo  12361  alginv  12369  algcvg  12370  eucalgval  12376  eucalginv  12378  eucalglt  12379  eucalgcvga  12380  eucalg  12381  lcmgcd  12400  lcm1  12403  sqpweven  12497  2sqpwodd  12498  sqne2sq  12499  qnumval  12507  qdenval  12508  qden1elz  12527  nn0sqrtelqelz  12528  phival  12535  dfphi2  12542  phiprmpw  12544  phiprm  12545  eulerthlemth  12554  hashgcdeq  12562  phisum  12563  pythagtriplem6  12593  pythagtriplem7  12594  pythagtriplem12  12598  pythagtriplem14  12600  fldivp1  12671  4sqlem11  12724  ennnfonelemg  12774  ennnfonelemp1  12777  ennnfonelemkh  12783  ennnfonelemhf1o  12784  ennnfonelemnn0  12793  ctinfomlemom  12798  ctiunctlemu1st  12805  ctiunctlemu2nd  12806  ctiunctlemudc  12808  ctiunctlemfo  12810  isstruct2im  12842  isstruct2r  12843  setsslid  12883  ressbasd  12899  resseqnbasd  12905  ressplusgd  12961  ptex  13096  prdsex  13101  prdsval  13105  prdsbas3  13119  pwsval  13123  pwsbas  13124  pwsplusgval  13127  pwsmulrval  13128  imasex  13137  imasival  13138  f1ocpbl  13143  f1ovscpbl  13144  imasaddvallemg  13147  qusval  13155  fvprif  13175  xpsff1o  13181  igsumvalx  13221  gsumprval  13231  pws0g  13283  imasmnd  13285  ismhm  13293  mhmpropd  13298  mhmlin  13299  mhmf1o  13302  resmhm  13319  mhmco  13322  gsumwmhm  13330  grpinvsub  13414  pwsinvg  13444  imasgrp2  13446  imasgrp  13447  mhmlem  13450  mhmid  13451  mhmmnd  13452  ghmgrp  13454  mulgfvalg  13457  mulgval  13458  mulgnegnn  13468  mulgneg  13476  mulgnegneg  13477  mulgm1  13478  mulginvcom  13483  mulgz  13486  mulgnndir  13487  mulgdir  13490  mulgass  13495  mhmmulg  13499  subgmulg  13524  isnsg  13538  eqgfval  13558  ghmlin  13584  ghmid  13585  ghminv  13586  ghmsub  13587  ghmmulg  13592  resghm  13596  ghmeql  13603  ablsub2inv  13647  ghmcmn  13663  invghm  13665  imasabl  13672  gsumfzreidx  13673  gsumfzmhm  13679  mgpplusgg  13686  mgpbasg  13688  mgpscag  13689  mgptsetg  13690  mgpdsg  13692  rngm2neg  13711  imasrng  13718  isring  13762  ringm2neg  13817  imasring  13826  opprmulfvalg  13832  opprsllem  13836  isunitd  13868  opprunitd  13872  invrfvald  13884  rdivmuldivd  13906  rhmmul  13926  isrhm2d  13927  rhm1  13929  rhmdvdsr  13937  rhmopp  13938  rhmunitinv  13940  islmod  14053  islmodd  14055  scaffvalg  14068  lmodpropd  14111  lsssetm  14118  islssmd  14121  lssats2  14176  lspsnneg  14182  lspsnsub  14183  lspun0  14187  lmodindp1  14190  sralemg  14200  srascag  14204  sravscag  14205  sraipg  14206  rlmscabas  14222  ixpsnbasval  14228  2idlval  14264  2idlvalg  14265  mulgrhm2  14372  zlmlemg  14390  zlmsca  14394  zlmvscag  14395  znval  14398  znle  14399  znbaslemnn  14401  znidomb  14420  psrval  14428  psrbasg  14436  psrplusgg  14440  mplvalcoe  14452  mplsubgfileminv  14462  mpl0fi  14464  mplnegfi  14467  istps  14504  tpspropd  14508  eltpsg  14512  txvalex  14726  txval  14727  txbasval  14739  upxp  14744  uptx  14746  txrest  14748  cnmpt11  14755  cnmpt21  14763  hmeontr  14785  txhmeo  14791  psmetxrge0  14804  xmetunirn  14830  mopnval  14914  mopntopon  14915  isxms  14923  isxms2  14924  isms  14925  msrtri  14948  xmspropd  14949  mspropd  14950  setsmsbasg  14951  setsmsdsg  14952  setsmstsetg  14953  comet  14971  metcnpi  14987  metcnpi2  14988  cnbl0  15006  cnblcld  15007  resubmet  15028  mpomulcn  15038  elcncf  15045  cncfi  15050  rescncf  15053  mulc1cncf  15061  cncfco  15063  cncfmptid  15069  addccncf  15072  cdivcncfap  15076  negcncf  15077  mulcncflem  15079  ivthinclemlopn  15108  ivthinclemuopn  15110  limccl  15131  ellimc3apf  15132  limcimolemlt  15136  cnplimclemle  15140  limccnpcntop  15147  reldvg  15151  dvfvalap  15153  dveflem  15198  dvef  15199  plymullem1  15220  plycjlemc  15232  plycj  15233  plyrecj  15235  plyreres  15236  sin0pilem1  15253  ef2kpi  15278  sinperlem  15280  sin2kpi  15283  cos2kpi  15284  sin2pim  15285  cos2pim  15286  ptolemy  15296  sincosq2sgn  15299  sincosq3sgn  15300  sincosq4sgn  15301  sinq12gt0  15302  tangtx  15310  sincosq1eq  15311  abssinper  15318  sinkpi  15319  coskpi  15320  cosq34lt1  15322  relogeftb  15337  relogoprlem  15340  relogexp  15344  rpcxpef  15366  logcxp  15369  1cxp  15372  ecxp  15373  rpcxpadd  15377  rpmulcxp  15381  cxpmul  15384  abscxp  15387  logsqrt  15395  rpabscxpbnd  15412  rpcxplogb  15436  lgsval  15481  lgsval2lem  15487  lgsval4a  15499  lgsdi  15514  lgseisenlem3  15549  lgseisenlem4  15550  lgsquadlem1  15554  lgsquadlem2  15555  lgsquadlem3  15556  2lgslem1  15568  2lgslem3a  15570  2lgslem3b  15571  2lgslem3c  15572  2lgslem3d  15573  nnsf  15942  peano4nninf  15943  peano3nninf  15944  nninfalllem1  15945  nninfall  15946  nninfsellemdc  15947  nninfsellemeq  15951  nninfsellemqall  15952  nninfsellemeqinf  15953  nninfsel  15954  nnnninfex  15959  exmidsbthr  15962  qdencn  15966  refeq  15967  isomninnlem  15969  apdifflemr  15986  apdiff  15987  ismkvnnlem  15991  nconstwlpolem  16004