Theorem fveq2d 5520

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

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

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 2740  df-un 3134  df-sn 3599  df-pr 3600  df-op 3602  df-uni 3811  df-br 4005  df-iota 5179  df-fv 5225

This theorem is referenced by:  2fveq3  5521  fveq12d  5523  fveqeq2d  5524  csbfvg  5554  fvmptdf  5604  fvmptt  5608  fcof1  5784  oveq1  5882  oveq2  5883  fvoveq1d  5897  caofinvl  6105  op1stg  6151  op2ndg  6152  ot1stg  6153  ot2ndg  6154  eloprabi  6197  1stconst  6222  algrflemg  6231  tfrlem1  6309  tfrlem3ag  6310  tfrlem3a  6311  tfrlem9  6320  tfr0dm  6323  tfrlemisucaccv  6326  tfrlemiubacc  6331  tfrlemiex  6332  tfrlemi1  6333  tfr1onlem3ag  6338  tfr1onlemsucaccv  6342  tfr1onlemubacc  6347  tfr1onlemex  6348  tfr1onlemaccex  6349  tfrcllemsucaccv  6355  tfrcllembxssdm  6357  tfrcllemubacc  6360  tfrcllemex  6361  tfrcllemaccex  6362  tfrcllemres  6363  tfrcldm  6364  rdgivallem  6382  rdgival  6383  rdgss  6384  rdgisuc1  6385  rdgon  6387  rdg0  6388  frec0g  6398  frecabcl  6400  freccllem  6403  frecfcllem  6405  frecsuclem  6407  frecsuc  6408  frecrdg  6409  oav2  6464  omv2  6466  xpdom2  6831  xpmapenlem  6849  xpmapen  6850  ac6sfi  6898  1stinl  7073  2ndinl  7074  1stinr  7075  2ndinr  7076  updjudhcoinlf  7079  updjudhcoinrg  7080  caseinl  7090  caseinr  7091  omp1eomlem  7093  omp1eom  7094  difinfsn  7099  ctmlemr  7107  ctm  7108  ctssdclemn0  7109  ctssdccl  7110  nnnninfeq  7126  nnnninfeq2  7127  enomnilem  7136  enmkvlem  7159  enwomnilem  7167  exmidfodomrlemeldju  7198  exmidfodomrlemreseldju  7199  exmidfodomrlemr  7201  exmidfodomrlemrALT  7202  exmidaclem  7207  cc2  7266  cc3  7267  ltdfpr  7505  genpelvl  7511  genpelvu  7512  recexpr  7637  cauappcvgprlem1  7658  caucvgprlemnkj  7665  caucvgprlemnbj  7666  caucvgprlemm  7667  caucvgprlemdisj  7673  caucvgprlemloc  7674  caucvgprlemcl  7675  caucvgprlemladdfu  7676  caucvgprlemladdrl  7677  caucvgprlem1  7678  caucvgprlem2  7679  caucvgpr  7681  caucvgprprlemell  7684  caucvgprprlemelu  7685  caucvgprprlemcbv  7686  caucvgprprlemval  7687  caucvgprprlemnkeqj  7689  caucvgprprlemmu  7694  caucvgprprlemopl  7696  caucvgprprlemlol  7697  caucvgprprlemopu  7698  caucvgprprlemloc  7702  caucvgprprlemclphr  7704  caucvgprprlemexbt  7705  caucvgprprlem1  7708  caucvgprprlem2  7709  caucvgsr  7801  axcaucvglemval  7896  axcaucvglemres  7898  fv0p1e1  9034  uzin  9560  cnref1o  9650  fzsuc2  10079  fseq1m1p1  10095  fzoss2  10172  elfzonlteqm1  10210  divfl0  10296  flqzadd  10298  fldiv4p1lem1div2  10305  ceilqval  10306  flqdiv  10321  modqval  10324  modqfrac  10337  modqmulnn  10342  modqid  10349  modqcyc  10359  modqdi  10392  frec2uzuzd  10402  frec2uzrdg  10409  frecuzrdgrcl  10410  frecuzrdgtcl  10412  frecuzrdgsuc  10414  frecuzrdgrclt  10415  frecuzrdgg  10416  frecuzrdgfunlem  10419  frecuzrdgsuctlem  10423  iseqovex  10456  iseqvalcbv  10457  seq3val  10458  seqvalcd  10459  seq3m1  10468  seq3shft2  10473  monoord  10476  monoord2  10477  iseqf1olemqval  10487  iseqf1olemab  10489  iseqf1olemqk  10494  iseqf1olemjpcl  10495  iseqf1olemqpcl  10496  iseqf1olemfvp  10497  seq3f1olemqsumkj  10498  seq3f1olemqsumk  10499  seq3f1olemqsum  10500  seq3f1olemp  10502  seq3f1oleml  10503  seq3homo  10510  exp3val  10522  expnegap0  10528  facnn2  10714  facwordi  10720  faclbnd6  10724  bcval  10729  bccmpl  10734  bcn0  10735  bcm1k  10740  bcp1n  10741  bcn2  10744  hashinfom  10758  hashennn  10760  hashsng  10778  omgadd  10782  hashprg  10788  fihashssdif  10798  hashdifpr  10800  hashfzo  10802  hashfzp1  10804  hashxp  10806  zfz1isolemiso  10819  zfz1iso  10821  shftval2  10835  shftval3  10836  shftval4  10837  shftval5  10838  seq3shft  10847  imval  10859  imre  10860  reim  10861  crim  10867  reim0  10870  mulreap  10873  recj  10876  reneg  10877  readd  10878  resub  10879  remullem  10880  redivap  10883  imcj  10884  imneg  10885  imadd  10886  imsub  10887  imdivap  10890  cjsub  10901  cjexp  10902  cjreim2  10913  cjap  10915  cjdivap  10918  cnrecnv  10919  cvg1nlemcau  10993  cvg1nlemres  10994  absval  11010  rennim  11011  sqrtdiv  11051  sqrtmsq  11054  absneg  11059  abscj  11061  absval2  11066  absreim  11077  absmul  11078  absdivap  11079  absid  11080  absre  11086  absexp  11088  absexpzap  11089  absimle  11093  abssub  11110  abs3dif  11114  abs2dif  11115  abs2dif2  11116  recan  11118  cau3lem  11123  max0addsup  11228  minabs  11244  bdtrilem  11247  clim  11289  clim2  11291  clim0  11293  clim0c  11294  climi0  11297  climconst  11298  climshftlemg  11310  climcn1  11316  climcn2  11317  addcn2  11318  subcn2  11319  mulcn2  11320  reccn2ap  11321  cjcn2  11324  recn2  11325  imcn2  11326  iser3shft  11354  climcau  11355  climcvg1nlem  11357  climcvg1n  11358  serf0  11360  summodclem3  11388  summodclem2a  11389  summodc  11391  fsumf1o  11398  sumsnf  11417  fsumm1  11424  fsumcnv  11445  fsumabs  11473  fsumrelem  11479  iserabs  11483  hash2iun1dif1  11488  isumshft  11498  isumsplit  11499  expcnvap0  11510  expcnv  11512  cvgratnnlemseq  11534  cvgratnnlemrate  11538  cvgratz  11540  mertenslemub  11542  mertenslemi1  11543  mertenslem2  11544  mertensabs  11545  prodmodclem3  11583  fprodf1o  11596  prodsnf  11600  fprodm1  11606  fprodabs  11624  fprodcnv  11633  efcllemp  11666  efcj  11681  efaddlem  11682  efcan  11684  efsub  11689  efexp  11690  efzval  11691  efgt0  11692  eftlub  11698  efltim  11706  sinval  11710  cosval  11711  tanval3ap  11722  resinval  11723  recosval  11724  resin4p  11726  recos4p  11727  sinneg  11734  cosneg  11735  efmival  11741  efeul  11742  sinadd  11744  cosadd  11745  sinsub  11748  cossub  11749  addsin  11750  subsin  11751  addcos  11754  subcos  11755  sincossq  11756  sin2t  11757  cos2t  11758  sin01bnd  11765  cos01bnd  11766  sin02gt0  11771  cos12dec  11775  absefi  11776  absef  11777  absefib  11778  efieq1re  11779  demoivre  11780  demoivreALT  11781  flodddiv4  11939  alginv  12047  algcvg  12048  eucalgval  12054  eucalginv  12056  eucalglt  12057  eucalgcvga  12058  eucalg  12059  lcmgcd  12078  lcm1  12081  sqpweven  12175  2sqpwodd  12176  sqne2sq  12177  qnumval  12185  qdenval  12186  qden1elz  12205  nn0sqrtelqelz  12206  phival  12213  dfphi2  12220  phiprmpw  12222  phiprm  12223  eulerthlemth  12232  hashgcdeq  12239  phisum  12240  pythagtriplem6  12270  pythagtriplem7  12271  pythagtriplem12  12275  pythagtriplem14  12277  fldivp1  12346  ennnfonelemg  12404  ennnfonelemp1  12407  ennnfonelemkh  12413  ennnfonelemhf1o  12414  ennnfonelemnn0  12423  ctinfomlemom  12428  ctiunctlemu1st  12435  ctiunctlemu2nd  12436  ctiunctlemudc  12438  ctiunctlemfo  12440  isstruct2im  12472  isstruct2r  12473  strslfv3  12508  setsslid  12513  ressbasd  12527  resseqnbasd  12532  ressplusgd  12587  ptex  12713  prdsex  12718  imasex  12726  imasival  12727  f1ocpbl  12732  f1ovscpbl  12733  imasaddvallemg  12736  qusval  12744  fvprif  12762  xpsff1o  12768  ismhm  12853  mhmpropd  12857  mhmlin  12858  mhmf1o  12861  mhmco  12874  grpinvsub  12952  mhmlem  12978  mhmid  12979  mhmmnd  12980  ghmgrp  12982  mulgfvalg  12985  mulgval  12986  mulgnegnn  12993  mulgneg  13001  mulgnegneg  13002  mulgm1  13003  mulginvcom  13008  mulgz  13011  mulgnndir  13012  mulgdir  13015  mulgass  13020  mhmmulg  13024  subgmulg  13048  isnsg  13062  eqgfval  13081  ablsub2inv  13114  mgpplusgg  13134  mgpbasg  13136  mgpscag  13137  mgptsetg  13138  mgpdsg  13140  isring  13183  ringm2neg  13232  opprmulfvalg  13242  opprsllem  13246  isunitd  13275  opprunitd  13279  invrfvald  13291  rdivmuldivd  13313  islmod  13381  islmodd  13383  scaffvalg  13396  lmodpropd  13439  istps  13535  tpspropd  13539  eltpsg  13543  txvalex  13757  txval  13758  txbasval  13770  upxp  13775  uptx  13777  txrest  13779  cnmpt11  13786  cnmpt21  13794  hmeontr  13816  txhmeo  13822  psmetxrge0  13835  xmetunirn  13861  mopnval  13945  mopntopon  13946  isxms  13954  isxms2  13955  isms  13956  msrtri  13979  xmspropd  13980  mspropd  13981  setsmsbasg  13982  setsmsdsg  13983  setsmstsetg  13984  comet  14002  metcnpi  14018  metcnpi2  14019  cnbl0  14037  cnblcld  14038  resubmet  14051  elcncf  14063  cncfi  14068  rescncf  14071  mulc1cncf  14079  cncfco  14081  cncfmptid  14086  addccncf  14089  cdivcncfap  14090  negcncf  14091  mulcncflem  14093  ivthinclemlopn  14117  ivthinclemuopn  14119  limccl  14131  ellimc3apf  14132  limcimolemlt  14136  cnplimclemle  14140  limccnpcntop  14147  reldvg  14151  dvfvalap  14153  dveflem  14190  dvef  14191  sin0pilem1  14205  ef2kpi  14230  sinperlem  14232  sin2kpi  14235  cos2kpi  14236  sin2pim  14237  cos2pim  14238  ptolemy  14248  sincosq2sgn  14251  sincosq3sgn  14252  sincosq4sgn  14253  sinq12gt0  14254  tangtx  14262  sincosq1eq  14263  abssinper  14270  sinkpi  14271  coskpi  14272  cosq34lt1  14274  relogeftb  14289  relogoprlem  14292  relogexp  14296  rpcxpef  14318  logcxp  14321  1cxp  14324  ecxp  14325  rpcxpadd  14329  rpmulcxp  14333  cxpmul  14336  abscxp  14338  logsqrt  14346  rpabscxpbnd  14362  rpcxplogb  14385  lgsval  14408  lgsval2lem  14414  lgsval4a  14426  lgsdi  14441  nnsf  14757  peano4nninf  14758  peano3nninf  14759  nninfalllem1  14760  nninfall  14761  nninfsellemdc  14762  nninfsellemeq  14766  nninfsellemqall  14767  nninfsellemeqinf  14768  nninfsel  14769  exmidsbthr  14774  qdencn  14778  refeq  14779  isomninnlem  14781  apdifflemr  14798  apdiff  14799  ismkvnnlem  14803  nconstwlpolem  14815