Theorem fveq2d 5565

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

Syntax hints:   → wi 4   = wceq 1364  ‘cfv 5259

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 710  ax-5 1461  ax-7 1462  ax-gen 1463  ax-ie1 1507  ax-ie2 1508  ax-8 1518  ax-10 1519  ax-11 1520  ax-i12 1521  ax-bndl 1523  ax-4 1524  ax-17 1540  ax-i9 1544  ax-ial 1548  ax-i5r 1549  ax-ext 2178

This theorem depends on definitions:  df-bi 117  df-3an 982  df-tru 1367  df-nf 1475  df-sb 1777  df-clab 2183  df-cleq 2189  df-clel 2192  df-nfc 2328  df-rex 2481  df-v 2765  df-un 3161  df-sn 3629  df-pr 3630  df-op 3632  df-uni 3841  df-br 4035  df-iota 5220  df-fv 5267

This theorem is referenced by:  2fveq3  5566  fveq12d  5568  fveqeq2d  5569  csbfvg  5601  fvmptdf  5652  fvmptt  5656  fcof1  5833  oveq1  5932  oveq2  5933  fvoveq1d  5947  caofinvl  6165  op1stg  6217  op2ndg  6218  ot1stg  6219  ot2ndg  6220  eloprabi  6263  1stconst  6288  algrflemg  6297  tfrlem1  6375  tfrlem3ag  6376  tfrlem3a  6377  tfrlem9  6386  tfr0dm  6389  tfrlemisucaccv  6392  tfrlemiubacc  6397  tfrlemiex  6398  tfrlemi1  6399  tfr1onlem3ag  6404  tfr1onlemsucaccv  6408  tfr1onlemubacc  6413  tfr1onlemex  6414  tfr1onlemaccex  6415  tfrcllemsucaccv  6421  tfrcllembxssdm  6423  tfrcllemubacc  6426  tfrcllemex  6427  tfrcllemaccex  6428  tfrcllemres  6429  tfrcldm  6430  rdgivallem  6448  rdgival  6449  rdgss  6450  rdgisuc1  6451  rdgon  6453  rdg0  6454  frec0g  6464  frecabcl  6466  freccllem  6469  frecfcllem  6471  frecsuclem  6473  frecsuc  6474  frecrdg  6475  oav2  6530  omv2  6532  xpdom2  6899  xpmapenlem  6919  xpmapen  6920  ac6sfi  6968  1stinl  7149  2ndinl  7150  1stinr  7151  2ndinr  7152  updjudhcoinlf  7155  updjudhcoinrg  7156  caseinl  7166  caseinr  7167  omp1eomlem  7169  omp1eom  7170  difinfsn  7175  ctmlemr  7183  ctm  7184  ctssdclemn0  7185  ctssdccl  7186  nninfninc  7198  nnnninfeq  7203  nnnninfeq2  7204  enomnilem  7213  enmkvlem  7236  enwomnilem  7244  exmidfodomrlemeldju  7278  exmidfodomrlemreseldju  7279  exmidfodomrlemr  7281  exmidfodomrlemrALT  7282  exmidaclem  7291  cc2  7350  cc3  7351  ltdfpr  7590  genpelvl  7596  genpelvu  7597  recexpr  7722  cauappcvgprlem1  7743  caucvgprlemnkj  7750  caucvgprlemnbj  7751  caucvgprlemm  7752  caucvgprlemdisj  7758  caucvgprlemloc  7759  caucvgprlemcl  7760  caucvgprlemladdfu  7761  caucvgprlemladdrl  7762  caucvgprlem1  7763  caucvgprlem2  7764  caucvgpr  7766  caucvgprprlemell  7769  caucvgprprlemelu  7770  caucvgprprlemcbv  7771  caucvgprprlemval  7772  caucvgprprlemnkeqj  7774  caucvgprprlemmu  7779  caucvgprprlemopl  7781  caucvgprprlemlol  7782  caucvgprprlemopu  7783  caucvgprprlemloc  7787  caucvgprprlemclphr  7789  caucvgprprlemexbt  7790  caucvgprprlem1  7793  caucvgprprlem2  7794  caucvgsr  7886  axcaucvglemval  7981  axcaucvglemres  7983  fv0p1e1  9122  uzin  9651  cnref1o  9742  fzsuc2  10171  fseq1m1p1  10187  fzoss2  10265  elfzonlteqm1  10303  divfl0  10403  flqzadd  10405  fldiv4p1lem1div2  10412  ceilqval  10415  flqdiv  10430  modqval  10433  modqfrac  10446  modqmulnn  10451  modqid  10458  modqcyc  10468  modqdi  10501  frec2uzuzd  10511  frec2uzrdg  10518  frecuzrdgrcl  10519  frecuzrdgtcl  10521  frecuzrdgsuc  10523  frecuzrdgrclt  10524  frecuzrdgg  10525  frecuzrdgfunlem  10528  frecuzrdgsuctlem  10532  iseqovex  10567  iseqvalcbv  10568  seq3val  10569  seqvalcd  10570  seq3m1  10582  seq3shft2  10590  seqshft2g  10591  monoord  10594  monoord2  10595  iseqf1olemqval  10609  iseqf1olemab  10611  iseqf1olemqk  10616  iseqf1olemjpcl  10617  iseqf1olemqpcl  10618  iseqf1olemfvp  10619  seq3f1olemqsumkj  10620  seq3f1olemqsumk  10621  seq3f1olemqsum  10622  seq3f1olemp  10624  seq3f1oleml  10625  seqf1oglem1  10628  seqf1oglem2  10629  seqf1og  10630  seq3homo  10636  seqhomog  10639  exp3val  10650  expnegap0  10656  facnn2  10843  facwordi  10849  faclbnd6  10853  bcval  10858  bccmpl  10863  bcn0  10864  bcm1k  10869  bcp1n  10870  bcn2  10873  hashinfom  10887  hashennn  10889  hashsng  10907  omgadd  10911  hashprg  10917  fihashssdif  10927  hashdifpr  10929  hashfzo  10931  hashfzp1  10933  hashxp  10935  zfz1isolemiso  10948  zfz1iso  10950  shftval2  11008  shftval3  11009  shftval4  11010  shftval5  11011  seq3shft  11020  imval  11032  imre  11033  reim  11034  crim  11040  reim0  11043  mulreap  11046  recj  11049  reneg  11050  readd  11051  resub  11052  remullem  11053  redivap  11056  imcj  11057  imneg  11058  imadd  11059  imsub  11060  imdivap  11063  cjsub  11074  cjexp  11075  cjreim2  11086  cjap  11088  cjdivap  11091  cnrecnv  11092  cvg1nlemcau  11166  cvg1nlemres  11167  absval  11183  rennim  11184  sqrtdiv  11224  sqrtmsq  11227  absneg  11232  abscj  11234  absval2  11239  absreim  11250  absmul  11251  absdivap  11252  absid  11253  absre  11259  absexp  11261  absexpzap  11262  absimle  11266  abssub  11283  abs3dif  11287  abs2dif  11288  abs2dif2  11289  recan  11291  cau3lem  11296  max0addsup  11401  minabs  11418  bdtrilem  11421  clim  11463  clim2  11465  clim0  11467  clim0c  11468  climi0  11471  climconst  11472  climshftlemg  11484  climcn1  11490  climcn2  11491  addcn2  11492  subcn2  11493  mulcn2  11494  reccn2ap  11495  cjcn2  11498  recn2  11499  imcn2  11500  iser3shft  11528  climcau  11529  climcvg1nlem  11531  climcvg1n  11532  serf0  11534  summodclem3  11562  summodclem2a  11563  summodc  11565  fsumf1o  11572  sumsnf  11591  fsumm1  11598  fsumcnv  11619  fsumabs  11647  fsumrelem  11653  iserabs  11657  hash2iun1dif1  11662  isumshft  11672  isumsplit  11673  expcnvap0  11684  expcnv  11686  cvgratnnlemseq  11708  cvgratnnlemrate  11712  cvgratz  11714  mertenslemub  11716  mertenslemi1  11717  mertenslem2  11718  mertensabs  11719  prodmodclem3  11757  fprodf1o  11770  prodsnf  11774  fprodm1  11780  fprodabs  11798  fprodcnv  11807  efcllemp  11840  efcj  11855  efaddlem  11856  efcan  11858  efsub  11863  efexp  11864  efzval  11865  efgt0  11866  eftlub  11872  efltim  11880  sinval  11884  cosval  11885  tanval3ap  11896  resinval  11897  recosval  11898  resin4p  11900  recos4p  11901  sinneg  11908  cosneg  11909  efmival  11915  efeul  11916  sinadd  11918  cosadd  11919  sinsub  11922  cossub  11923  addsin  11924  subsin  11925  addcos  11928  subcos  11929  sincossq  11930  sin2t  11931  cos2t  11932  sin01bnd  11939  cos01bnd  11940  sin02gt0  11946  cos12dec  11950  absefi  11951  absef  11952  absefib  11953  efieq1re  11954  demoivre  11955  demoivreALT  11956  flodddiv4  12118  bitsval  12125  bits0  12130  bitsp1  12133  bitsp1e  12134  bitsp1o  12135  bitsmod  12138  nninfctlemfo  12232  alginv  12240  algcvg  12241  eucalgval  12247  eucalginv  12249  eucalglt  12250  eucalgcvga  12251  eucalg  12252  lcmgcd  12271  lcm1  12274  sqpweven  12368  2sqpwodd  12369  sqne2sq  12370  qnumval  12378  qdenval  12379  qden1elz  12398  nn0sqrtelqelz  12399  phival  12406  dfphi2  12413  phiprmpw  12415  phiprm  12416  eulerthlemth  12425  hashgcdeq  12433  phisum  12434  pythagtriplem6  12464  pythagtriplem7  12465  pythagtriplem12  12469  pythagtriplem14  12471  fldivp1  12542  4sqlem11  12595  ennnfonelemg  12645  ennnfonelemp1  12648  ennnfonelemkh  12654  ennnfonelemhf1o  12655  ennnfonelemnn0  12664  ctinfomlemom  12669  ctiunctlemu1st  12676  ctiunctlemu2nd  12677  ctiunctlemudc  12679  ctiunctlemfo  12681  isstruct2im  12713  isstruct2r  12714  setsslid  12754  ressbasd  12770  resseqnbasd  12776  ressplusgd  12831  ptex  12966  prdsex  12971  prdsval  12975  prdsbas3  12989  pwsval  12993  pwsbas  12994  pwsplusgval  12997  pwsmulrval  12998  imasex  13007  imasival  13008  f1ocpbl  13013  f1ovscpbl  13014  imasaddvallemg  13017  qusval  13025  fvprif  13045  xpsff1o  13051  igsumvalx  13091  gsumprval  13101  pws0g  13153  imasmnd  13155  ismhm  13163  mhmpropd  13168  mhmlin  13169  mhmf1o  13172  resmhm  13189  mhmco  13192  gsumwmhm  13200  grpinvsub  13284  pwsinvg  13314  imasgrp2  13316  imasgrp  13317  mhmlem  13320  mhmid  13321  mhmmnd  13322  ghmgrp  13324  mulgfvalg  13327  mulgval  13328  mulgnegnn  13338  mulgneg  13346  mulgnegneg  13347  mulgm1  13348  mulginvcom  13353  mulgz  13356  mulgnndir  13357  mulgdir  13360  mulgass  13365  mhmmulg  13369  subgmulg  13394  isnsg  13408  eqgfval  13428  ghmlin  13454  ghmid  13455  ghminv  13456  ghmsub  13457  ghmmulg  13462  resghm  13466  ghmeql  13473  ablsub2inv  13517  ghmcmn  13533  invghm  13535  imasabl  13542  gsumfzreidx  13543  gsumfzmhm  13549  mgpplusgg  13556  mgpbasg  13558  mgpscag  13559  mgptsetg  13560  mgpdsg  13562  rngm2neg  13581  imasrng  13588  isring  13632  ringm2neg  13687  imasring  13696  opprmulfvalg  13702  opprsllem  13706  isunitd  13738  opprunitd  13742  invrfvald  13754  rdivmuldivd  13776  rhmmul  13796  isrhm2d  13797  rhm1  13799  rhmdvdsr  13807  rhmopp  13808  rhmunitinv  13810  islmod  13923  islmodd  13925  scaffvalg  13938  lmodpropd  13981  lsssetm  13988  islssmd  13991  lssats2  14046  lspsnneg  14052  lspsnsub  14053  lspun0  14057  lmodindp1  14060  sralemg  14070  srascag  14074  sravscag  14075  sraipg  14076  rlmscabas  14092  ixpsnbasval  14098  2idlval  14134  2idlvalg  14135  mulgrhm2  14242  zlmlemg  14260  zlmsca  14264  zlmvscag  14265  znval  14268  znle  14269  znbaslemnn  14271  znidomb  14290  psrval  14296  psrbasg  14303  psrplusgg  14306  istps  14352  tpspropd  14356  eltpsg  14360  txvalex  14574  txval  14575  txbasval  14587  upxp  14592  uptx  14594  txrest  14596  cnmpt11  14603  cnmpt21  14611  hmeontr  14633  txhmeo  14639  psmetxrge0  14652  xmetunirn  14678  mopnval  14762  mopntopon  14763  isxms  14771  isxms2  14772  isms  14773  msrtri  14796  xmspropd  14797  mspropd  14798  setsmsbasg  14799  setsmsdsg  14800  setsmstsetg  14801  comet  14819  metcnpi  14835  metcnpi2  14836  cnbl0  14854  cnblcld  14855  resubmet  14876  mpomulcn  14886  elcncf  14893  cncfi  14898  rescncf  14901  mulc1cncf  14909  cncfco  14911  cncfmptid  14917  addccncf  14920  cdivcncfap  14924  negcncf  14925  mulcncflem  14927  ivthinclemlopn  14956  ivthinclemuopn  14958  limccl  14979  ellimc3apf  14980  limcimolemlt  14984  cnplimclemle  14988  limccnpcntop  14995  reldvg  14999  dvfvalap  15001  dveflem  15046  dvef  15047  plymullem1  15068  plycjlemc  15080  plycj  15081  plyrecj  15083  plyreres  15084  sin0pilem1  15101  ef2kpi  15126  sinperlem  15128  sin2kpi  15131  cos2kpi  15132  sin2pim  15133  cos2pim  15134  ptolemy  15144  sincosq2sgn  15147  sincosq3sgn  15148  sincosq4sgn  15149  sinq12gt0  15150  tangtx  15158  sincosq1eq  15159  abssinper  15166  sinkpi  15167  coskpi  15168  cosq34lt1  15170  relogeftb  15185  relogoprlem  15188  relogexp  15192  rpcxpef  15214  logcxp  15217  1cxp  15220  ecxp  15221  rpcxpadd  15225  rpmulcxp  15229  cxpmul  15232  abscxp  15235  logsqrt  15243  rpabscxpbnd  15260  rpcxplogb  15284  lgsval  15329  lgsval2lem  15335  lgsval4a  15347  lgsdi  15362  lgseisenlem3  15397  lgseisenlem4  15398  lgsquadlem1  15402  lgsquadlem2  15403  lgsquadlem3  15404  2lgslem1  15416  2lgslem3a  15418  2lgslem3b  15419  2lgslem3c  15420  2lgslem3d  15421  nnsf  15736  peano4nninf  15737  peano3nninf  15738  nninfalllem1  15739  nninfall  15740  nninfsellemdc  15741  nninfsellemeq  15745  nninfsellemqall  15746  nninfsellemeqinf  15747  nninfsel  15748  exmidsbthr  15754  qdencn  15758  refeq  15759  isomninnlem  15761  apdifflemr  15778  apdiff  15779  ismkvnnlem  15783  nconstwlpolem  15796