Theorem fveq2d 5519

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

Syntax hints:   → wi 4   = wceq 1353  ‘cfv 5216

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 709  ax-5 1447  ax-7 1448  ax-gen 1449  ax-ie1 1493  ax-ie2 1494  ax-8 1504  ax-10 1505  ax-11 1506  ax-i12 1507  ax-bndl 1509  ax-4 1510  ax-17 1526  ax-i9 1530  ax-ial 1534  ax-i5r 1535  ax-ext 2159

This theorem depends on definitions:  df-bi 117  df-3an 980  df-tru 1356  df-nf 1461  df-sb 1763  df-clab 2164  df-cleq 2170  df-clel 2173  df-nfc 2308  df-rex 2461  df-v 2739  df-un 3133  df-sn 3598  df-pr 3599  df-op 3601  df-uni 3810  df-br 4004  df-iota 5178  df-fv 5224

This theorem is referenced by:  2fveq3  5520  fveq12d  5522  fveqeq2d  5523  csbfvg  5553  fvmptdf  5603  fvmptt  5607  fcof1  5783  oveq1  5881  oveq2  5882  fvoveq1d  5896  caofinvl  6104  op1stg  6150  op2ndg  6151  ot1stg  6152  ot2ndg  6153  eloprabi  6196  1stconst  6221  algrflemg  6230  tfrlem1  6308  tfrlem3ag  6309  tfrlem3a  6310  tfrlem9  6319  tfr0dm  6322  tfrlemisucaccv  6325  tfrlemiubacc  6330  tfrlemiex  6331  tfrlemi1  6332  tfr1onlem3ag  6337  tfr1onlemsucaccv  6341  tfr1onlemubacc  6346  tfr1onlemex  6347  tfr1onlemaccex  6348  tfrcllemsucaccv  6354  tfrcllembxssdm  6356  tfrcllemubacc  6359  tfrcllemex  6360  tfrcllemaccex  6361  tfrcllemres  6362  tfrcldm  6363  rdgivallem  6381  rdgival  6382  rdgss  6383  rdgisuc1  6384  rdgon  6386  rdg0  6387  frec0g  6397  frecabcl  6399  freccllem  6402  frecfcllem  6404  frecsuclem  6406  frecsuc  6407  frecrdg  6408  oav2  6463  omv2  6465  xpdom2  6830  xpmapenlem  6848  xpmapen  6849  ac6sfi  6897  1stinl  7072  2ndinl  7073  1stinr  7074  2ndinr  7075  updjudhcoinlf  7078  updjudhcoinrg  7079  caseinl  7089  caseinr  7090  omp1eomlem  7092  omp1eom  7093  difinfsn  7098  ctmlemr  7106  ctm  7107  ctssdclemn0  7108  ctssdccl  7109  nnnninfeq  7125  nnnninfeq2  7126  enomnilem  7135  enmkvlem  7158  enwomnilem  7166  exmidfodomrlemeldju  7197  exmidfodomrlemreseldju  7198  exmidfodomrlemr  7200  exmidfodomrlemrALT  7201  exmidaclem  7206  cc2  7265  cc3  7266  ltdfpr  7504  genpelvl  7510  genpelvu  7511  recexpr  7636  cauappcvgprlem1  7657  caucvgprlemnkj  7664  caucvgprlemnbj  7665  caucvgprlemm  7666  caucvgprlemdisj  7672  caucvgprlemloc  7673  caucvgprlemcl  7674  caucvgprlemladdfu  7675  caucvgprlemladdrl  7676  caucvgprlem1  7677  caucvgprlem2  7678  caucvgpr  7680  caucvgprprlemell  7683  caucvgprprlemelu  7684  caucvgprprlemcbv  7685  caucvgprprlemval  7686  caucvgprprlemnkeqj  7688  caucvgprprlemmu  7693  caucvgprprlemopl  7695  caucvgprprlemlol  7696  caucvgprprlemopu  7697  caucvgprprlemloc  7701  caucvgprprlemclphr  7703  caucvgprprlemexbt  7704  caucvgprprlem1  7707  caucvgprprlem2  7708  caucvgsr  7800  axcaucvglemval  7895  axcaucvglemres  7897  fv0p1e1  9033  uzin  9559  cnref1o  9649  fzsuc2  10078  fseq1m1p1  10094  fzoss2  10171  elfzonlteqm1  10209  divfl0  10295  flqzadd  10297  fldiv4p1lem1div2  10304  ceilqval  10305  flqdiv  10320  modqval  10323  modqfrac  10336  modqmulnn  10341  modqid  10348  modqcyc  10358  modqdi  10391  frec2uzuzd  10401  frec2uzrdg  10408  frecuzrdgrcl  10409  frecuzrdgtcl  10411  frecuzrdgsuc  10413  frecuzrdgrclt  10414  frecuzrdgg  10415  frecuzrdgfunlem  10418  frecuzrdgsuctlem  10422  iseqovex  10455  iseqvalcbv  10456  seq3val  10457  seqvalcd  10458  seq3m1  10467  seq3shft2  10472  monoord  10475  monoord2  10476  iseqf1olemqval  10486  iseqf1olemab  10488  iseqf1olemqk  10493  iseqf1olemjpcl  10494  iseqf1olemqpcl  10495  iseqf1olemfvp  10496  seq3f1olemqsumkj  10497  seq3f1olemqsumk  10498  seq3f1olemqsum  10499  seq3f1olemp  10501  seq3f1oleml  10502  seq3homo  10509  exp3val  10521  expnegap0  10527  facnn2  10713  facwordi  10719  faclbnd6  10723  bcval  10728  bccmpl  10733  bcn0  10734  bcm1k  10739  bcp1n  10740  bcn2  10743  hashinfom  10757  hashennn  10759  hashsng  10777  omgadd  10781  hashprg  10787  fihashssdif  10797  hashdifpr  10799  hashfzo  10801  hashfzp1  10803  hashxp  10805  zfz1isolemiso  10818  zfz1iso  10820  shftval2  10834  shftval3  10835  shftval4  10836  shftval5  10837  seq3shft  10846  imval  10858  imre  10859  reim  10860  crim  10866  reim0  10869  mulreap  10872  recj  10875  reneg  10876  readd  10877  resub  10878  remullem  10879  redivap  10882  imcj  10883  imneg  10884  imadd  10885  imsub  10886  imdivap  10889  cjsub  10900  cjexp  10901  cjreim2  10912  cjap  10914  cjdivap  10917  cnrecnv  10918  cvg1nlemcau  10992  cvg1nlemres  10993  absval  11009  rennim  11010  sqrtdiv  11050  sqrtmsq  11053  absneg  11058  abscj  11060  absval2  11065  absreim  11076  absmul  11077  absdivap  11078  absid  11079  absre  11085  absexp  11087  absexpzap  11088  absimle  11092  abssub  11109  abs3dif  11113  abs2dif  11114  abs2dif2  11115  recan  11117  cau3lem  11122  max0addsup  11227  minabs  11243  bdtrilem  11246  clim  11288  clim2  11290  clim0  11292  clim0c  11293  climi0  11296  climconst  11297  climshftlemg  11309  climcn1  11315  climcn2  11316  addcn2  11317  subcn2  11318  mulcn2  11319  reccn2ap  11320  cjcn2  11323  recn2  11324  imcn2  11325  iser3shft  11353  climcau  11354  climcvg1nlem  11356  climcvg1n  11357  serf0  11359  summodclem3  11387  summodclem2a  11388  summodc  11390  fsumf1o  11397  sumsnf  11416  fsumm1  11423  fsumcnv  11444  fsumabs  11472  fsumrelem  11478  iserabs  11482  hash2iun1dif1  11487  isumshft  11497  isumsplit  11498  expcnvap0  11509  expcnv  11511  cvgratnnlemseq  11533  cvgratnnlemrate  11537  cvgratz  11539  mertenslemub  11541  mertenslemi1  11542  mertenslem2  11543  mertensabs  11544  prodmodclem3  11582  fprodf1o  11595  prodsnf  11599  fprodm1  11605  fprodabs  11623  fprodcnv  11632  efcllemp  11665  efcj  11680  efaddlem  11681  efcan  11683  efsub  11688  efexp  11689  efzval  11690  efgt0  11691  eftlub  11697  efltim  11705  sinval  11709  cosval  11710  tanval3ap  11721  resinval  11722  recosval  11723  resin4p  11725  recos4p  11726  sinneg  11733  cosneg  11734  efmival  11740  efeul  11741  sinadd  11743  cosadd  11744  sinsub  11747  cossub  11748  addsin  11749  subsin  11750  addcos  11753  subcos  11754  sincossq  11755  sin2t  11756  cos2t  11757  sin01bnd  11764  cos01bnd  11765  sin02gt0  11770  cos12dec  11774  absefi  11775  absef  11776  absefib  11777  efieq1re  11778  demoivre  11779  demoivreALT  11780  flodddiv4  11938  alginv  12046  algcvg  12047  eucalgval  12053  eucalginv  12055  eucalglt  12056  eucalgcvga  12057  eucalg  12058  lcmgcd  12077  lcm1  12080  sqpweven  12174  2sqpwodd  12175  sqne2sq  12176  qnumval  12184  qdenval  12185  qden1elz  12204  nn0sqrtelqelz  12205  phival  12212  dfphi2  12219  phiprmpw  12221  phiprm  12222  eulerthlemth  12231  hashgcdeq  12238  phisum  12239  pythagtriplem6  12269  pythagtriplem7  12270  pythagtriplem12  12274  pythagtriplem14  12276  fldivp1  12345  ennnfonelemg  12403  ennnfonelemp1  12406  ennnfonelemkh  12412  ennnfonelemhf1o  12413  ennnfonelemnn0  12422  ctinfomlemom  12427  ctiunctlemu1st  12434  ctiunctlemu2nd  12435  ctiunctlemudc  12437  ctiunctlemfo  12439  isstruct2im  12471  isstruct2r  12472  strslfv3  12507  setsslid  12512  ressbasd  12526  resseqnbasd  12531  ressplusgd  12586  ptex  12712  prdsex  12717  imasex  12725  imasival  12726  f1ocpbl  12731  f1ovscpbl  12732  imasaddvallemg  12735  qusval  12743  fvprif  12761  xpsff1o  12767  ismhm  12852  mhmpropd  12856  mhmlin  12857  mhmf1o  12860  mhmco  12873  grpinvsub  12951  mhmlem  12977  mhmid  12978  mhmmnd  12979  ghmgrp  12981  mulgfvalg  12984  mulgval  12985  mulgnegnn  12992  mulgneg  13000  mulgnegneg  13001  mulgm1  13002  mulginvcom  13006  mulgz  13009  mulgnndir  13010  mulgdir  13013  mulgass  13018  mhmmulg  13022  subgmulg  13046  isnsg  13060  eqgfval  13079  ablsub2inv  13112  mgpplusgg  13132  mgpbasg  13134  mgpscag  13135  mgptsetg  13136  mgpdsg  13138  isring  13181  ringm2neg  13230  opprmulfvalg  13240  opprsllem  13244  isunitd  13273  opprunitd  13277  invrfvald  13289  rdivmuldivd  13311  istps  13468  tpspropd  13472  eltpsg  13476  txvalex  13690  txval  13691  txbasval  13703  upxp  13708  uptx  13710  txrest  13712  cnmpt11  13719  cnmpt21  13727  hmeontr  13749  txhmeo  13755  psmetxrge0  13768  xmetunirn  13794  mopnval  13878  mopntopon  13879  isxms  13887  isxms2  13888  isms  13889  msrtri  13912  xmspropd  13913  mspropd  13914  setsmsbasg  13915  setsmsdsg  13916  setsmstsetg  13917  comet  13935  metcnpi  13951  metcnpi2  13952  cnbl0  13970  cnblcld  13971  resubmet  13984  elcncf  13996  cncfi  14001  rescncf  14004  mulc1cncf  14012  cncfco  14014  cncfmptid  14019  addccncf  14022  cdivcncfap  14023  negcncf  14024  mulcncflem  14026  ivthinclemlopn  14050  ivthinclemuopn  14052  limccl  14064  ellimc3apf  14065  limcimolemlt  14069  cnplimclemle  14073  limccnpcntop  14080  reldvg  14084  dvfvalap  14086  dveflem  14123  dvef  14124  sin0pilem1  14138  ef2kpi  14163  sinperlem  14165  sin2kpi  14168  cos2kpi  14169  sin2pim  14170  cos2pim  14171  ptolemy  14181  sincosq2sgn  14184  sincosq3sgn  14185  sincosq4sgn  14186  sinq12gt0  14187  tangtx  14195  sincosq1eq  14196  abssinper  14203  sinkpi  14204  coskpi  14205  cosq34lt1  14207  relogeftb  14222  relogoprlem  14225  relogexp  14229  rpcxpef  14251  logcxp  14254  1cxp  14257  ecxp  14258  rpcxpadd  14262  rpmulcxp  14266  cxpmul  14269  abscxp  14271  logsqrt  14279  rpabscxpbnd  14295  rpcxplogb  14318  lgsval  14341  lgsval2lem  14347  lgsval4a  14359  lgsdi  14374  nnsf  14690  peano4nninf  14691  peano3nninf  14692  nninfalllem1  14693  nninfall  14694  nninfsellemdc  14695  nninfsellemeq  14699  nninfsellemqall  14700  nninfsellemeqinf  14701  nninfsel  14702  exmidsbthr  14707  qdencn  14711  refeq  14712  isomninnlem  14714  apdifflemr  14731  apdiff  14732  ismkvnnlem  14736  nconstwlpolem  14748