Theorem fveq2d 5630

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

Syntax hints:   → wi 4   = wceq 1395  ‘cfv 5317

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 714  ax-5 1493  ax-7 1494  ax-gen 1495  ax-ie1 1539  ax-ie2 1540  ax-8 1550  ax-10 1551  ax-11 1552  ax-i12 1553  ax-bndl 1555  ax-4 1556  ax-17 1572  ax-i9 1576  ax-ial 1580  ax-i5r 1581  ax-ext 2211

This theorem depends on definitions:  df-bi 117  df-3an 1004  df-tru 1398  df-nf 1507  df-sb 1809  df-clab 2216  df-cleq 2222  df-clel 2225  df-nfc 2361  df-rex 2514  df-v 2801  df-un 3201  df-sn 3672  df-pr 3673  df-op 3675  df-uni 3888  df-br 4083  df-iota 5277  df-fv 5325

This theorem is referenced by:  2fveq3  5631  fveq12d  5633  fveqeq2d  5634  csbfvg  5668  fvmptdf  5721  fvmptt  5725  fcof1  5906  oveq1  6007  oveq2  6008  fvoveq1d  6022  caofinvl  6242  op1stg  6294  op2ndg  6295  ot1stg  6296  ot2ndg  6297  eloprabi  6340  1stconst  6365  algrflemg  6374  tfrlem1  6452  tfrlem3ag  6453  tfrlem3a  6454  tfrlem9  6463  tfr0dm  6466  tfrlemisucaccv  6469  tfrlemiubacc  6474  tfrlemiex  6475  tfrlemi1  6476  tfr1onlem3ag  6481  tfr1onlemsucaccv  6485  tfr1onlemubacc  6490  tfr1onlemex  6491  tfr1onlemaccex  6492  tfrcllemsucaccv  6498  tfrcllembxssdm  6500  tfrcllemubacc  6503  tfrcllemex  6504  tfrcllemaccex  6505  tfrcllemres  6506  tfrcldm  6507  rdgivallem  6525  rdgival  6526  rdgss  6527  rdgisuc1  6528  rdgon  6530  rdg0  6531  frec0g  6541  frecabcl  6543  freccllem  6546  frecfcllem  6548  frecsuclem  6550  frecsuc  6551  frecrdg  6552  oav2  6607  omv2  6609  xpdom2  6986  xpmapenlem  7006  xpmapen  7007  ac6sfi  7056  1stinl  7237  2ndinl  7238  1stinr  7239  2ndinr  7240  updjudhcoinlf  7243  updjudhcoinrg  7244  caseinl  7254  caseinr  7255  omp1eomlem  7257  omp1eom  7258  difinfsn  7263  ctmlemr  7271  ctm  7272  ctssdclemn0  7273  ctssdccl  7274  nninfninc  7286  nnnninfeq  7291  nnnninfeq2  7292  enomnilem  7301  enmkvlem  7324  enwomnilem  7332  exmidfodomrlemeldju  7373  exmidfodomrlemreseldju  7374  exmidfodomrlemr  7376  exmidfodomrlemrALT  7377  exmidaclem  7386  cc2  7449  cc3  7450  ltdfpr  7689  genpelvl  7695  genpelvu  7696  recexpr  7821  cauappcvgprlem1  7842  caucvgprlemnkj  7849  caucvgprlemnbj  7850  caucvgprlemm  7851  caucvgprlemdisj  7857  caucvgprlemloc  7858  caucvgprlemcl  7859  caucvgprlemladdfu  7860  caucvgprlemladdrl  7861  caucvgprlem1  7862  caucvgprlem2  7863  caucvgpr  7865  caucvgprprlemell  7868  caucvgprprlemelu  7869  caucvgprprlemcbv  7870  caucvgprprlemval  7871  caucvgprprlemnkeqj  7873  caucvgprprlemmu  7878  caucvgprprlemopl  7880  caucvgprprlemlol  7881  caucvgprprlemopu  7882  caucvgprprlemloc  7886  caucvgprprlemclphr  7888  caucvgprprlemexbt  7889  caucvgprprlem1  7892  caucvgprprlem2  7893  caucvgsr  7985  axcaucvglemval  8080  axcaucvglemres  8082  fv0p1e1  9221  uzin  9751  cnref1o  9842  fzsuc2  10271  fseq1m1p1  10287  fzoss2  10366  elfzonlteqm1  10411  divfl0  10511  flqzadd  10513  fldiv4p1lem1div2  10520  ceilqval  10523  flqdiv  10538  modqval  10541  modqfrac  10554  modqmulnn  10559  modqid  10566  modqcyc  10576  modqdi  10609  frec2uzuzd  10619  frec2uzrdg  10626  frecuzrdgrcl  10627  frecuzrdgtcl  10629  frecuzrdgsuc  10631  frecuzrdgrclt  10632  frecuzrdgg  10633  frecuzrdgfunlem  10636  frecuzrdgsuctlem  10640  iseqovex  10675  iseqvalcbv  10676  seq3val  10677  seqvalcd  10678  seq3m1  10690  seq3shft2  10698  seqshft2g  10699  monoord  10702  monoord2  10703  iseqf1olemqval  10717  iseqf1olemab  10719  iseqf1olemqk  10724  iseqf1olemjpcl  10725  iseqf1olemqpcl  10726  iseqf1olemfvp  10727  seq3f1olemqsumkj  10728  seq3f1olemqsumk  10729  seq3f1olemqsum  10730  seq3f1olemp  10732  seq3f1oleml  10733  seqf1oglem1  10736  seqf1oglem2  10737  seqf1og  10738  seq3homo  10744  seqhomog  10747  exp3val  10758  expnegap0  10764  facnn2  10951  facwordi  10957  faclbnd6  10961  bcval  10966  bccmpl  10971  bcn0  10972  bcm1k  10977  bcp1n  10978  bcn2  10981  hashinfom  10995  hashennn  10997  hashsng  11015  omgadd  11019  hashprg  11025  fihashssdif  11035  hashdifpr  11037  hashfzo  11039  hashfzp1  11041  hashxp  11043  zfz1isolemiso  11056  zfz1iso  11058  lsw1  11116  ccatfvalfi  11122  ccatlen  11125  ccatval3  11129  ccatval21sw  11135  ccatlid  11136  ccatass  11138  lswccatn0lsw  11141  lswccat0lsw  11142  s1leng  11152  ccats1val2  11166  lswccats1  11169  swrdfv0  11181  swrdfv2  11190  swrdsbslen  11193  swrds1  11195  ccatswrd  11197  pfxmpt  11207  pfxfv  11211  pfxtrcfvl  11224  ccatpfx  11228  swrdswrd  11232  lenpfxcctswrd  11238  ccatopth  11243  cats1un  11248  swrdccatin2  11256  pfxccatin12lem2  11258  shftval2  11332  shftval3  11333  shftval4  11334  shftval5  11335  seq3shft  11344  imval  11356  imre  11357  reim  11358  crim  11364  reim0  11367  mulreap  11370  recj  11373  reneg  11374  readd  11375  resub  11376  remullem  11377  redivap  11380  imcj  11381  imneg  11382  imadd  11383  imsub  11384  imdivap  11387  cjsub  11398  cjexp  11399  cjreim2  11410  cjap  11412  cjdivap  11415  cnrecnv  11416  cvg1nlemcau  11490  cvg1nlemres  11491  absval  11507  rennim  11508  sqrtdiv  11548  sqrtmsq  11551  absneg  11556  abscj  11558  absval2  11563  absreim  11574  absmul  11575  absdivap  11576  absid  11577  absre  11583  absexp  11585  absexpzap  11586  absimle  11590  abssub  11607  abs3dif  11611  abs2dif  11612  abs2dif2  11613  recan  11615  cau3lem  11620  max0addsup  11725  minabs  11742  bdtrilem  11745  clim  11787  clim2  11789  clim0  11791  clim0c  11792  climi0  11795  climconst  11796  climshftlemg  11808  climcn1  11814  climcn2  11815  addcn2  11816  subcn2  11817  mulcn2  11818  reccn2ap  11819  cjcn2  11822  recn2  11823  imcn2  11824  iser3shft  11852  climcau  11853  climcvg1nlem  11855  climcvg1n  11856  serf0  11858  summodclem3  11886  summodclem2a  11887  summodc  11889  fsumf1o  11896  sumsnf  11915  fsumm1  11922  fsumcnv  11943  fsumabs  11971  fsumrelem  11977  iserabs  11981  hash2iun1dif1  11986  isumshft  11996  isumsplit  11997  expcnvap0  12008  expcnv  12010  cvgratnnlemseq  12032  cvgratnnlemrate  12036  cvgratz  12038  mertenslemub  12040  mertenslemi1  12041  mertenslem2  12042  mertensabs  12043  prodmodclem3  12081  fprodf1o  12094  prodsnf  12098  fprodm1  12104  fprodabs  12122  fprodcnv  12131  efcllemp  12164  efcj  12179  efaddlem  12180  efcan  12182  efsub  12187  efexp  12188  efzval  12189  efgt0  12190  eftlub  12196  efltim  12204  sinval  12208  cosval  12209  tanval3ap  12220  resinval  12221  recosval  12222  resin4p  12224  recos4p  12225  sinneg  12232  cosneg  12233  efmival  12239  efeul  12240  sinadd  12242  cosadd  12243  sinsub  12246  cossub  12247  addsin  12248  subsin  12249  addcos  12252  subcos  12253  sincossq  12254  sin2t  12255  cos2t  12256  sin01bnd  12263  cos01bnd  12264  sin02gt0  12270  cos12dec  12274  absefi  12275  absef  12276  absefib  12277  efieq1re  12278  demoivre  12279  demoivreALT  12280  flodddiv4  12442  bitsval  12449  bits0  12454  bitsp1  12457  bitsp1e  12458  bitsp1o  12459  bitsmod  12462  nninfctlemfo  12556  alginv  12564  algcvg  12565  eucalgval  12571  eucalginv  12573  eucalglt  12574  eucalgcvga  12575  eucalg  12576  lcmgcd  12595  lcm1  12598  sqpweven  12692  2sqpwodd  12693  sqne2sq  12694  qnumval  12702  qdenval  12703  qden1elz  12722  nn0sqrtelqelz  12723  phival  12730  dfphi2  12737  phiprmpw  12739  phiprm  12740  eulerthlemth  12749  hashgcdeq  12757  phisum  12758  pythagtriplem6  12788  pythagtriplem7  12789  pythagtriplem12  12793  pythagtriplem14  12795  fldivp1  12866  4sqlem11  12919  ennnfonelemg  12969  ennnfonelemp1  12972  ennnfonelemkh  12978  ennnfonelemhf1o  12979  ennnfonelemnn0  12988  ctinfomlemom  12993  ctiunctlemu1st  13000  ctiunctlemu2nd  13001  ctiunctlemudc  13003  ctiunctlemfo  13005  isstruct2im  13037  isstruct2r  13038  setsslid  13078  ressbasd  13095  resseqnbasd  13101  ressplusgd  13157  ptex  13292  prdsex  13297  prdsval  13301  prdsbas3  13315  pwsval  13319  pwsbas  13320  pwsplusgval  13323  pwsmulrval  13324  imasex  13333  imasival  13334  f1ocpbl  13339  f1ovscpbl  13340  imasaddvallemg  13343  qusval  13351  fvprif  13371  xpsff1o  13377  igsumvalx  13417  gsumprval  13427  pws0g  13479  imasmnd  13481  ismhm  13489  mhmpropd  13494  mhmlin  13495  mhmf1o  13498  resmhm  13515  mhmco  13518  gsumwmhm  13526  grpinvsub  13610  pwsinvg  13640  imasgrp2  13642  imasgrp  13643  mhmlem  13646  mhmid  13647  mhmmnd  13648  ghmgrp  13650  mulgfvalg  13653  mulgval  13654  mulgnegnn  13664  mulgneg  13672  mulgnegneg  13673  mulgm1  13674  mulginvcom  13679  mulgz  13682  mulgnndir  13683  mulgdir  13686  mulgass  13691  mhmmulg  13695  subgmulg  13720  isnsg  13734  eqgfval  13754  ghmlin  13780  ghmid  13781  ghminv  13782  ghmsub  13783  ghmmulg  13788  resghm  13792  ghmeql  13799  ablsub2inv  13843  ghmcmn  13859  invghm  13861  imasabl  13868  gsumfzreidx  13869  gsumfzmhm  13875  mgpplusgg  13882  mgpbasg  13884  mgpscag  13885  mgptsetg  13886  mgpdsg  13888  rngm2neg  13907  imasrng  13914  isring  13958  ringm2neg  14013  imasring  14022  opprmulfvalg  14028  opprsllem  14032  isunitd  14064  opprunitd  14068  invrfvald  14080  rdivmuldivd  14102  rhmmul  14122  isrhm2d  14123  rhm1  14125  rhmdvdsr  14133  rhmopp  14134  rhmunitinv  14136  islmod  14249  islmodd  14251  scaffvalg  14264  lmodpropd  14307  lsssetm  14314  islssmd  14317  lssats2  14372  lspsnneg  14378  lspsnsub  14379  lspun0  14383  lmodindp1  14386  sralemg  14396  srascag  14400  sravscag  14401  sraipg  14402  rlmscabas  14418  ixpsnbasval  14424  2idlval  14460  2idlvalg  14461  mulgrhm2  14568  zlmlemg  14586  zlmsca  14590  zlmvscag  14591  znval  14594  znle  14595  znbaslemnn  14597  znidomb  14616  psrval  14624  psrbasg  14632  psrplusgg  14636  mplvalcoe  14648  mplsubgfileminv  14658  mpl0fi  14660  mplnegfi  14663  istps  14700  tpspropd  14704  eltpsg  14708  txvalex  14922  txval  14923  txbasval  14935  upxp  14940  uptx  14942  txrest  14944  cnmpt11  14951  cnmpt21  14959  hmeontr  14981  txhmeo  14987  psmetxrge0  15000  xmetunirn  15026  mopnval  15110  mopntopon  15111  isxms  15119  isxms2  15120  isms  15121  msrtri  15144  xmspropd  15145  mspropd  15146  setsmsbasg  15147  setsmsdsg  15148  setsmstsetg  15149  comet  15167  metcnpi  15183  metcnpi2  15184  cnbl0  15202  cnblcld  15203  resubmet  15224  mpomulcn  15234  elcncf  15241  cncfi  15246  rescncf  15249  mulc1cncf  15257  cncfco  15259  cncfmptid  15265  addccncf  15268  cdivcncfap  15272  negcncf  15273  mulcncflem  15275  ivthinclemlopn  15304  ivthinclemuopn  15306  limccl  15327  ellimc3apf  15328  limcimolemlt  15332  cnplimclemle  15336  limccnpcntop  15343  reldvg  15347  dvfvalap  15349  dveflem  15394  dvef  15395  plymullem1  15416  plycjlemc  15428  plycj  15429  plyrecj  15431  plyreres  15432  sin0pilem1  15449  ef2kpi  15474  sinperlem  15476  sin2kpi  15479  cos2kpi  15480  sin2pim  15481  cos2pim  15482  ptolemy  15492  sincosq2sgn  15495  sincosq3sgn  15496  sincosq4sgn  15497  sinq12gt0  15498  tangtx  15506  sincosq1eq  15507  abssinper  15514  sinkpi  15515  coskpi  15516  cosq34lt1  15518  relogeftb  15533  relogoprlem  15536  relogexp  15540  rpcxpef  15562  logcxp  15565  1cxp  15568  ecxp  15569  rpcxpadd  15573  rpmulcxp  15577  cxpmul  15580  abscxp  15583  logsqrt  15591  rpabscxpbnd  15608  rpcxplogb  15632  lgsval  15677  lgsval2lem  15683  lgsval4a  15695  lgsdi  15710  lgseisenlem3  15745  lgseisenlem4  15746  lgsquadlem1  15750  lgsquadlem2  15751  lgsquadlem3  15752  2lgslem1  15764  2lgslem3a  15766  2lgslem3b  15767  2lgslem3c  15768  2lgslem3d  15769  iswlk  16029  nnsf  16330  peano4nninf  16331  peano3nninf  16332  nninfalllem1  16333  nninfall  16334  nninfsellemdc  16335  nninfsellemeq  16339  nninfsellemqall  16340  nninfsellemeqinf  16341  nninfsel  16342  nnnninfex  16347  exmidsbthr  16350  qdencn  16354  refeq  16355  isomninnlem  16357  apdifflemr  16374  apdiff  16375  ismkvnnlem  16379  nconstwlpolem  16392