Theorem fveq2d 5593

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

Syntax hints:   → wi 4   = wceq 1373  ‘cfv 5280

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 711  ax-5 1471  ax-7 1472  ax-gen 1473  ax-ie1 1517  ax-ie2 1518  ax-8 1528  ax-10 1529  ax-11 1530  ax-i12 1531  ax-bndl 1533  ax-4 1534  ax-17 1550  ax-i9 1554  ax-ial 1558  ax-i5r 1559  ax-ext 2188

This theorem depends on definitions:  df-bi 117  df-3an 983  df-tru 1376  df-nf 1485  df-sb 1787  df-clab 2193  df-cleq 2199  df-clel 2202  df-nfc 2338  df-rex 2491  df-v 2775  df-un 3174  df-sn 3644  df-pr 3645  df-op 3647  df-uni 3857  df-br 4052  df-iota 5241  df-fv 5288

This theorem is referenced by:  2fveq3  5594  fveq12d  5596  fveqeq2d  5597  csbfvg  5629  fvmptdf  5680  fvmptt  5684  fcof1  5865  oveq1  5964  oveq2  5965  fvoveq1d  5979  caofinvl  6197  op1stg  6249  op2ndg  6250  ot1stg  6251  ot2ndg  6252  eloprabi  6295  1stconst  6320  algrflemg  6329  tfrlem1  6407  tfrlem3ag  6408  tfrlem3a  6409  tfrlem9  6418  tfr0dm  6421  tfrlemisucaccv  6424  tfrlemiubacc  6429  tfrlemiex  6430  tfrlemi1  6431  tfr1onlem3ag  6436  tfr1onlemsucaccv  6440  tfr1onlemubacc  6445  tfr1onlemex  6446  tfr1onlemaccex  6447  tfrcllemsucaccv  6453  tfrcllembxssdm  6455  tfrcllemubacc  6458  tfrcllemex  6459  tfrcllemaccex  6460  tfrcllemres  6461  tfrcldm  6462  rdgivallem  6480  rdgival  6481  rdgss  6482  rdgisuc1  6483  rdgon  6485  rdg0  6486  frec0g  6496  frecabcl  6498  freccllem  6501  frecfcllem  6503  frecsuclem  6505  frecsuc  6506  frecrdg  6507  oav2  6562  omv2  6564  xpdom2  6941  xpmapenlem  6961  xpmapen  6962  ac6sfi  7010  1stinl  7191  2ndinl  7192  1stinr  7193  2ndinr  7194  updjudhcoinlf  7197  updjudhcoinrg  7198  caseinl  7208  caseinr  7209  omp1eomlem  7211  omp1eom  7212  difinfsn  7217  ctmlemr  7225  ctm  7226  ctssdclemn0  7227  ctssdccl  7228  nninfninc  7240  nnnninfeq  7245  nnnninfeq2  7246  enomnilem  7255  enmkvlem  7278  enwomnilem  7286  exmidfodomrlemeldju  7323  exmidfodomrlemreseldju  7324  exmidfodomrlemr  7326  exmidfodomrlemrALT  7327  exmidaclem  7336  cc2  7399  cc3  7400  ltdfpr  7639  genpelvl  7645  genpelvu  7646  recexpr  7771  cauappcvgprlem1  7792  caucvgprlemnkj  7799  caucvgprlemnbj  7800  caucvgprlemm  7801  caucvgprlemdisj  7807  caucvgprlemloc  7808  caucvgprlemcl  7809  caucvgprlemladdfu  7810  caucvgprlemladdrl  7811  caucvgprlem1  7812  caucvgprlem2  7813  caucvgpr  7815  caucvgprprlemell  7818  caucvgprprlemelu  7819  caucvgprprlemcbv  7820  caucvgprprlemval  7821  caucvgprprlemnkeqj  7823  caucvgprprlemmu  7828  caucvgprprlemopl  7830  caucvgprprlemlol  7831  caucvgprprlemopu  7832  caucvgprprlemloc  7836  caucvgprprlemclphr  7838  caucvgprprlemexbt  7839  caucvgprprlem1  7842  caucvgprprlem2  7843  caucvgsr  7935  axcaucvglemval  8030  axcaucvglemres  8032  fv0p1e1  9171  uzin  9701  cnref1o  9792  fzsuc2  10221  fseq1m1p1  10237  fzoss2  10316  elfzonlteqm1  10361  divfl0  10461  flqzadd  10463  fldiv4p1lem1div2  10470  ceilqval  10473  flqdiv  10488  modqval  10491  modqfrac  10504  modqmulnn  10509  modqid  10516  modqcyc  10526  modqdi  10559  frec2uzuzd  10569  frec2uzrdg  10576  frecuzrdgrcl  10577  frecuzrdgtcl  10579  frecuzrdgsuc  10581  frecuzrdgrclt  10582  frecuzrdgg  10583  frecuzrdgfunlem  10586  frecuzrdgsuctlem  10590  iseqovex  10625  iseqvalcbv  10626  seq3val  10627  seqvalcd  10628  seq3m1  10640  seq3shft2  10648  seqshft2g  10649  monoord  10652  monoord2  10653  iseqf1olemqval  10667  iseqf1olemab  10669  iseqf1olemqk  10674  iseqf1olemjpcl  10675  iseqf1olemqpcl  10676  iseqf1olemfvp  10677  seq3f1olemqsumkj  10678  seq3f1olemqsumk  10679  seq3f1olemqsum  10680  seq3f1olemp  10682  seq3f1oleml  10683  seqf1oglem1  10686  seqf1oglem2  10687  seqf1og  10688  seq3homo  10694  seqhomog  10697  exp3val  10708  expnegap0  10714  facnn2  10901  facwordi  10907  faclbnd6  10911  bcval  10916  bccmpl  10921  bcn0  10922  bcm1k  10927  bcp1n  10928  bcn2  10931  hashinfom  10945  hashennn  10947  hashsng  10965  omgadd  10969  hashprg  10975  fihashssdif  10985  hashdifpr  10987  hashfzo  10989  hashfzp1  10991  hashxp  10993  zfz1isolemiso  11006  zfz1iso  11008  lsw1  11065  ccatfvalfi  11071  ccatlen  11074  ccatval3  11078  ccatval21sw  11084  ccatlid  11085  ccatass  11087  lswccatn0lsw  11090  lswccat0lsw  11091  s1leng  11101  ccats1val2  11115  lswccats1  11118  swrdfv0  11130  swrdfv2  11139  swrdsbslen  11142  swrds1  11144  ccatswrd  11146  pfxmpt  11156  pfxfv  11160  pfxtrcfvl  11173  ccatpfx  11177  swrdswrd  11181  lenpfxcctswrd  11187  ccatopth  11192  cats1un  11197  shftval2  11212  shftval3  11213  shftval4  11214  shftval5  11215  seq3shft  11224  imval  11236  imre  11237  reim  11238  crim  11244  reim0  11247  mulreap  11250  recj  11253  reneg  11254  readd  11255  resub  11256  remullem  11257  redivap  11260  imcj  11261  imneg  11262  imadd  11263  imsub  11264  imdivap  11267  cjsub  11278  cjexp  11279  cjreim2  11290  cjap  11292  cjdivap  11295  cnrecnv  11296  cvg1nlemcau  11370  cvg1nlemres  11371  absval  11387  rennim  11388  sqrtdiv  11428  sqrtmsq  11431  absneg  11436  abscj  11438  absval2  11443  absreim  11454  absmul  11455  absdivap  11456  absid  11457  absre  11463  absexp  11465  absexpzap  11466  absimle  11470  abssub  11487  abs3dif  11491  abs2dif  11492  abs2dif2  11493  recan  11495  cau3lem  11500  max0addsup  11605  minabs  11622  bdtrilem  11625  clim  11667  clim2  11669  clim0  11671  clim0c  11672  climi0  11675  climconst  11676  climshftlemg  11688  climcn1  11694  climcn2  11695  addcn2  11696  subcn2  11697  mulcn2  11698  reccn2ap  11699  cjcn2  11702  recn2  11703  imcn2  11704  iser3shft  11732  climcau  11733  climcvg1nlem  11735  climcvg1n  11736  serf0  11738  summodclem3  11766  summodclem2a  11767  summodc  11769  fsumf1o  11776  sumsnf  11795  fsumm1  11802  fsumcnv  11823  fsumabs  11851  fsumrelem  11857  iserabs  11861  hash2iun1dif1  11866  isumshft  11876  isumsplit  11877  expcnvap0  11888  expcnv  11890  cvgratnnlemseq  11912  cvgratnnlemrate  11916  cvgratz  11918  mertenslemub  11920  mertenslemi1  11921  mertenslem2  11922  mertensabs  11923  prodmodclem3  11961  fprodf1o  11974  prodsnf  11978  fprodm1  11984  fprodabs  12002  fprodcnv  12011  efcllemp  12044  efcj  12059  efaddlem  12060  efcan  12062  efsub  12067  efexp  12068  efzval  12069  efgt0  12070  eftlub  12076  efltim  12084  sinval  12088  cosval  12089  tanval3ap  12100  resinval  12101  recosval  12102  resin4p  12104  recos4p  12105  sinneg  12112  cosneg  12113  efmival  12119  efeul  12120  sinadd  12122  cosadd  12123  sinsub  12126  cossub  12127  addsin  12128  subsin  12129  addcos  12132  subcos  12133  sincossq  12134  sin2t  12135  cos2t  12136  sin01bnd  12143  cos01bnd  12144  sin02gt0  12150  cos12dec  12154  absefi  12155  absef  12156  absefib  12157  efieq1re  12158  demoivre  12159  demoivreALT  12160  flodddiv4  12322  bitsval  12329  bits0  12334  bitsp1  12337  bitsp1e  12338  bitsp1o  12339  bitsmod  12342  nninfctlemfo  12436  alginv  12444  algcvg  12445  eucalgval  12451  eucalginv  12453  eucalglt  12454  eucalgcvga  12455  eucalg  12456  lcmgcd  12475  lcm1  12478  sqpweven  12572  2sqpwodd  12573  sqne2sq  12574  qnumval  12582  qdenval  12583  qden1elz  12602  nn0sqrtelqelz  12603  phival  12610  dfphi2  12617  phiprmpw  12619  phiprm  12620  eulerthlemth  12629  hashgcdeq  12637  phisum  12638  pythagtriplem6  12668  pythagtriplem7  12669  pythagtriplem12  12673  pythagtriplem14  12675  fldivp1  12746  4sqlem11  12799  ennnfonelemg  12849  ennnfonelemp1  12852  ennnfonelemkh  12858  ennnfonelemhf1o  12859  ennnfonelemnn0  12868  ctinfomlemom  12873  ctiunctlemu1st  12880  ctiunctlemu2nd  12881  ctiunctlemudc  12883  ctiunctlemfo  12885  isstruct2im  12917  isstruct2r  12918  setsslid  12958  ressbasd  12974  resseqnbasd  12980  ressplusgd  13036  ptex  13171  prdsex  13176  prdsval  13180  prdsbas3  13194  pwsval  13198  pwsbas  13199  pwsplusgval  13202  pwsmulrval  13203  imasex  13212  imasival  13213  f1ocpbl  13218  f1ovscpbl  13219  imasaddvallemg  13222  qusval  13230  fvprif  13250  xpsff1o  13256  igsumvalx  13296  gsumprval  13306  pws0g  13358  imasmnd  13360  ismhm  13368  mhmpropd  13373  mhmlin  13374  mhmf1o  13377  resmhm  13394  mhmco  13397  gsumwmhm  13405  grpinvsub  13489  pwsinvg  13519  imasgrp2  13521  imasgrp  13522  mhmlem  13525  mhmid  13526  mhmmnd  13527  ghmgrp  13529  mulgfvalg  13532  mulgval  13533  mulgnegnn  13543  mulgneg  13551  mulgnegneg  13552  mulgm1  13553  mulginvcom  13558  mulgz  13561  mulgnndir  13562  mulgdir  13565  mulgass  13570  mhmmulg  13574  subgmulg  13599  isnsg  13613  eqgfval  13633  ghmlin  13659  ghmid  13660  ghminv  13661  ghmsub  13662  ghmmulg  13667  resghm  13671  ghmeql  13678  ablsub2inv  13722  ghmcmn  13738  invghm  13740  imasabl  13747  gsumfzreidx  13748  gsumfzmhm  13754  mgpplusgg  13761  mgpbasg  13763  mgpscag  13764  mgptsetg  13765  mgpdsg  13767  rngm2neg  13786  imasrng  13793  isring  13837  ringm2neg  13892  imasring  13901  opprmulfvalg  13907  opprsllem  13911  isunitd  13943  opprunitd  13947  invrfvald  13959  rdivmuldivd  13981  rhmmul  14001  isrhm2d  14002  rhm1  14004  rhmdvdsr  14012  rhmopp  14013  rhmunitinv  14015  islmod  14128  islmodd  14130  scaffvalg  14143  lmodpropd  14186  lsssetm  14193  islssmd  14196  lssats2  14251  lspsnneg  14257  lspsnsub  14258  lspun0  14262  lmodindp1  14265  sralemg  14275  srascag  14279  sravscag  14280  sraipg  14281  rlmscabas  14297  ixpsnbasval  14303  2idlval  14339  2idlvalg  14340  mulgrhm2  14447  zlmlemg  14465  zlmsca  14469  zlmvscag  14470  znval  14473  znle  14474  znbaslemnn  14476  znidomb  14495  psrval  14503  psrbasg  14511  psrplusgg  14515  mplvalcoe  14527  mplsubgfileminv  14537  mpl0fi  14539  mplnegfi  14542  istps  14579  tpspropd  14583  eltpsg  14587  txvalex  14801  txval  14802  txbasval  14814  upxp  14819  uptx  14821  txrest  14823  cnmpt11  14830  cnmpt21  14838  hmeontr  14860  txhmeo  14866  psmetxrge0  14879  xmetunirn  14905  mopnval  14989  mopntopon  14990  isxms  14998  isxms2  14999  isms  15000  msrtri  15023  xmspropd  15024  mspropd  15025  setsmsbasg  15026  setsmsdsg  15027  setsmstsetg  15028  comet  15046  metcnpi  15062  metcnpi2  15063  cnbl0  15081  cnblcld  15082  resubmet  15103  mpomulcn  15113  elcncf  15120  cncfi  15125  rescncf  15128  mulc1cncf  15136  cncfco  15138  cncfmptid  15144  addccncf  15147  cdivcncfap  15151  negcncf  15152  mulcncflem  15154  ivthinclemlopn  15183  ivthinclemuopn  15185  limccl  15206  ellimc3apf  15207  limcimolemlt  15211  cnplimclemle  15215  limccnpcntop  15222  reldvg  15226  dvfvalap  15228  dveflem  15273  dvef  15274  plymullem1  15295  plycjlemc  15307  plycj  15308  plyrecj  15310  plyreres  15311  sin0pilem1  15328  ef2kpi  15353  sinperlem  15355  sin2kpi  15358  cos2kpi  15359  sin2pim  15360  cos2pim  15361  ptolemy  15371  sincosq2sgn  15374  sincosq3sgn  15375  sincosq4sgn  15376  sinq12gt0  15377  tangtx  15385  sincosq1eq  15386  abssinper  15393  sinkpi  15394  coskpi  15395  cosq34lt1  15397  relogeftb  15412  relogoprlem  15415  relogexp  15419  rpcxpef  15441  logcxp  15444  1cxp  15447  ecxp  15448  rpcxpadd  15452  rpmulcxp  15456  cxpmul  15459  abscxp  15462  logsqrt  15470  rpabscxpbnd  15487  rpcxplogb  15511  lgsval  15556  lgsval2lem  15562  lgsval4a  15574  lgsdi  15589  lgseisenlem3  15624  lgseisenlem4  15625  lgsquadlem1  15629  lgsquadlem2  15630  lgsquadlem3  15631  2lgslem1  15643  2lgslem3a  15645  2lgslem3b  15646  2lgslem3c  15647  2lgslem3d  15648  nnsf  16083  peano4nninf  16084  peano3nninf  16085  nninfalllem1  16086  nninfall  16087  nninfsellemdc  16088  nninfsellemeq  16092  nninfsellemqall  16093  nninfsellemeqinf  16094  nninfsel  16095  nnnninfex  16100  exmidsbthr  16103  qdencn  16107  refeq  16108  isomninnlem  16110  apdifflemr  16127  apdiff  16128  ismkvnnlem  16132  nconstwlpolem  16145