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  7280  exmidfodomrlemreseldju  7281  exmidfodomrlemr  7283  exmidfodomrlemrALT  7284  exmidaclem  7293  cc2  7352  cc3  7353  ltdfpr  7592  genpelvl  7598  genpelvu  7599  recexpr  7724  cauappcvgprlem1  7745  caucvgprlemnkj  7752  caucvgprlemnbj  7753  caucvgprlemm  7754  caucvgprlemdisj  7760  caucvgprlemloc  7761  caucvgprlemcl  7762  caucvgprlemladdfu  7763  caucvgprlemladdrl  7764  caucvgprlem1  7765  caucvgprlem2  7766  caucvgpr  7768  caucvgprprlemell  7771  caucvgprprlemelu  7772  caucvgprprlemcbv  7773  caucvgprprlemval  7774  caucvgprprlemnkeqj  7776  caucvgprprlemmu  7781  caucvgprprlemopl  7783  caucvgprprlemlol  7784  caucvgprprlemopu  7785  caucvgprprlemloc  7789  caucvgprprlemclphr  7791  caucvgprprlemexbt  7792  caucvgprprlem1  7795  caucvgprprlem2  7796  caucvgsr  7888  axcaucvglemval  7983  axcaucvglemres  7985  fv0p1e1  9124  uzin  9653  cnref1o  9744  fzsuc2  10173  fseq1m1p1  10189  fzoss2  10267  elfzonlteqm1  10305  divfl0  10405  flqzadd  10407  fldiv4p1lem1div2  10414  ceilqval  10417  flqdiv  10432  modqval  10435  modqfrac  10448  modqmulnn  10453  modqid  10460  modqcyc  10470  modqdi  10503  frec2uzuzd  10513  frec2uzrdg  10520  frecuzrdgrcl  10521  frecuzrdgtcl  10523  frecuzrdgsuc  10525  frecuzrdgrclt  10526  frecuzrdgg  10527  frecuzrdgfunlem  10530  frecuzrdgsuctlem  10534  iseqovex  10569  iseqvalcbv  10570  seq3val  10571  seqvalcd  10572  seq3m1  10584  seq3shft2  10592  seqshft2g  10593  monoord  10596  monoord2  10597  iseqf1olemqval  10611  iseqf1olemab  10613  iseqf1olemqk  10618  iseqf1olemjpcl  10619  iseqf1olemqpcl  10620  iseqf1olemfvp  10621  seq3f1olemqsumkj  10622  seq3f1olemqsumk  10623  seq3f1olemqsum  10624  seq3f1olemp  10626  seq3f1oleml  10627  seqf1oglem1  10630  seqf1oglem2  10631  seqf1og  10632  seq3homo  10638  seqhomog  10641  exp3val  10652  expnegap0  10658  facnn2  10845  facwordi  10851  faclbnd6  10855  bcval  10860  bccmpl  10865  bcn0  10866  bcm1k  10871  bcp1n  10872  bcn2  10875  hashinfom  10889  hashennn  10891  hashsng  10909  omgadd  10913  hashprg  10919  fihashssdif  10929  hashdifpr  10931  hashfzo  10933  hashfzp1  10935  hashxp  10937  zfz1isolemiso  10950  zfz1iso  10952  shftval2  11010  shftval3  11011  shftval4  11012  shftval5  11013  seq3shft  11022  imval  11034  imre  11035  reim  11036  crim  11042  reim0  11045  mulreap  11048  recj  11051  reneg  11052  readd  11053  resub  11054  remullem  11055  redivap  11058  imcj  11059  imneg  11060  imadd  11061  imsub  11062  imdivap  11065  cjsub  11076  cjexp  11077  cjreim2  11088  cjap  11090  cjdivap  11093  cnrecnv  11094  cvg1nlemcau  11168  cvg1nlemres  11169  absval  11185  rennim  11186  sqrtdiv  11226  sqrtmsq  11229  absneg  11234  abscj  11236  absval2  11241  absreim  11252  absmul  11253  absdivap  11254  absid  11255  absre  11261  absexp  11263  absexpzap  11264  absimle  11268  abssub  11285  abs3dif  11289  abs2dif  11290  abs2dif2  11291  recan  11293  cau3lem  11298  max0addsup  11403  minabs  11420  bdtrilem  11423  clim  11465  clim2  11467  clim0  11469  clim0c  11470  climi0  11473  climconst  11474  climshftlemg  11486  climcn1  11492  climcn2  11493  addcn2  11494  subcn2  11495  mulcn2  11496  reccn2ap  11497  cjcn2  11500  recn2  11501  imcn2  11502  iser3shft  11530  climcau  11531  climcvg1nlem  11533  climcvg1n  11534  serf0  11536  summodclem3  11564  summodclem2a  11565  summodc  11567  fsumf1o  11574  sumsnf  11593  fsumm1  11600  fsumcnv  11621  fsumabs  11649  fsumrelem  11655  iserabs  11659  hash2iun1dif1  11664  isumshft  11674  isumsplit  11675  expcnvap0  11686  expcnv  11688  cvgratnnlemseq  11710  cvgratnnlemrate  11714  cvgratz  11716  mertenslemub  11718  mertenslemi1  11719  mertenslem2  11720  mertensabs  11721  prodmodclem3  11759  fprodf1o  11772  prodsnf  11776  fprodm1  11782  fprodabs  11800  fprodcnv  11809  efcllemp  11842  efcj  11857  efaddlem  11858  efcan  11860  efsub  11865  efexp  11866  efzval  11867  efgt0  11868  eftlub  11874  efltim  11882  sinval  11886  cosval  11887  tanval3ap  11898  resinval  11899  recosval  11900  resin4p  11902  recos4p  11903  sinneg  11910  cosneg  11911  efmival  11917  efeul  11918  sinadd  11920  cosadd  11921  sinsub  11924  cossub  11925  addsin  11926  subsin  11927  addcos  11930  subcos  11931  sincossq  11932  sin2t  11933  cos2t  11934  sin01bnd  11941  cos01bnd  11942  sin02gt0  11948  cos12dec  11952  absefi  11953  absef  11954  absefib  11955  efieq1re  11956  demoivre  11957  demoivreALT  11958  flodddiv4  12120  bitsval  12127  bits0  12132  bitsp1  12135  bitsp1e  12136  bitsp1o  12137  bitsmod  12140  nninfctlemfo  12234  alginv  12242  algcvg  12243  eucalgval  12249  eucalginv  12251  eucalglt  12252  eucalgcvga  12253  eucalg  12254  lcmgcd  12273  lcm1  12276  sqpweven  12370  2sqpwodd  12371  sqne2sq  12372  qnumval  12380  qdenval  12381  qden1elz  12400  nn0sqrtelqelz  12401  phival  12408  dfphi2  12415  phiprmpw  12417  phiprm  12418  eulerthlemth  12427  hashgcdeq  12435  phisum  12436  pythagtriplem6  12466  pythagtriplem7  12467  pythagtriplem12  12471  pythagtriplem14  12473  fldivp1  12544  4sqlem11  12597  ennnfonelemg  12647  ennnfonelemp1  12650  ennnfonelemkh  12656  ennnfonelemhf1o  12657  ennnfonelemnn0  12666  ctinfomlemom  12671  ctiunctlemu1st  12678  ctiunctlemu2nd  12679  ctiunctlemudc  12681  ctiunctlemfo  12683  isstruct2im  12715  isstruct2r  12716  setsslid  12756  ressbasd  12772  resseqnbasd  12778  ressplusgd  12833  ptex  12968  prdsex  12973  prdsval  12977  prdsbas3  12991  pwsval  12995  pwsbas  12996  pwsplusgval  12999  pwsmulrval  13000  imasex  13009  imasival  13010  f1ocpbl  13015  f1ovscpbl  13016  imasaddvallemg  13019  qusval  13027  fvprif  13047  xpsff1o  13053  igsumvalx  13093  gsumprval  13103  pws0g  13155  imasmnd  13157  ismhm  13165  mhmpropd  13170  mhmlin  13171  mhmf1o  13174  resmhm  13191  mhmco  13194  gsumwmhm  13202  grpinvsub  13286  pwsinvg  13316  imasgrp2  13318  imasgrp  13319  mhmlem  13322  mhmid  13323  mhmmnd  13324  ghmgrp  13326  mulgfvalg  13329  mulgval  13330  mulgnegnn  13340  mulgneg  13348  mulgnegneg  13349  mulgm1  13350  mulginvcom  13355  mulgz  13358  mulgnndir  13359  mulgdir  13362  mulgass  13367  mhmmulg  13371  subgmulg  13396  isnsg  13410  eqgfval  13430  ghmlin  13456  ghmid  13457  ghminv  13458  ghmsub  13459  ghmmulg  13464  resghm  13468  ghmeql  13475  ablsub2inv  13519  ghmcmn  13535  invghm  13537  imasabl  13544  gsumfzreidx  13545  gsumfzmhm  13551  mgpplusgg  13558  mgpbasg  13560  mgpscag  13561  mgptsetg  13562  mgpdsg  13564  rngm2neg  13583  imasrng  13590  isring  13634  ringm2neg  13689  imasring  13698  opprmulfvalg  13704  opprsllem  13708  isunitd  13740  opprunitd  13744  invrfvald  13756  rdivmuldivd  13778  rhmmul  13798  isrhm2d  13799  rhm1  13801  rhmdvdsr  13809  rhmopp  13810  rhmunitinv  13812  islmod  13925  islmodd  13927  scaffvalg  13940  lmodpropd  13983  lsssetm  13990  islssmd  13993  lssats2  14048  lspsnneg  14054  lspsnsub  14055  lspun0  14059  lmodindp1  14062  sralemg  14072  srascag  14076  sravscag  14077  sraipg  14078  rlmscabas  14094  ixpsnbasval  14100  2idlval  14136  2idlvalg  14137  mulgrhm2  14244  zlmlemg  14262  zlmsca  14266  zlmvscag  14267  znval  14270  znle  14271  znbaslemnn  14273  znidomb  14292  psrval  14300  psrbasg  14308  psrplusgg  14312  mplvalcoe  14324  mplsubgfileminv  14334  mpl0fi  14336  mplnegfi  14339  istps  14376  tpspropd  14380  eltpsg  14384  txvalex  14598  txval  14599  txbasval  14611  upxp  14616  uptx  14618  txrest  14620  cnmpt11  14627  cnmpt21  14635  hmeontr  14657  txhmeo  14663  psmetxrge0  14676  xmetunirn  14702  mopnval  14786  mopntopon  14787  isxms  14795  isxms2  14796  isms  14797  msrtri  14820  xmspropd  14821  mspropd  14822  setsmsbasg  14823  setsmsdsg  14824  setsmstsetg  14825  comet  14843  metcnpi  14859  metcnpi2  14860  cnbl0  14878  cnblcld  14879  resubmet  14900  mpomulcn  14910  elcncf  14917  cncfi  14922  rescncf  14925  mulc1cncf  14933  cncfco  14935  cncfmptid  14941  addccncf  14944  cdivcncfap  14948  negcncf  14949  mulcncflem  14951  ivthinclemlopn  14980  ivthinclemuopn  14982  limccl  15003  ellimc3apf  15004  limcimolemlt  15008  cnplimclemle  15012  limccnpcntop  15019  reldvg  15023  dvfvalap  15025  dveflem  15070  dvef  15071  plymullem1  15092  plycjlemc  15104  plycj  15105  plyrecj  15107  plyreres  15108  sin0pilem1  15125  ef2kpi  15150  sinperlem  15152  sin2kpi  15155  cos2kpi  15156  sin2pim  15157  cos2pim  15158  ptolemy  15168  sincosq2sgn  15171  sincosq3sgn  15172  sincosq4sgn  15173  sinq12gt0  15174  tangtx  15182  sincosq1eq  15183  abssinper  15190  sinkpi  15191  coskpi  15192  cosq34lt1  15194  relogeftb  15209  relogoprlem  15212  relogexp  15216  rpcxpef  15238  logcxp  15241  1cxp  15244  ecxp  15245  rpcxpadd  15249  rpmulcxp  15253  cxpmul  15256  abscxp  15259  logsqrt  15267  rpabscxpbnd  15284  rpcxplogb  15308  lgsval  15353  lgsval2lem  15359  lgsval4a  15371  lgsdi  15386  lgseisenlem3  15421  lgseisenlem4  15422  lgsquadlem1  15426  lgsquadlem2  15427  lgsquadlem3  15428  2lgslem1  15440  2lgslem3a  15442  2lgslem3b  15443  2lgslem3c  15444  2lgslem3d  15445  nnsf  15760  peano4nninf  15761  peano3nninf  15762  nninfalllem1  15763  nninfall  15764  nninfsellemdc  15765  nninfsellemeq  15769  nninfsellemqall  15770  nninfsellemeqinf  15771  nninfsel  15772  nnnninfex  15777  exmidsbthr  15780  qdencn  15784  refeq  15785  isomninnlem  15787  apdifflemr  15804  apdiff  15805  ismkvnnlem  15809  nconstwlpolem  15822