Theorem fveq2d 5562

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 5558	. 2 ⊢ (𝐴 = 𝐵 → (𝐹‘𝐴) = (𝐹‘𝐵))
3	1, 2	syl 14	1 ⊢ (𝜑 → (𝐹‘𝐴) = (𝐹‘𝐵))

Syntax hints:   → wi 4   = wceq 1364  ‘cfv 5258

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 1461  ax-7 1462  ax-gen 1463  ax-ie1 1507  ax-ie2 1508  ax-8 1518  ax-10 1519  ax-11 1520  ax-i12 1521  ax-bndl 1523  ax-4 1524  ax-17 1540  ax-i9 1544  ax-ial 1548  ax-i5r 1549  ax-ext 2178

This theorem depends on definitions:  df-bi 117  df-3an 982  df-tru 1367  df-nf 1475  df-sb 1777  df-clab 2183  df-cleq 2189  df-clel 2192  df-nfc 2328  df-rex 2481  df-v 2765  df-un 3161  df-sn 3628  df-pr 3629  df-op 3631  df-uni 3840  df-br 4034  df-iota 5219  df-fv 5266

This theorem is referenced by:  2fveq3  5563  fveq12d  5565  fveqeq2d  5566  csbfvg  5598  fvmptdf  5649  fvmptt  5653  fcof1  5830  oveq1  5929  oveq2  5930  fvoveq1d  5944  caofinvl  6160  op1stg  6208  op2ndg  6209  ot1stg  6210  ot2ndg  6211  eloprabi  6254  1stconst  6279  algrflemg  6288  tfrlem1  6366  tfrlem3ag  6367  tfrlem3a  6368  tfrlem9  6377  tfr0dm  6380  tfrlemisucaccv  6383  tfrlemiubacc  6388  tfrlemiex  6389  tfrlemi1  6390  tfr1onlem3ag  6395  tfr1onlemsucaccv  6399  tfr1onlemubacc  6404  tfr1onlemex  6405  tfr1onlemaccex  6406  tfrcllemsucaccv  6412  tfrcllembxssdm  6414  tfrcllemubacc  6417  tfrcllemex  6418  tfrcllemaccex  6419  tfrcllemres  6420  tfrcldm  6421  rdgivallem  6439  rdgival  6440  rdgss  6441  rdgisuc1  6442  rdgon  6444  rdg0  6445  frec0g  6455  frecabcl  6457  freccllem  6460  frecfcllem  6462  frecsuclem  6464  frecsuc  6465  frecrdg  6466  oav2  6521  omv2  6523  xpdom2  6890  xpmapenlem  6910  xpmapen  6911  ac6sfi  6959  1stinl  7140  2ndinl  7141  1stinr  7142  2ndinr  7143  updjudhcoinlf  7146  updjudhcoinrg  7147  caseinl  7157  caseinr  7158  omp1eomlem  7160  omp1eom  7161  difinfsn  7166  ctmlemr  7174  ctm  7175  ctssdclemn0  7176  ctssdccl  7177  nninfninc  7189  nnnninfeq  7194  nnnninfeq2  7195  enomnilem  7204  enmkvlem  7227  enwomnilem  7235  exmidfodomrlemeldju  7266  exmidfodomrlemreseldju  7267  exmidfodomrlemr  7269  exmidfodomrlemrALT  7270  exmidaclem  7275  cc2  7334  cc3  7335  ltdfpr  7573  genpelvl  7579  genpelvu  7580  recexpr  7705  cauappcvgprlem1  7726  caucvgprlemnkj  7733  caucvgprlemnbj  7734  caucvgprlemm  7735  caucvgprlemdisj  7741  caucvgprlemloc  7742  caucvgprlemcl  7743  caucvgprlemladdfu  7744  caucvgprlemladdrl  7745  caucvgprlem1  7746  caucvgprlem2  7747  caucvgpr  7749  caucvgprprlemell  7752  caucvgprprlemelu  7753  caucvgprprlemcbv  7754  caucvgprprlemval  7755  caucvgprprlemnkeqj  7757  caucvgprprlemmu  7762  caucvgprprlemopl  7764  caucvgprprlemlol  7765  caucvgprprlemopu  7766  caucvgprprlemloc  7770  caucvgprprlemclphr  7772  caucvgprprlemexbt  7773  caucvgprprlem1  7776  caucvgprprlem2  7777  caucvgsr  7869  axcaucvglemval  7964  axcaucvglemres  7966  fv0p1e1  9105  uzin  9634  cnref1o  9725  fzsuc2  10154  fseq1m1p1  10170  fzoss2  10248  elfzonlteqm1  10286  divfl0  10386  flqzadd  10388  fldiv4p1lem1div2  10395  ceilqval  10398  flqdiv  10413  modqval  10416  modqfrac  10429  modqmulnn  10434  modqid  10441  modqcyc  10451  modqdi  10484  frec2uzuzd  10494  frec2uzrdg  10501  frecuzrdgrcl  10502  frecuzrdgtcl  10504  frecuzrdgsuc  10506  frecuzrdgrclt  10507  frecuzrdgg  10508  frecuzrdgfunlem  10511  frecuzrdgsuctlem  10515  iseqovex  10550  iseqvalcbv  10551  seq3val  10552  seqvalcd  10553  seq3m1  10565  seq3shft2  10573  seqshft2g  10574  monoord  10577  monoord2  10578  iseqf1olemqval  10592  iseqf1olemab  10594  iseqf1olemqk  10599  iseqf1olemjpcl  10600  iseqf1olemqpcl  10601  iseqf1olemfvp  10602  seq3f1olemqsumkj  10603  seq3f1olemqsumk  10604  seq3f1olemqsum  10605  seq3f1olemp  10607  seq3f1oleml  10608  seqf1oglem1  10611  seqf1oglem2  10612  seqf1og  10613  seq3homo  10619  seqhomog  10622  exp3val  10633  expnegap0  10639  facnn2  10826  facwordi  10832  faclbnd6  10836  bcval  10841  bccmpl  10846  bcn0  10847  bcm1k  10852  bcp1n  10853  bcn2  10856  hashinfom  10870  hashennn  10872  hashsng  10890  omgadd  10894  hashprg  10900  fihashssdif  10910  hashdifpr  10912  hashfzo  10914  hashfzp1  10916  hashxp  10918  zfz1isolemiso  10931  zfz1iso  10933  shftval2  10991  shftval3  10992  shftval4  10993  shftval5  10994  seq3shft  11003  imval  11015  imre  11016  reim  11017  crim  11023  reim0  11026  mulreap  11029  recj  11032  reneg  11033  readd  11034  resub  11035  remullem  11036  redivap  11039  imcj  11040  imneg  11041  imadd  11042  imsub  11043  imdivap  11046  cjsub  11057  cjexp  11058  cjreim2  11069  cjap  11071  cjdivap  11074  cnrecnv  11075  cvg1nlemcau  11149  cvg1nlemres  11150  absval  11166  rennim  11167  sqrtdiv  11207  sqrtmsq  11210  absneg  11215  abscj  11217  absval2  11222  absreim  11233  absmul  11234  absdivap  11235  absid  11236  absre  11242  absexp  11244  absexpzap  11245  absimle  11249  abssub  11266  abs3dif  11270  abs2dif  11271  abs2dif2  11272  recan  11274  cau3lem  11279  max0addsup  11384  minabs  11401  bdtrilem  11404  clim  11446  clim2  11448  clim0  11450  clim0c  11451  climi0  11454  climconst  11455  climshftlemg  11467  climcn1  11473  climcn2  11474  addcn2  11475  subcn2  11476  mulcn2  11477  reccn2ap  11478  cjcn2  11481  recn2  11482  imcn2  11483  iser3shft  11511  climcau  11512  climcvg1nlem  11514  climcvg1n  11515  serf0  11517  summodclem3  11545  summodclem2a  11546  summodc  11548  fsumf1o  11555  sumsnf  11574  fsumm1  11581  fsumcnv  11602  fsumabs  11630  fsumrelem  11636  iserabs  11640  hash2iun1dif1  11645  isumshft  11655  isumsplit  11656  expcnvap0  11667  expcnv  11669  cvgratnnlemseq  11691  cvgratnnlemrate  11695  cvgratz  11697  mertenslemub  11699  mertenslemi1  11700  mertenslem2  11701  mertensabs  11702  prodmodclem3  11740  fprodf1o  11753  prodsnf  11757  fprodm1  11763  fprodabs  11781  fprodcnv  11790  efcllemp  11823  efcj  11838  efaddlem  11839  efcan  11841  efsub  11846  efexp  11847  efzval  11848  efgt0  11849  eftlub  11855  efltim  11863  sinval  11867  cosval  11868  tanval3ap  11879  resinval  11880  recosval  11881  resin4p  11883  recos4p  11884  sinneg  11891  cosneg  11892  efmival  11898  efeul  11899  sinadd  11901  cosadd  11902  sinsub  11905  cossub  11906  addsin  11907  subsin  11908  addcos  11911  subcos  11912  sincossq  11913  sin2t  11914  cos2t  11915  sin01bnd  11922  cos01bnd  11923  sin02gt0  11929  cos12dec  11933  absefi  11934  absef  11935  absefib  11936  efieq1re  11937  demoivre  11938  demoivreALT  11939  flodddiv4  12101  bitsval  12108  bits0  12112  bitsp1  12115  bitsp1e  12116  bitsp1o  12117  nninfctlemfo  12207  alginv  12215  algcvg  12216  eucalgval  12222  eucalginv  12224  eucalglt  12225  eucalgcvga  12226  eucalg  12227  lcmgcd  12246  lcm1  12249  sqpweven  12343  2sqpwodd  12344  sqne2sq  12345  qnumval  12353  qdenval  12354  qden1elz  12373  nn0sqrtelqelz  12374  phival  12381  dfphi2  12388  phiprmpw  12390  phiprm  12391  eulerthlemth  12400  hashgcdeq  12408  phisum  12409  pythagtriplem6  12439  pythagtriplem7  12440  pythagtriplem12  12444  pythagtriplem14  12446  fldivp1  12517  4sqlem11  12570  ennnfonelemg  12620  ennnfonelemp1  12623  ennnfonelemkh  12629  ennnfonelemhf1o  12630  ennnfonelemnn0  12639  ctinfomlemom  12644  ctiunctlemu1st  12651  ctiunctlemu2nd  12652  ctiunctlemudc  12654  ctiunctlemfo  12656  isstruct2im  12688  isstruct2r  12689  strslfv3  12724  setsslid  12729  ressbasd  12745  resseqnbasd  12751  ressplusgd  12806  ptex  12935  prdsex  12940  imasex  12948  imasival  12949  f1ocpbl  12954  f1ovscpbl  12955  imasaddvallemg  12958  qusval  12966  fvprif  12986  xpsff1o  12992  igsumvalx  13032  gsumprval  13042  ismhm  13093  mhmpropd  13098  mhmlin  13099  mhmf1o  13102  resmhm  13119  mhmco  13122  gsumwmhm  13130  grpinvsub  13214  imasgrp2  13240  imasgrp  13241  mhmlem  13244  mhmid  13245  mhmmnd  13246  ghmgrp  13248  mulgfvalg  13251  mulgval  13252  mulgnegnn  13262  mulgneg  13270  mulgnegneg  13271  mulgm1  13272  mulginvcom  13277  mulgz  13280  mulgnndir  13281  mulgdir  13284  mulgass  13289  mhmmulg  13293  subgmulg  13318  isnsg  13332  eqgfval  13352  ghmlin  13378  ghmid  13379  ghminv  13380  ghmsub  13381  ghmmulg  13386  resghm  13390  ghmeql  13397  ablsub2inv  13441  ghmcmn  13457  invghm  13459  imasabl  13466  gsumfzreidx  13467  gsumfzmhm  13473  mgpplusgg  13480  mgpbasg  13482  mgpscag  13483  mgptsetg  13484  mgpdsg  13486  rngm2neg  13505  imasrng  13512  isring  13556  ringm2neg  13611  imasring  13620  opprmulfvalg  13626  opprsllem  13630  isunitd  13662  opprunitd  13666  invrfvald  13678  rdivmuldivd  13700  rhmmul  13720  isrhm2d  13721  rhm1  13723  rhmdvdsr  13731  rhmopp  13732  rhmunitinv  13734  islmod  13847  islmodd  13849  scaffvalg  13862  lmodpropd  13905  lsssetm  13912  islssmd  13915  lssats2  13970  lspsnneg  13976  lspsnsub  13977  lspun0  13981  lmodindp1  13984  sralemg  13994  srascag  13998  sravscag  13999  sraipg  14000  rlmscabas  14016  ixpsnbasval  14022  2idlval  14058  2idlvalg  14059  mulgrhm2  14166  zlmlemg  14184  zlmsca  14188  zlmvscag  14189  znval  14192  znle  14193  znbaslemnn  14195  znidomb  14214  psrval  14220  psrbasg  14227  psrplusgg  14230  istps  14268  tpspropd  14272  eltpsg  14276  txvalex  14490  txval  14491  txbasval  14503  upxp  14508  uptx  14510  txrest  14512  cnmpt11  14519  cnmpt21  14527  hmeontr  14549  txhmeo  14555  psmetxrge0  14568  xmetunirn  14594  mopnval  14678  mopntopon  14679  isxms  14687  isxms2  14688  isms  14689  msrtri  14712  xmspropd  14713  mspropd  14714  setsmsbasg  14715  setsmsdsg  14716  setsmstsetg  14717  comet  14735  metcnpi  14751  metcnpi2  14752  cnbl0  14770  cnblcld  14771  resubmet  14792  mpomulcn  14802  elcncf  14809  cncfi  14814  rescncf  14817  mulc1cncf  14825  cncfco  14827  cncfmptid  14833  addccncf  14836  cdivcncfap  14840  negcncf  14841  mulcncflem  14843  ivthinclemlopn  14872  ivthinclemuopn  14874  limccl  14895  ellimc3apf  14896  limcimolemlt  14900  cnplimclemle  14904  limccnpcntop  14911  reldvg  14915  dvfvalap  14917  dveflem  14962  dvef  14963  plymullem1  14984  plycjlemc  14996  plycj  14997  plyrecj  14999  plyreres  15000  sin0pilem1  15017  ef2kpi  15042  sinperlem  15044  sin2kpi  15047  cos2kpi  15048  sin2pim  15049  cos2pim  15050  ptolemy  15060  sincosq2sgn  15063  sincosq3sgn  15064  sincosq4sgn  15065  sinq12gt0  15066  tangtx  15074  sincosq1eq  15075  abssinper  15082  sinkpi  15083  coskpi  15084  cosq34lt1  15086  relogeftb  15101  relogoprlem  15104  relogexp  15108  rpcxpef  15130  logcxp  15133  1cxp  15136  ecxp  15137  rpcxpadd  15141  rpmulcxp  15145  cxpmul  15148  abscxp  15151  logsqrt  15159  rpabscxpbnd  15176  rpcxplogb  15200  lgsval  15245  lgsval2lem  15251  lgsval4a  15263  lgsdi  15278  lgseisenlem3  15313  lgseisenlem4  15314  lgsquadlem1  15318  lgsquadlem2  15319  lgsquadlem3  15320  2lgslem1  15332  2lgslem3a  15334  2lgslem3b  15335  2lgslem3c  15336  2lgslem3d  15337  nnsf  15649  peano4nninf  15650  peano3nninf  15651  nninfalllem1  15652  nninfall  15653  nninfsellemdc  15654  nninfsellemeq  15658  nninfsellemqall  15659  nninfsellemeqinf  15660  nninfsel  15661  exmidsbthr  15667  qdencn  15671  refeq  15672  isomninnlem  15674  apdifflemr  15691  apdiff  15692  ismkvnnlem  15696  nconstwlpolem  15709