Theorem fveq2d 5579

Description: Equality deduction for function value. (Contributed by NM, 29-May-1999.)

Hypothesis

Ref	Expression
fveq2d.1	⊢ (𝜑 → 𝐴 = 𝐵)

Assertion

Ref	Expression
fveq2d	⊢ (𝜑 → (𝐹‘𝐴) = (𝐹‘𝐵))

Proof of Theorem fveq2d

Step	Hyp	Ref	Expression
1		fveq2d.1	. 2 ⊢ (𝜑 → 𝐴 = 𝐵)
2		fveq2 5575	. 2 ⊢ (𝐴 = 𝐵 → (𝐹‘𝐴) = (𝐹‘𝐵))
3	1, 2	syl 14	1 ⊢ (𝜑 → (𝐹‘𝐴) = (𝐹‘𝐵))

Syntax hints:   → wi 4   = wceq 1372  ‘cfv 5270

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 710  ax-5 1469  ax-7 1470  ax-gen 1471  ax-ie1 1515  ax-ie2 1516  ax-8 1526  ax-10 1527  ax-11 1528  ax-i12 1529  ax-bndl 1531  ax-4 1532  ax-17 1548  ax-i9 1552  ax-ial 1556  ax-i5r 1557  ax-ext 2186

This theorem depends on definitions:  df-bi 117  df-3an 982  df-tru 1375  df-nf 1483  df-sb 1785  df-clab 2191  df-cleq 2197  df-clel 2200  df-nfc 2336  df-rex 2489  df-v 2773  df-un 3169  df-sn 3638  df-pr 3639  df-op 3641  df-uni 3850  df-br 4044  df-iota 5231  df-fv 5278

This theorem is referenced by:  2fveq3  5580  fveq12d  5582  fveqeq2d  5583  csbfvg  5615  fvmptdf  5666  fvmptt  5670  fcof1  5851  oveq1  5950  oveq2  5951  fvoveq1d  5965  caofinvl  6183  op1stg  6235  op2ndg  6236  ot1stg  6237  ot2ndg  6238  eloprabi  6281  1stconst  6306  algrflemg  6315  tfrlem1  6393  tfrlem3ag  6394  tfrlem3a  6395  tfrlem9  6404  tfr0dm  6407  tfrlemisucaccv  6410  tfrlemiubacc  6415  tfrlemiex  6416  tfrlemi1  6417  tfr1onlem3ag  6422  tfr1onlemsucaccv  6426  tfr1onlemubacc  6431  tfr1onlemex  6432  tfr1onlemaccex  6433  tfrcllemsucaccv  6439  tfrcllembxssdm  6441  tfrcllemubacc  6444  tfrcllemex  6445  tfrcllemaccex  6446  tfrcllemres  6447  tfrcldm  6448  rdgivallem  6466  rdgival  6467  rdgss  6468  rdgisuc1  6469  rdgon  6471  rdg0  6472  frec0g  6482  frecabcl  6484  freccllem  6487  frecfcllem  6489  frecsuclem  6491  frecsuc  6492  frecrdg  6493  oav2  6548  omv2  6550  xpdom2  6925  xpmapenlem  6945  xpmapen  6946  ac6sfi  6994  1stinl  7175  2ndinl  7176  1stinr  7177  2ndinr  7178  updjudhcoinlf  7181  updjudhcoinrg  7182  caseinl  7192  caseinr  7193  omp1eomlem  7195  omp1eom  7196  difinfsn  7201  ctmlemr  7209  ctm  7210  ctssdclemn0  7211  ctssdccl  7212  nninfninc  7224  nnnninfeq  7229  nnnninfeq2  7230  enomnilem  7239  enmkvlem  7262  enwomnilem  7270  exmidfodomrlemeldju  7306  exmidfodomrlemreseldju  7307  exmidfodomrlemr  7309  exmidfodomrlemrALT  7310  exmidaclem  7319  cc2  7378  cc3  7379  ltdfpr  7618  genpelvl  7624  genpelvu  7625  recexpr  7750  cauappcvgprlem1  7771  caucvgprlemnkj  7778  caucvgprlemnbj  7779  caucvgprlemm  7780  caucvgprlemdisj  7786  caucvgprlemloc  7787  caucvgprlemcl  7788  caucvgprlemladdfu  7789  caucvgprlemladdrl  7790  caucvgprlem1  7791  caucvgprlem2  7792  caucvgpr  7794  caucvgprprlemell  7797  caucvgprprlemelu  7798  caucvgprprlemcbv  7799  caucvgprprlemval  7800  caucvgprprlemnkeqj  7802  caucvgprprlemmu  7807  caucvgprprlemopl  7809  caucvgprprlemlol  7810  caucvgprprlemopu  7811  caucvgprprlemloc  7815  caucvgprprlemclphr  7817  caucvgprprlemexbt  7818  caucvgprprlem1  7821  caucvgprprlem2  7822  caucvgsr  7914  axcaucvglemval  8009  axcaucvglemres  8011  fv0p1e1  9150  uzin  9680  cnref1o  9771  fzsuc2  10200  fseq1m1p1  10216  fzoss2  10294  elfzonlteqm1  10337  divfl0  10437  flqzadd  10439  fldiv4p1lem1div2  10446  ceilqval  10449  flqdiv  10464  modqval  10467  modqfrac  10480  modqmulnn  10485  modqid  10492  modqcyc  10502  modqdi  10535  frec2uzuzd  10545  frec2uzrdg  10552  frecuzrdgrcl  10553  frecuzrdgtcl  10555  frecuzrdgsuc  10557  frecuzrdgrclt  10558  frecuzrdgg  10559  frecuzrdgfunlem  10562  frecuzrdgsuctlem  10566  iseqovex  10601  iseqvalcbv  10602  seq3val  10603  seqvalcd  10604  seq3m1  10616  seq3shft2  10624  seqshft2g  10625  monoord  10628  monoord2  10629  iseqf1olemqval  10643  iseqf1olemab  10645  iseqf1olemqk  10650  iseqf1olemjpcl  10651  iseqf1olemqpcl  10652  iseqf1olemfvp  10653  seq3f1olemqsumkj  10654  seq3f1olemqsumk  10655  seq3f1olemqsum  10656  seq3f1olemp  10658  seq3f1oleml  10659  seqf1oglem1  10662  seqf1oglem2  10663  seqf1og  10664  seq3homo  10670  seqhomog  10673  exp3val  10684  expnegap0  10690  facnn2  10877  facwordi  10883  faclbnd6  10887  bcval  10892  bccmpl  10897  bcn0  10898  bcm1k  10903  bcp1n  10904  bcn2  10907  hashinfom  10921  hashennn  10923  hashsng  10941  omgadd  10945  hashprg  10951  fihashssdif  10961  hashdifpr  10963  hashfzo  10965  hashfzp1  10967  hashxp  10969  zfz1isolemiso  10982  zfz1iso  10984  lsw1  11041  ccatfvalfi  11046  ccatlen  11049  ccatval3  11053  ccatval21sw  11059  ccatlid  11060  ccatass  11062  lswccatn0lsw  11065  lswccat0lsw  11066  shftval2  11079  shftval3  11080  shftval4  11081  shftval5  11082  seq3shft  11091  imval  11103  imre  11104  reim  11105  crim  11111  reim0  11114  mulreap  11117  recj  11120  reneg  11121  readd  11122  resub  11123  remullem  11124  redivap  11127  imcj  11128  imneg  11129  imadd  11130  imsub  11131  imdivap  11134  cjsub  11145  cjexp  11146  cjreim2  11157  cjap  11159  cjdivap  11162  cnrecnv  11163  cvg1nlemcau  11237  cvg1nlemres  11238  absval  11254  rennim  11255  sqrtdiv  11295  sqrtmsq  11298  absneg  11303  abscj  11305  absval2  11310  absreim  11321  absmul  11322  absdivap  11323  absid  11324  absre  11330  absexp  11332  absexpzap  11333  absimle  11337  abssub  11354  abs3dif  11358  abs2dif  11359  abs2dif2  11360  recan  11362  cau3lem  11367  max0addsup  11472  minabs  11489  bdtrilem  11492  clim  11534  clim2  11536  clim0  11538  clim0c  11539  climi0  11542  climconst  11543  climshftlemg  11555  climcn1  11561  climcn2  11562  addcn2  11563  subcn2  11564  mulcn2  11565  reccn2ap  11566  cjcn2  11569  recn2  11570  imcn2  11571  iser3shft  11599  climcau  11600  climcvg1nlem  11602  climcvg1n  11603  serf0  11605  summodclem3  11633  summodclem2a  11634  summodc  11636  fsumf1o  11643  sumsnf  11662  fsumm1  11669  fsumcnv  11690  fsumabs  11718  fsumrelem  11724  iserabs  11728  hash2iun1dif1  11733  isumshft  11743  isumsplit  11744  expcnvap0  11755  expcnv  11757  cvgratnnlemseq  11779  cvgratnnlemrate  11783  cvgratz  11785  mertenslemub  11787  mertenslemi1  11788  mertenslem2  11789  mertensabs  11790  prodmodclem3  11828  fprodf1o  11841  prodsnf  11845  fprodm1  11851  fprodabs  11869  fprodcnv  11878  efcllemp  11911  efcj  11926  efaddlem  11927  efcan  11929  efsub  11934  efexp  11935  efzval  11936  efgt0  11937  eftlub  11943  efltim  11951  sinval  11955  cosval  11956  tanval3ap  11967  resinval  11968  recosval  11969  resin4p  11971  recos4p  11972  sinneg  11979  cosneg  11980  efmival  11986  efeul  11987  sinadd  11989  cosadd  11990  sinsub  11993  cossub  11994  addsin  11995  subsin  11996  addcos  11999  subcos  12000  sincossq  12001  sin2t  12002  cos2t  12003  sin01bnd  12010  cos01bnd  12011  sin02gt0  12017  cos12dec  12021  absefi  12022  absef  12023  absefib  12024  efieq1re  12025  demoivre  12026  demoivreALT  12027  flodddiv4  12189  bitsval  12196  bits0  12201  bitsp1  12204  bitsp1e  12205  bitsp1o  12206  bitsmod  12209  nninfctlemfo  12303  alginv  12311  algcvg  12312  eucalgval  12318  eucalginv  12320  eucalglt  12321  eucalgcvga  12322  eucalg  12323  lcmgcd  12342  lcm1  12345  sqpweven  12439  2sqpwodd  12440  sqne2sq  12441  qnumval  12449  qdenval  12450  qden1elz  12469  nn0sqrtelqelz  12470  phival  12477  dfphi2  12484  phiprmpw  12486  phiprm  12487  eulerthlemth  12496  hashgcdeq  12504  phisum  12505  pythagtriplem6  12535  pythagtriplem7  12536  pythagtriplem12  12540  pythagtriplem14  12542  fldivp1  12613  4sqlem11  12666  ennnfonelemg  12716  ennnfonelemp1  12719  ennnfonelemkh  12725  ennnfonelemhf1o  12726  ennnfonelemnn0  12735  ctinfomlemom  12740  ctiunctlemu1st  12747  ctiunctlemu2nd  12748  ctiunctlemudc  12750  ctiunctlemfo  12752  isstruct2im  12784  isstruct2r  12785  setsslid  12825  ressbasd  12841  resseqnbasd  12847  ressplusgd  12903  ptex  13038  prdsex  13043  prdsval  13047  prdsbas3  13061  pwsval  13065  pwsbas  13066  pwsplusgval  13069  pwsmulrval  13070  imasex  13079  imasival  13080  f1ocpbl  13085  f1ovscpbl  13086  imasaddvallemg  13089  qusval  13097  fvprif  13117  xpsff1o  13123  igsumvalx  13163  gsumprval  13173  pws0g  13225  imasmnd  13227  ismhm  13235  mhmpropd  13240  mhmlin  13241  mhmf1o  13244  resmhm  13261  mhmco  13264  gsumwmhm  13272  grpinvsub  13356  pwsinvg  13386  imasgrp2  13388  imasgrp  13389  mhmlem  13392  mhmid  13393  mhmmnd  13394  ghmgrp  13396  mulgfvalg  13399  mulgval  13400  mulgnegnn  13410  mulgneg  13418  mulgnegneg  13419  mulgm1  13420  mulginvcom  13425  mulgz  13428  mulgnndir  13429  mulgdir  13432  mulgass  13437  mhmmulg  13441  subgmulg  13466  isnsg  13480  eqgfval  13500  ghmlin  13526  ghmid  13527  ghminv  13528  ghmsub  13529  ghmmulg  13534  resghm  13538  ghmeql  13545  ablsub2inv  13589  ghmcmn  13605  invghm  13607  imasabl  13614  gsumfzreidx  13615  gsumfzmhm  13621  mgpplusgg  13628  mgpbasg  13630  mgpscag  13631  mgptsetg  13632  mgpdsg  13634  rngm2neg  13653  imasrng  13660  isring  13704  ringm2neg  13759  imasring  13768  opprmulfvalg  13774  opprsllem  13778  isunitd  13810  opprunitd  13814  invrfvald  13826  rdivmuldivd  13848  rhmmul  13868  isrhm2d  13869  rhm1  13871  rhmdvdsr  13879  rhmopp  13880  rhmunitinv  13882  islmod  13995  islmodd  13997  scaffvalg  14010  lmodpropd  14053  lsssetm  14060  islssmd  14063  lssats2  14118  lspsnneg  14124  lspsnsub  14125  lspun0  14129  lmodindp1  14132  sralemg  14142  srascag  14146  sravscag  14147  sraipg  14148  rlmscabas  14164  ixpsnbasval  14170  2idlval  14206  2idlvalg  14207  mulgrhm2  14314  zlmlemg  14332  zlmsca  14336  zlmvscag  14337  znval  14340  znle  14341  znbaslemnn  14343  znidomb  14362  psrval  14370  psrbasg  14378  psrplusgg  14382  mplvalcoe  14394  mplsubgfileminv  14404  mpl0fi  14406  mplnegfi  14409  istps  14446  tpspropd  14450  eltpsg  14454  txvalex  14668  txval  14669  txbasval  14681  upxp  14686  uptx  14688  txrest  14690  cnmpt11  14697  cnmpt21  14705  hmeontr  14727  txhmeo  14733  psmetxrge0  14746  xmetunirn  14772  mopnval  14856  mopntopon  14857  isxms  14865  isxms2  14866  isms  14867  msrtri  14890  xmspropd  14891  mspropd  14892  setsmsbasg  14893  setsmsdsg  14894  setsmstsetg  14895  comet  14913  metcnpi  14929  metcnpi2  14930  cnbl0  14948  cnblcld  14949  resubmet  14970  mpomulcn  14980  elcncf  14987  cncfi  14992  rescncf  14995  mulc1cncf  15003  cncfco  15005  cncfmptid  15011  addccncf  15014  cdivcncfap  15018  negcncf  15019  mulcncflem  15021  ivthinclemlopn  15050  ivthinclemuopn  15052  limccl  15073  ellimc3apf  15074  limcimolemlt  15078  cnplimclemle  15082  limccnpcntop  15089  reldvg  15093  dvfvalap  15095  dveflem  15140  dvef  15141  plymullem1  15162  plycjlemc  15174  plycj  15175  plyrecj  15177  plyreres  15178  sin0pilem1  15195  ef2kpi  15220  sinperlem  15222  sin2kpi  15225  cos2kpi  15226  sin2pim  15227  cos2pim  15228  ptolemy  15238  sincosq2sgn  15241  sincosq3sgn  15242  sincosq4sgn  15243  sinq12gt0  15244  tangtx  15252  sincosq1eq  15253  abssinper  15260  sinkpi  15261  coskpi  15262  cosq34lt1  15264  relogeftb  15279  relogoprlem  15282  relogexp  15286  rpcxpef  15308  logcxp  15311  1cxp  15314  ecxp  15315  rpcxpadd  15319  rpmulcxp  15323  cxpmul  15326  abscxp  15329  logsqrt  15337  rpabscxpbnd  15354  rpcxplogb  15378  lgsval  15423  lgsval2lem  15429  lgsval4a  15441  lgsdi  15456  lgseisenlem3  15491  lgseisenlem4  15492  lgsquadlem1  15496  lgsquadlem2  15497  lgsquadlem3  15498  2lgslem1  15510  2lgslem3a  15512  2lgslem3b  15513  2lgslem3c  15514  2lgslem3d  15515  nnsf  15875  peano4nninf  15876  peano3nninf  15877  nninfalllem1  15878  nninfall  15879  nninfsellemdc  15880  nninfsellemeq  15884  nninfsellemqall  15885  nninfsellemeqinf  15886  nninfsel  15887  nnnninfex  15892  exmidsbthr  15895  qdencn  15899  refeq  15900  isomninnlem  15902  apdifflemr  15919  apdiff  15920  ismkvnnlem  15924  nconstwlpolem  15937