Theorem fveq2d 5515

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

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

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 3597  df-pr 3598  df-op 3600  df-uni 3808  df-br 4001  df-iota 5174  df-fv 5220

This theorem is referenced by:  2fveq3  5516  fveq12d  5518  fveqeq2d  5519  csbfvg  5549  fvmptdf  5599  fvmptt  5603  fcof1  5778  oveq1  5876  oveq2  5877  fvoveq1d  5891  caofinvl  6099  op1stg  6145  op2ndg  6146  ot1stg  6147  ot2ndg  6148  eloprabi  6191  1stconst  6216  algrflemg  6225  tfrlem1  6303  tfrlem3ag  6304  tfrlem3a  6305  tfrlem9  6314  tfr0dm  6317  tfrlemisucaccv  6320  tfrlemiubacc  6325  tfrlemiex  6326  tfrlemi1  6327  tfr1onlem3ag  6332  tfr1onlemsucaccv  6336  tfr1onlemubacc  6341  tfr1onlemex  6342  tfr1onlemaccex  6343  tfrcllemsucaccv  6349  tfrcllembxssdm  6351  tfrcllemubacc  6354  tfrcllemex  6355  tfrcllemaccex  6356  tfrcllemres  6357  tfrcldm  6358  rdgivallem  6376  rdgival  6377  rdgss  6378  rdgisuc1  6379  rdgon  6381  rdg0  6382  frec0g  6392  frecabcl  6394  freccllem  6397  frecfcllem  6399  frecsuclem  6401  frecsuc  6402  frecrdg  6403  oav2  6458  omv2  6460  xpdom2  6825  xpmapenlem  6843  xpmapen  6844  ac6sfi  6892  1stinl  7067  2ndinl  7068  1stinr  7069  2ndinr  7070  updjudhcoinlf  7073  updjudhcoinrg  7074  caseinl  7084  caseinr  7085  omp1eomlem  7087  omp1eom  7088  difinfsn  7093  ctmlemr  7101  ctm  7102  ctssdclemn0  7103  ctssdccl  7104  nnnninfeq  7120  nnnninfeq2  7121  enomnilem  7130  enmkvlem  7153  enwomnilem  7161  exmidfodomrlemeldju  7192  exmidfodomrlemreseldju  7193  exmidfodomrlemr  7195  exmidfodomrlemrALT  7196  exmidaclem  7201  cc2  7257  cc3  7258  ltdfpr  7496  genpelvl  7502  genpelvu  7503  recexpr  7628  cauappcvgprlem1  7649  caucvgprlemnkj  7656  caucvgprlemnbj  7657  caucvgprlemm  7658  caucvgprlemdisj  7664  caucvgprlemloc  7665  caucvgprlemcl  7666  caucvgprlemladdfu  7667  caucvgprlemladdrl  7668  caucvgprlem1  7669  caucvgprlem2  7670  caucvgpr  7672  caucvgprprlemell  7675  caucvgprprlemelu  7676  caucvgprprlemcbv  7677  caucvgprprlemval  7678  caucvgprprlemnkeqj  7680  caucvgprprlemmu  7685  caucvgprprlemopl  7687  caucvgprprlemlol  7688  caucvgprprlemopu  7689  caucvgprprlemloc  7693  caucvgprprlemclphr  7695  caucvgprprlemexbt  7696  caucvgprprlem1  7699  caucvgprprlem2  7700  caucvgsr  7792  axcaucvglemval  7887  axcaucvglemres  7889  fv0p1e1  9023  uzin  9549  cnref1o  9639  fzsuc2  10065  fseq1m1p1  10081  fzoss2  10158  elfzonlteqm1  10196  divfl0  10282  flqzadd  10284  fldiv4p1lem1div2  10291  ceilqval  10292  flqdiv  10307  modqval  10310  modqfrac  10323  modqmulnn  10328  modqid  10335  modqcyc  10345  modqdi  10378  frec2uzuzd  10388  frec2uzrdg  10395  frecuzrdgrcl  10396  frecuzrdgtcl  10398  frecuzrdgsuc  10400  frecuzrdgrclt  10401  frecuzrdgg  10402  frecuzrdgfunlem  10405  frecuzrdgsuctlem  10409  iseqovex  10442  iseqvalcbv  10443  seq3val  10444  seqvalcd  10445  seq3m1  10454  seq3shft2  10459  monoord  10462  monoord2  10463  iseqf1olemqval  10473  iseqf1olemab  10475  iseqf1olemqk  10480  iseqf1olemjpcl  10481  iseqf1olemqpcl  10482  iseqf1olemfvp  10483  seq3f1olemqsumkj  10484  seq3f1olemqsumk  10485  seq3f1olemqsum  10486  seq3f1olemp  10488  seq3f1oleml  10489  seq3homo  10496  exp3val  10508  expnegap0  10514  facnn2  10698  facwordi  10704  faclbnd6  10708  bcval  10713  bccmpl  10718  bcn0  10719  bcm1k  10724  bcp1n  10725  bcn2  10728  hashinfom  10742  hashennn  10744  hashsng  10762  omgadd  10766  hashprg  10772  fihashssdif  10782  hashdifpr  10784  hashfzo  10786  hashfzp1  10788  hashxp  10790  zfz1isolemiso  10803  zfz1iso  10805  shftval2  10819  shftval3  10820  shftval4  10821  shftval5  10822  seq3shft  10831  imval  10843  imre  10844  reim  10845  crim  10851  reim0  10854  mulreap  10857  recj  10860  reneg  10861  readd  10862  resub  10863  remullem  10864  redivap  10867  imcj  10868  imneg  10869  imadd  10870  imsub  10871  imdivap  10874  cjsub  10885  cjexp  10886  cjreim2  10897  cjap  10899  cjdivap  10902  cnrecnv  10903  cvg1nlemcau  10977  cvg1nlemres  10978  absval  10994  rennim  10995  sqrtdiv  11035  sqrtmsq  11038  absneg  11043  abscj  11045  absval2  11050  absreim  11061  absmul  11062  absdivap  11063  absid  11064  absre  11070  absexp  11072  absexpzap  11073  absimle  11077  abssub  11094  abs3dif  11098  abs2dif  11099  abs2dif2  11100  recan  11102  cau3lem  11107  max0addsup  11212  minabs  11228  bdtrilem  11231  clim  11273  clim2  11275  clim0  11277  clim0c  11278  climi0  11281  climconst  11282  climshftlemg  11294  climcn1  11300  climcn2  11301  addcn2  11302  subcn2  11303  mulcn2  11304  reccn2ap  11305  cjcn2  11308  recn2  11309  imcn2  11310  iser3shft  11338  climcau  11339  climcvg1nlem  11341  climcvg1n  11342  serf0  11344  summodclem3  11372  summodclem2a  11373  summodc  11375  fsumf1o  11382  sumsnf  11401  fsumm1  11408  fsumcnv  11429  fsumabs  11457  fsumrelem  11463  iserabs  11467  hash2iun1dif1  11472  isumshft  11482  isumsplit  11483  expcnvap0  11494  expcnv  11496  cvgratnnlemseq  11518  cvgratnnlemrate  11522  cvgratz  11524  mertenslemub  11526  mertenslemi1  11527  mertenslem2  11528  mertensabs  11529  prodmodclem3  11567  fprodf1o  11580  prodsnf  11584  fprodm1  11590  fprodabs  11608  fprodcnv  11617  efcllemp  11650  efcj  11665  efaddlem  11666  efcan  11668  efsub  11673  efexp  11674  efzval  11675  efgt0  11676  eftlub  11682  efltim  11690  sinval  11694  cosval  11695  tanval3ap  11706  resinval  11707  recosval  11708  resin4p  11710  recos4p  11711  sinneg  11718  cosneg  11719  efmival  11725  efeul  11726  sinadd  11728  cosadd  11729  sinsub  11732  cossub  11733  addsin  11734  subsin  11735  addcos  11738  subcos  11739  sincossq  11740  sin2t  11741  cos2t  11742  sin01bnd  11749  cos01bnd  11750  sin02gt0  11755  cos12dec  11759  absefi  11760  absef  11761  absefib  11762  efieq1re  11763  demoivre  11764  demoivreALT  11765  flodddiv4  11922  alginv  12030  algcvg  12031  eucalgval  12037  eucalginv  12039  eucalglt  12040  eucalgcvga  12041  eucalg  12042  lcmgcd  12061  lcm1  12064  sqpweven  12158  2sqpwodd  12159  sqne2sq  12160  qnumval  12168  qdenval  12169  qden1elz  12188  nn0sqrtelqelz  12189  phival  12196  dfphi2  12203  phiprmpw  12205  phiprm  12206  eulerthlemth  12215  hashgcdeq  12222  phisum  12223  pythagtriplem6  12253  pythagtriplem7  12254  pythagtriplem12  12258  pythagtriplem14  12260  fldivp1  12329  ennnfonelemg  12387  ennnfonelemp1  12390  ennnfonelemkh  12396  ennnfonelemhf1o  12397  ennnfonelemnn0  12406  ctinfomlemom  12411  ctiunctlemu1st  12418  ctiunctlemu2nd  12419  ctiunctlemudc  12421  ctiunctlemfo  12423  isstruct2im  12455  isstruct2r  12456  strslfv3  12490  setsslid  12495  ressbasd  12509  resseqnbasd  12514  ressplusgd  12566  ismhm  12743  mhmpropd  12747  mhmlin  12748  mhmf1o  12751  mhmco  12764  grpinvsub  12841  mhmlem  12867  mhmid  12868  mhmmnd  12869  ghmgrp  12871  mulgfvalg  12874  mulgval  12875  mulgnegnn  12882  mulgneg  12890  mulgnegneg  12891  mulgm1  12892  mulginvcom  12896  mulgz  12899  mulgnndir  12900  mulgdir  12903  mulgass  12908  mhmmulg  12912  ablsub2inv  12941  mgpplusgg  12961  mgpbasg  12963  mgpscag  12964  mgptsetg  12965  mgpdsg  12967  isring  13009  ringm2neg  13058  opprmulfvalg  13067  opprsllem  13071  isunitd  13100  opprunitd  13104  invrfvald  13116  istps  13197  tpspropd  13201  eltpsg  13205  txvalex  13421  txval  13422  txbasval  13434  upxp  13439  uptx  13441  txrest  13443  cnmpt11  13450  cnmpt21  13458  hmeontr  13480  txhmeo  13486  psmetxrge0  13499  xmetunirn  13525  mopnval  13609  mopntopon  13610  isxms  13618  isxms2  13619  isms  13620  msrtri  13643  xmspropd  13644  mspropd  13645  setsmsbasg  13646  setsmsdsg  13647  setsmstsetg  13648  comet  13666  metcnpi  13682  metcnpi2  13683  cnbl0  13701  cnblcld  13702  resubmet  13715  elcncf  13727  cncfi  13732  rescncf  13735  mulc1cncf  13743  cncfco  13745  cncfmptid  13750  addccncf  13753  cdivcncfap  13754  negcncf  13755  mulcncflem  13757  ivthinclemlopn  13781  ivthinclemuopn  13783  limccl  13795  ellimc3apf  13796  limcimolemlt  13800  cnplimclemle  13804  limccnpcntop  13811  reldvg  13815  dvfvalap  13817  dveflem  13854  dvef  13855  sin0pilem1  13869  ef2kpi  13894  sinperlem  13896  sin2kpi  13899  cos2kpi  13900  sin2pim  13901  cos2pim  13902  ptolemy  13912  sincosq2sgn  13915  sincosq3sgn  13916  sincosq4sgn  13917  sinq12gt0  13918  tangtx  13926  sincosq1eq  13927  abssinper  13934  sinkpi  13935  coskpi  13936  cosq34lt1  13938  relogeftb  13953  relogoprlem  13956  relogexp  13960  rpcxpef  13982  logcxp  13985  1cxp  13988  ecxp  13989  rpcxpadd  13993  rpmulcxp  13997  cxpmul  14000  abscxp  14002  logsqrt  14010  rpabscxpbnd  14026  rpcxplogb  14049  lgsval  14072  lgsval2lem  14078  lgsval4a  14090  lgsdi  14105  nnsf  14410  peano4nninf  14411  peano3nninf  14412  nninfalllem1  14413  nninfall  14414  nninfsellemdc  14415  nninfsellemeq  14419  nninfsellemqall  14420  nninfsellemeqinf  14421  nninfsel  14422  exmidsbthr  14427  qdencn  14431  refeq  14432  isomninnlem  14434  apdifflemr  14451  apdiff  14452  ismkvnnlem  14456  nconstwlpolem  14468