Theorem fveq2d 5652

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

Syntax hints:   → wi 4   = wceq 1398  ‘cfv 5333

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 717  ax-5 1496  ax-7 1497  ax-gen 1498  ax-ie1 1542  ax-ie2 1543  ax-8 1553  ax-10 1554  ax-11 1555  ax-i12 1556  ax-bndl 1558  ax-4 1559  ax-17 1575  ax-i9 1579  ax-ial 1583  ax-i5r 1584  ax-ext 2213

This theorem depends on definitions:  df-bi 117  df-3an 1007  df-tru 1401  df-nf 1510  df-sb 1811  df-clab 2218  df-cleq 2224  df-clel 2227  df-nfc 2364  df-rex 2517  df-v 2805  df-un 3205  df-sn 3679  df-pr 3680  df-op 3682  df-uni 3899  df-br 4094  df-iota 5293  df-fv 5341

This theorem is referenced by:  2fveq3  5653  fveq12d  5655  fveqeq2d  5656  csbfvg  5690  fvmptdf  5743  fvmptt  5747  resfvresima  5901  fcof1  5934  oveq1  6035  oveq2  6036  fvoveq1d  6050  caofinvl  6270  op1stg  6322  op2ndg  6323  ot1stg  6324  ot2ndg  6325  eloprabi  6370  1stconst  6395  algrflemg  6404  tfrlem1  6517  tfrlem3ag  6518  tfrlem3a  6519  tfrlem9  6528  tfr0dm  6531  tfrlemisucaccv  6534  tfrlemiubacc  6539  tfrlemiex  6540  tfrlemi1  6541  tfr1onlem3ag  6546  tfr1onlemsucaccv  6550  tfr1onlemubacc  6555  tfr1onlemex  6556  tfr1onlemaccex  6557  tfrcllemsucaccv  6563  tfrcllembxssdm  6565  tfrcllemubacc  6568  tfrcllemex  6569  tfrcllemaccex  6570  tfrcllemres  6571  tfrcldm  6572  rdgivallem  6590  rdgival  6591  rdgss  6592  rdgisuc1  6593  rdgon  6595  rdg0  6596  frec0g  6606  frecabcl  6608  freccllem  6611  frecfcllem  6613  frecsuclem  6615  frecsuc  6616  frecrdg  6617  oav2  6674  omv2  6676  xpdom2  7058  xpmapenlem  7078  xpmapen  7079  ac6sfi  7130  1stinl  7316  2ndinl  7317  1stinr  7318  2ndinr  7319  updjudhcoinlf  7322  updjudhcoinrg  7323  caseinl  7333  caseinr  7334  omp1eomlem  7336  omp1eom  7337  difinfsn  7342  ctmlemr  7350  ctm  7351  ctssdclemn0  7352  ctssdccl  7353  nninfninc  7365  nnnninfeq  7370  nnnninfeq2  7371  enomnilem  7380  enmkvlem  7403  enwomnilem  7411  exmidfodomrlemeldju  7453  exmidfodomrlemreseldju  7454  exmidfodomrlemr  7456  exmidfodomrlemrALT  7457  exmidaclem  7466  cc2  7529  cc3  7530  ltdfpr  7769  genpelvl  7775  genpelvu  7776  recexpr  7901  cauappcvgprlem1  7922  caucvgprlemnkj  7929  caucvgprlemnbj  7930  caucvgprlemm  7931  caucvgprlemdisj  7937  caucvgprlemloc  7938  caucvgprlemcl  7939  caucvgprlemladdfu  7940  caucvgprlemladdrl  7941  caucvgprlem1  7942  caucvgprlem2  7943  caucvgpr  7945  caucvgprprlemell  7948  caucvgprprlemelu  7949  caucvgprprlemcbv  7950  caucvgprprlemval  7951  caucvgprprlemnkeqj  7953  caucvgprprlemmu  7958  caucvgprprlemopl  7960  caucvgprprlemlol  7961  caucvgprprlemopu  7962  caucvgprprlemloc  7966  caucvgprprlemclphr  7968  caucvgprprlemexbt  7969  caucvgprprlem1  7972  caucvgprprlem2  7973  caucvgsr  8065  axcaucvglemval  8160  axcaucvglemres  8162  fv0p1e1  9300  uzin  9833  cnref1o  9929  fzsuc2  10359  fseq1m1p1  10375  fzoss2  10454  elfzonlteqm1  10501  divfl0  10602  flqzadd  10604  fldiv4p1lem1div2  10611  ceilqval  10614  flqdiv  10629  modqval  10632  modqfrac  10645  modqmulnn  10650  modqid  10657  modqcyc  10667  modqdi  10700  frec2uzuzd  10710  frec2uzrdg  10717  frecuzrdgrcl  10718  frecuzrdgtcl  10720  frecuzrdgsuc  10722  frecuzrdgrclt  10723  frecuzrdgg  10724  frecuzrdgfunlem  10727  frecuzrdgsuctlem  10731  iseqovex  10766  iseqvalcbv  10767  seq3val  10768  seqvalcd  10769  seq3m1  10781  seq3shft2  10789  seqshft2g  10790  monoord  10793  monoord2  10794  iseqf1olemqval  10808  iseqf1olemab  10810  iseqf1olemqk  10815  iseqf1olemjpcl  10816  iseqf1olemqpcl  10817  iseqf1olemfvp  10818  seq3f1olemqsumkj  10819  seq3f1olemqsumk  10820  seq3f1olemqsum  10821  seq3f1olemp  10823  seq3f1oleml  10824  seqf1oglem1  10827  seqf1oglem2  10828  seqf1og  10829  seq3homo  10835  seqhomog  10838  exp3val  10849  expnegap0  10855  facnn2  11042  facwordi  11048  faclbnd6  11052  bcval  11057  bccmpl  11062  bcn0  11063  bcm1k  11068  bcp1n  11069  bcn2  11072  hashinfom  11086  hashennn  11088  hashsng  11106  omgadd  11111  hashprg  11118  fihashssdif  11128  hashdifpr  11130  hashfzo  11132  hashfzp1  11134  hashxp  11136  zfz1isolemiso  11149  zfz1iso  11151  hashtpglem  11156  lsw1  11212  ccatfvalfi  11218  ccatlen  11221  ccatval3  11225  ccatval21sw  11231  ccatlid  11232  ccatass  11234  lswccatn0lsw  11237  lswccat0lsw  11238  ccatalpha  11239  s1leng  11250  ccats1val2  11266  lswccats1  11269  swrdfv0  11284  swrdfv2  11293  swrdsbslen  11296  swrds1  11298  ccatswrd  11300  pfxmpt  11310  pfxfv  11314  pfxtrcfvl  11327  ccatpfx  11331  swrdswrd  11335  lenpfxcctswrd  11341  ccatopth  11346  cats1un  11351  swrdccatin2  11359  pfxccatin12lem2  11361  shftval2  11449  shftval3  11450  shftval4  11451  shftval5  11452  seq3shft  11461  imval  11473  imre  11474  reim  11475  crim  11481  reim0  11484  mulreap  11487  recj  11490  reneg  11491  readd  11492  resub  11493  remullem  11494  redivap  11497  imcj  11498  imneg  11499  imadd  11500  imsub  11501  imdivap  11504  cjsub  11515  cjexp  11516  cjreim2  11527  cjap  11529  cjdivap  11532  cnrecnv  11533  cvg1nlemcau  11607  cvg1nlemres  11608  absval  11624  rennim  11625  sqrtdiv  11665  sqrtmsq  11668  absneg  11673  abscj  11675  absval2  11680  absreim  11691  absmul  11692  absdivap  11693  absid  11694  absre  11700  absexp  11702  absexpzap  11703  absimle  11707  abssub  11724  abs3dif  11728  abs2dif  11729  abs2dif2  11730  recan  11732  cau3lem  11737  max0addsup  11842  minabs  11859  bdtrilem  11862  clim  11904  clim2  11906  clim0  11908  clim0c  11909  climi0  11912  climconst  11913  climshftlemg  11925  climcn1  11931  climcn2  11932  addcn2  11933  subcn2  11934  mulcn2  11935  reccn2ap  11936  cjcn2  11939  recn2  11940  imcn2  11941  iser3shft  11969  climcau  11970  climcvg1nlem  11972  climcvg1n  11973  serf0  11975  fzf1o  11999  summodclem3  12004  summodclem2a  12005  summodc  12007  fsumf1o  12014  sumsnf  12033  fsumm1  12040  fsumcnv  12061  fsumabs  12089  fsumrelem  12095  iserabs  12099  hash2iun1dif1  12104  isumshft  12114  isumsplit  12115  expcnvap0  12126  expcnv  12128  cvgratnnlemseq  12150  cvgratnnlemrate  12154  cvgratz  12156  mertenslemub  12158  mertenslemi1  12159  mertenslem2  12160  mertensabs  12161  prodmodclem3  12199  fprodf1o  12212  prodsnf  12216  fprodm1  12222  fprodabs  12240  fprodcnv  12249  efcllemp  12282  efcj  12297  efaddlem  12298  efcan  12300  efsub  12305  efexp  12306  efzval  12307  efgt0  12308  eftlub  12314  efltim  12322  sinval  12326  cosval  12327  tanval3ap  12338  resinval  12339  recosval  12340  resin4p  12342  recos4p  12343  sinneg  12350  cosneg  12351  efmival  12357  efeul  12358  sinadd  12360  cosadd  12361  sinsub  12364  cossub  12365  addsin  12366  subsin  12367  addcos  12370  subcos  12371  sincossq  12372  sin2t  12373  cos2t  12374  sin01bnd  12381  cos01bnd  12382  sin02gt0  12388  cos12dec  12392  absefi  12393  absef  12394  absefib  12395  efieq1re  12396  demoivre  12397  demoivreALT  12398  flodddiv4  12560  bitsval  12567  bits0  12572  bitsp1  12575  bitsp1e  12576  bitsp1o  12577  bitsmod  12580  nninfctlemfo  12674  alginv  12682  algcvg  12683  eucalgval  12689  eucalginv  12691  eucalglt  12692  eucalgcvga  12693  eucalg  12694  lcmgcd  12713  lcm1  12716  sqpweven  12810  2sqpwodd  12811  sqne2sq  12812  qnumval  12820  qdenval  12821  qden1elz  12840  nn0sqrtelqelz  12841  phival  12848  dfphi2  12855  phiprmpw  12857  phiprm  12858  eulerthlemth  12867  hashgcdeq  12875  phisum  12876  pythagtriplem6  12906  pythagtriplem7  12907  pythagtriplem12  12911  pythagtriplem14  12913  fldivp1  12984  4sqlem11  13037  ennnfonelemg  13087  ennnfonelemp1  13090  ennnfonelemkh  13096  ennnfonelemhf1o  13097  ennnfonelemnn0  13106  ctinfomlemom  13111  ctiunctlemu1st  13118  ctiunctlemu2nd  13119  ctiunctlemudc  13121  ctiunctlemfo  13123  isstruct2im  13155  isstruct2r  13156  setsslid  13196  ressbasd  13213  resseqnbasd  13219  ressplusgd  13275  ptex  13410  prdsex  13415  prdsval  13419  prdsbas3  13433  pwsval  13437  pwsbas  13438  pwsplusgval  13441  pwsmulrval  13442  imasex  13451  imasival  13452  f1ocpbl  13457  f1ovscpbl  13458  imasaddvallemg  13461  qusval  13469  fvprif  13489  xpsff1o  13495  igsumvalx  13535  gsumprval  13545  pws0g  13597  imasmnd  13599  ismhm  13607  mhmpropd  13612  mhmlin  13613  mhmf1o  13616  resmhm  13633  mhmco  13636  gsumwmhm  13644  grpinvsub  13728  pwsinvg  13758  imasgrp2  13760  imasgrp  13761  mhmlem  13764  mhmid  13765  mhmmnd  13766  ghmgrp  13768  mulgfvalg  13771  mulgval  13772  mulgnegnn  13782  mulgneg  13790  mulgnegneg  13791  mulgm1  13792  mulginvcom  13797  mulgz  13800  mulgnndir  13801  mulgdir  13804  mulgass  13809  mhmmulg  13813  subgmulg  13838  isnsg  13852  eqgfval  13872  ghmlin  13898  ghmid  13899  ghminv  13900  ghmsub  13901  ghmmulg  13906  resghm  13910  ghmeql  13917  ablsub2inv  13961  ghmcmn  13977  invghm  13979  imasabl  13986  gsumfzreidx  13987  gsumfzmhm  13993  gsumsplit0  13996  mgpplusgg  14001  mgpbasg  14003  mgpscag  14004  mgptsetg  14005  mgpdsg  14007  rngm2neg  14026  imasrng  14033  isring  14077  ringm2neg  14132  imasring  14141  opprmulfvalg  14147  opprsllem  14151  isunitd  14184  opprunitd  14188  invrfvald  14200  rdivmuldivd  14222  rhmmul  14242  isrhm2d  14243  rhm1  14245  rhmdvdsr  14253  rhmopp  14254  rhmunitinv  14256  islmod  14370  islmodd  14372  scaffvalg  14385  lmodpropd  14428  lsssetm  14435  islssmd  14438  lssats2  14493  lspsnneg  14499  lspsnsub  14500  lspun0  14504  lmodindp1  14507  sralemg  14517  srascag  14521  sravscag  14522  sraipg  14523  rlmscabas  14539  ixpsnbasval  14545  2idlval  14581  2idlvalg  14582  mulgrhm2  14689  zlmlemg  14707  zlmsca  14711  zlmvscag  14712  znval  14715  znle  14716  znbaslemnn  14718  znidomb  14737  psrval  14745  psrbasg  14758  psrplusgg  14762  mplvalcoe  14774  mplsubgfileminv  14784  mpl0fi  14786  mplnegfi  14789  istps  14826  tpspropd  14830  eltpsg  14834  txvalex  15048  txval  15049  txbasval  15061  upxp  15066  uptx  15068  txrest  15070  cnmpt11  15077  cnmpt21  15085  hmeontr  15107  txhmeo  15113  psmetxrge0  15126  xmetunirn  15152  mopnval  15236  mopntopon  15237  isxms  15245  isxms2  15246  isms  15247  msrtri  15270  xmspropd  15271  mspropd  15272  setsmsbasg  15273  setsmsdsg  15274  setsmstsetg  15275  comet  15293  metcnpi  15309  metcnpi2  15310  cnbl0  15328  cnblcld  15329  resubmet  15350  mpomulcn  15360  elcncf  15367  cncfi  15372  rescncf  15375  mulc1cncf  15383  cncfco  15385  cncfmptid  15391  addccncf  15394  cdivcncfap  15398  negcncf  15399  mulcncflem  15401  ivthinclemlopn  15430  ivthinclemuopn  15432  limccl  15453  ellimc3apf  15454  limcimolemlt  15458  cnplimclemle  15462  limccnpcntop  15469  reldvg  15473  dvfvalap  15475  dveflem  15520  dvef  15521  plymullem1  15542  plycjlemc  15554  plycj  15555  plyrecj  15557  plyreres  15558  sin0pilem1  15575  ef2kpi  15600  sinperlem  15602  sin2kpi  15605  cos2kpi  15606  sin2pim  15607  cos2pim  15608  ptolemy  15618  sincosq2sgn  15621  sincosq3sgn  15622  sincosq4sgn  15623  sinq12gt0  15624  tangtx  15632  sincosq1eq  15633  abssinper  15640  sinkpi  15641  coskpi  15642  cosq34lt1  15644  relogeftb  15659  relogoprlem  15662  relogexp  15666  rpcxpef  15688  logcxp  15691  1cxp  15694  ecxp  15695  rpcxpadd  15699  rpmulcxp  15703  cxpmul  15706  abscxp  15709  logsqrt  15717  rpabscxpbnd  15734  rpcxplogb  15758  pellexlem1  15774  pellexlem2  15775  pellexlem3  15776  lgsval  15806  lgsval2lem  15812  lgsval4a  15824  lgsdi  15839  lgseisenlem3  15874  lgseisenlem4  15875  lgsquadlem1  15879  lgsquadlem2  15880  lgsquadlem3  15881  2lgslem1  15893  2lgslem3a  15895  2lgslem3b  15896  2lgslem3c  15897  2lgslem3d  15898  vtxdgfval  16212  vtxdgfifival  16215  vtxdgop  16216  vtxdgfi0e  16219  vtxdeqd  16220  vtxdfifiun  16221  vtxdumgrfival  16222  1hevtxdg1en  16232  iswlk  16247  2wlklem  16300  wlkres  16303  clwwlkccatlem  16324  clwwlkn2  16345  clwwlkext2edg  16346  umgr2cwwk2dif  16348  clwwlknonex2lem2  16362  eupth2fi  16403  eulerpathprum  16404  depindlem1  16430  depind  16433  nnsf  16714  peano4nninf  16715  peano3nninf  16716  nninfalllem1  16717  nninfall  16718  nninfsellemdc  16719  nninfsellemeq  16723  nninfsellemqall  16724  nninfsellemeqinf  16725  nninfsel  16726  nnnninfex  16731  exmidsbthr  16734  qdencn  16738  refeq  16739  repiecele0  16741  repiecege0  16742  repiecef  16743  isomninnlem  16745  apdifflemr  16762  apdiff  16763  qdiff  16764  ismkvnnlem  16768  nconstwlpolem  16781  gfsumval  16792  gsumgfsumlem  16795  gfsump1  16798