Theorem fveq2d 5433

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

Syntax hints:   → wi 4   = wceq 1332  ‘cfv 5131

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-ia1 105  ax-ia2 106  ax-ia3 107  ax-io 699  ax-5 1424  ax-7 1425  ax-gen 1426  ax-ie1 1470  ax-ie2 1471  ax-8 1483  ax-10 1484  ax-11 1485  ax-i12 1486  ax-bndl 1487  ax-4 1488  ax-17 1507  ax-i9 1511  ax-ial 1515  ax-i5r 1516  ax-ext 2122

This theorem depends on definitions:  df-bi 116  df-3an 965  df-tru 1335  df-nf 1438  df-sb 1737  df-clab 2127  df-cleq 2133  df-clel 2136  df-nfc 2271  df-rex 2423  df-v 2691  df-un 3080  df-sn 3538  df-pr 3539  df-op 3541  df-uni 3745  df-br 3938  df-iota 5096  df-fv 5139

This theorem is referenced by:  2fveq3  5434  fveq12d  5436  fveqeq2d  5437  csbfvg  5467  fvmptdf  5516  fvmptt  5520  fcof1  5692  oveq1  5789  oveq2  5790  fvoveq1d  5804  caofinvl  6012  op1stg  6056  op2ndg  6057  ot1stg  6058  ot2ndg  6059  eloprabi  6102  1stconst  6126  algrflemg  6135  tfrlem1  6213  tfrlem3ag  6214  tfrlem3a  6215  tfrlem9  6224  tfr0dm  6227  tfrlemisucaccv  6230  tfrlemiubacc  6235  tfrlemiex  6236  tfrlemi1  6237  tfr1onlem3ag  6242  tfr1onlemsucaccv  6246  tfr1onlemubacc  6251  tfr1onlemex  6252  tfr1onlemaccex  6253  tfrcllemsucaccv  6259  tfrcllembxssdm  6261  tfrcllemubacc  6264  tfrcllemex  6265  tfrcllemaccex  6266  tfrcllemres  6267  tfrcldm  6268  rdgivallem  6286  rdgival  6287  rdgss  6288  rdgisuc1  6289  rdgon  6291  rdg0  6292  frec0g  6302  frecabcl  6304  freccllem  6307  frecfcllem  6309  frecsuclem  6311  frecsuc  6312  frecrdg  6313  oav2  6367  omv2  6369  xpdom2  6733  xpmapenlem  6751  xpmapen  6752  ac6sfi  6800  1stinl  6967  2ndinl  6968  1stinr  6969  2ndinr  6970  updjudhcoinlf  6973  updjudhcoinrg  6974  caseinl  6984  caseinr  6985  omp1eomlem  6987  omp1eom  6988  difinfsn  6993  ctmlemr  7001  ctm  7002  ctssdclemn0  7003  ctssdccl  7004  enomnilem  7018  enmkvlem  7043  enwomnilem  7050  exmidfodomrlemeldju  7072  exmidfodomrlemreseldju  7073  exmidfodomrlemr  7075  exmidfodomrlemrALT  7076  exmidaclem  7081  cc2  7099  cc3  7100  ltdfpr  7338  genpelvl  7344  genpelvu  7345  recexpr  7470  cauappcvgprlem1  7491  caucvgprlemnkj  7498  caucvgprlemnbj  7499  caucvgprlemm  7500  caucvgprlemdisj  7506  caucvgprlemloc  7507  caucvgprlemcl  7508  caucvgprlemladdfu  7509  caucvgprlemladdrl  7510  caucvgprlem1  7511  caucvgprlem2  7512  caucvgpr  7514  caucvgprprlemell  7517  caucvgprprlemelu  7518  caucvgprprlemcbv  7519  caucvgprprlemval  7520  caucvgprprlemnkeqj  7522  caucvgprprlemmu  7527  caucvgprprlemopl  7529  caucvgprprlemlol  7530  caucvgprprlemopu  7531  caucvgprprlemloc  7535  caucvgprprlemclphr  7537  caucvgprprlemexbt  7538  caucvgprprlem1  7541  caucvgprprlem2  7542  caucvgsr  7634  axcaucvglemval  7729  axcaucvglemres  7731  fv0p1e1  8859  uzin  9382  cnref1o  9469  fzsuc2  9890  fseq1m1p1  9906  fzoss2  9980  elfzonlteqm1  10018  divfl0  10100  flqzadd  10102  fldiv4p1lem1div2  10109  ceilqval  10110  flqdiv  10125  modqval  10128  modqfrac  10141  modqmulnn  10146  modqid  10153  modqcyc  10163  modqdi  10196  frec2uzuzd  10206  frec2uzrdg  10213  frecuzrdgrcl  10214  frecuzrdgtcl  10216  frecuzrdgsuc  10218  frecuzrdgrclt  10219  frecuzrdgg  10220  frecuzrdgfunlem  10223  frecuzrdgsuctlem  10227  iseqovex  10260  iseqvalcbv  10261  seq3val  10262  seqvalcd  10263  seq3m1  10272  seq3shft2  10277  monoord  10280  monoord2  10281  iseqf1olemqval  10291  iseqf1olemab  10293  iseqf1olemqk  10298  iseqf1olemjpcl  10299  iseqf1olemqpcl  10300  iseqf1olemfvp  10301  seq3f1olemqsumkj  10302  seq3f1olemqsumk  10303  seq3f1olemqsum  10304  seq3f1olemp  10306  seq3f1oleml  10307  seq3homo  10314  exp3val  10326  expnegap0  10332  facnn2  10512  facwordi  10518  faclbnd6  10522  bcval  10527  bccmpl  10532  bcn0  10533  bcm1k  10538  bcp1n  10539  bcn2  10542  hashinfom  10556  hashennn  10558  hashsng  10576  omgadd  10580  hashprg  10586  fihashssdif  10596  hashdifpr  10598  hashfzo  10600  hashfzp1  10602  hashxp  10604  zfz1isolemiso  10614  zfz1iso  10616  shftval2  10630  shftval3  10631  shftval4  10632  shftval5  10633  seq3shft  10642  imval  10654  imre  10655  reim  10656  crim  10662  reim0  10665  mulreap  10668  recj  10671  reneg  10672  readd  10673  resub  10674  remullem  10675  redivap  10678  imcj  10679  imneg  10680  imadd  10681  imsub  10682  imdivap  10685  cjsub  10696  cjexp  10697  cjreim2  10708  cjap  10710  cjdivap  10713  cnrecnv  10714  cvg1nlemcau  10788  cvg1nlemres  10789  absval  10805  rennim  10806  sqrtdiv  10846  sqrtmsq  10849  absneg  10854  abscj  10856  absval2  10861  absreim  10872  absmul  10873  absdivap  10874  absid  10875  absre  10881  absexp  10883  absexpzap  10884  absimle  10888  abssub  10905  abs3dif  10909  abs2dif  10910  abs2dif2  10911  recan  10913  cau3lem  10918  max0addsup  11023  minabs  11039  bdtrilem  11042  clim  11082  clim2  11084  clim0  11086  clim0c  11087  climi0  11090  climconst  11091  climshftlemg  11103  climcn1  11109  climcn2  11110  addcn2  11111  subcn2  11112  mulcn2  11113  reccn2ap  11114  cjcn2  11117  recn2  11118  imcn2  11119  iser3shft  11147  climcau  11148  climcvg1nlem  11150  climcvg1n  11151  serf0  11153  summodclem3  11181  summodclem2a  11182  summodc  11184  fsumf1o  11191  sumsnf  11210  fsumm1  11217  fsumcnv  11238  fsumabs  11266  fsumrelem  11272  iserabs  11276  hash2iun1dif1  11281  isumshft  11291  isumsplit  11292  expcnvap0  11303  expcnv  11305  cvgratnnlemseq  11327  cvgratnnlemrate  11331  cvgratz  11333  mertenslemub  11335  mertenslemi1  11336  mertenslem2  11337  mertensabs  11338  prodmodclem3  11376  efcllemp  11401  efcj  11416  efaddlem  11417  efcan  11419  efsub  11424  efexp  11425  efzval  11426  efgt0  11427  eftlub  11433  efltim  11441  sinval  11445  cosval  11446  tanval3ap  11457  resinval  11458  recosval  11459  resin4p  11461  recos4p  11462  sinneg  11469  cosneg  11470  efmival  11476  efeul  11477  sinadd  11479  cosadd  11480  sinsub  11483  cossub  11484  addsin  11485  subsin  11486  addcos  11489  subcos  11490  sincossq  11491  sin2t  11492  cos2t  11493  sin01bnd  11500  cos01bnd  11501  sin02gt0  11506  cos12dec  11510  absefi  11511  absef  11512  absefib  11513  efieq1re  11514  demoivre  11515  demoivreALT  11516  flodddiv4  11667  alginv  11764  algcvg  11765  eucalgval  11771  eucalginv  11773  eucalglt  11774  eucalgcvga  11775  eucalg  11776  lcmgcd  11795  lcm1  11798  sqpweven  11889  2sqpwodd  11890  sqne2sq  11891  qnumval  11899  qdenval  11900  qden1elz  11919  nn0sqrtelqelz  11920  phival  11925  dfphi2  11932  phiprmpw  11934  phiprm  11935  hashgcdeq  11940  ennnfonelemg  11952  ennnfonelemp1  11955  ennnfonelemkh  11961  ennnfonelemhf1o  11962  ennnfonelemnn0  11971  ctinfomlemom  11976  ctiunctlemu1st  11983  ctiunctlemu2nd  11984  ctiunctlemudc  11986  ctiunctlemfo  11988  isstruct2im  12008  isstruct2r  12009  strslfv3  12043  setsslid  12048  ressid2  12057  ressval2  12058  istps  12238  tpspropd  12242  eltpsg  12246  txvalex  12462  txval  12463  txbasval  12475  upxp  12480  uptx  12482  txrest  12484  cnmpt11  12491  cnmpt21  12499  hmeontr  12521  txhmeo  12527  psmetxrge0  12540  xmetunirn  12566  mopnval  12650  mopntopon  12651  isxms  12659  isxms2  12660  isms  12661  msrtri  12684  xmspropd  12685  mspropd  12686  setsmsbasg  12687  setsmsdsg  12688  setsmstsetg  12689  comet  12707  metcnpi  12723  metcnpi2  12724  cnbl0  12742  cnblcld  12743  resubmet  12756  elcncf  12768  cncfi  12773  rescncf  12776  mulc1cncf  12784  cncfco  12786  cncfmptid  12791  addccncf  12794  cdivcncfap  12795  negcncf  12796  mulcncflem  12798  ivthinclemlopn  12822  ivthinclemuopn  12824  limccl  12836  ellimc3apf  12837  limcimolemlt  12841  cnplimclemle  12845  limccnpcntop  12852  reldvg  12856  dvfvalap  12858  dveflem  12895  dvef  12896  sin0pilem1  12910  ef2kpi  12935  sinperlem  12937  sin2kpi  12940  cos2kpi  12941  sin2pim  12942  cos2pim  12943  ptolemy  12953  sincosq2sgn  12956  sincosq3sgn  12957  sincosq4sgn  12958  sinq12gt0  12959  tangtx  12967  sincosq1eq  12968  abssinper  12975  sinkpi  12976  coskpi  12977  cosq34lt1  12979  relogeftb  12994  relogoprlem  12997  relogexp  13001  rpcxpef  13023  logcxp  13026  1cxp  13029  ecxp  13030  rpcxpadd  13034  rpmulcxp  13038  cxpmul  13041  abscxp  13043  logsqrt  13051  rpabscxpbnd  13067  rpcxplogb  13089  nnsf  13374  peano4nninf  13375  peano3nninf  13376  nninfalllemn  13377  nninfalllem1  13378  nninfall  13379  nninfsellemdc  13381  nninfsellemeq  13385  nninfsellemqall  13386  nninfsellemeqinf  13387  nninfsel  13388  nninfomni  13390  exmidsbthr  13393  qdencn  13397  refeq  13398  isomninnlem  13400  apdifflemr  13415  apdiff  13416  ismkvnnlem  13419