Theorem fveq2d 5521

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

Syntax hints:   → wi 4   = wceq 1353  ‘cfv 5218

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 709  ax-5 1447  ax-7 1448  ax-gen 1449  ax-ie1 1493  ax-ie2 1494  ax-8 1504  ax-10 1505  ax-11 1506  ax-i12 1507  ax-bndl 1509  ax-4 1510  ax-17 1526  ax-i9 1530  ax-ial 1534  ax-i5r 1535  ax-ext 2159

This theorem depends on definitions:  df-bi 117  df-3an 980  df-tru 1356  df-nf 1461  df-sb 1763  df-clab 2164  df-cleq 2170  df-clel 2173  df-nfc 2308  df-rex 2461  df-v 2741  df-un 3135  df-sn 3600  df-pr 3601  df-op 3603  df-uni 3812  df-br 4006  df-iota 5180  df-fv 5226

This theorem is referenced by:  2fveq3  5522  fveq12d  5524  fveqeq2d  5525  csbfvg  5556  fvmptdf  5606  fvmptt  5610  fcof1  5787  oveq1  5885  oveq2  5886  fvoveq1d  5900  caofinvl  6108  op1stg  6154  op2ndg  6155  ot1stg  6156  ot2ndg  6157  eloprabi  6200  1stconst  6225  algrflemg  6234  tfrlem1  6312  tfrlem3ag  6313  tfrlem3a  6314  tfrlem9  6323  tfr0dm  6326  tfrlemisucaccv  6329  tfrlemiubacc  6334  tfrlemiex  6335  tfrlemi1  6336  tfr1onlem3ag  6341  tfr1onlemsucaccv  6345  tfr1onlemubacc  6350  tfr1onlemex  6351  tfr1onlemaccex  6352  tfrcllemsucaccv  6358  tfrcllembxssdm  6360  tfrcllemubacc  6363  tfrcllemex  6364  tfrcllemaccex  6365  tfrcllemres  6366  tfrcldm  6367  rdgivallem  6385  rdgival  6386  rdgss  6387  rdgisuc1  6388  rdgon  6390  rdg0  6391  frec0g  6401  frecabcl  6403  freccllem  6406  frecfcllem  6408  frecsuclem  6410  frecsuc  6411  frecrdg  6412  oav2  6467  omv2  6469  xpdom2  6834  xpmapenlem  6852  xpmapen  6853  ac6sfi  6901  1stinl  7076  2ndinl  7077  1stinr  7078  2ndinr  7079  updjudhcoinlf  7082  updjudhcoinrg  7083  caseinl  7093  caseinr  7094  omp1eomlem  7096  omp1eom  7097  difinfsn  7102  ctmlemr  7110  ctm  7111  ctssdclemn0  7112  ctssdccl  7113  nnnninfeq  7129  nnnninfeq2  7130  enomnilem  7139  enmkvlem  7162  enwomnilem  7170  exmidfodomrlemeldju  7201  exmidfodomrlemreseldju  7202  exmidfodomrlemr  7204  exmidfodomrlemrALT  7205  exmidaclem  7210  cc2  7269  cc3  7270  ltdfpr  7508  genpelvl  7514  genpelvu  7515  recexpr  7640  cauappcvgprlem1  7661  caucvgprlemnkj  7668  caucvgprlemnbj  7669  caucvgprlemm  7670  caucvgprlemdisj  7676  caucvgprlemloc  7677  caucvgprlemcl  7678  caucvgprlemladdfu  7679  caucvgprlemladdrl  7680  caucvgprlem1  7681  caucvgprlem2  7682  caucvgpr  7684  caucvgprprlemell  7687  caucvgprprlemelu  7688  caucvgprprlemcbv  7689  caucvgprprlemval  7690  caucvgprprlemnkeqj  7692  caucvgprprlemmu  7697  caucvgprprlemopl  7699  caucvgprprlemlol  7700  caucvgprprlemopu  7701  caucvgprprlemloc  7705  caucvgprprlemclphr  7707  caucvgprprlemexbt  7708  caucvgprprlem1  7711  caucvgprprlem2  7712  caucvgsr  7804  axcaucvglemval  7899  axcaucvglemres  7901  fv0p1e1  9037  uzin  9563  cnref1o  9653  fzsuc2  10082  fseq1m1p1  10098  fzoss2  10175  elfzonlteqm1  10213  divfl0  10299  flqzadd  10301  fldiv4p1lem1div2  10308  ceilqval  10309  flqdiv  10324  modqval  10327  modqfrac  10340  modqmulnn  10345  modqid  10352  modqcyc  10362  modqdi  10395  frec2uzuzd  10405  frec2uzrdg  10412  frecuzrdgrcl  10413  frecuzrdgtcl  10415  frecuzrdgsuc  10417  frecuzrdgrclt  10418  frecuzrdgg  10419  frecuzrdgfunlem  10422  frecuzrdgsuctlem  10426  iseqovex  10459  iseqvalcbv  10460  seq3val  10461  seqvalcd  10462  seq3m1  10471  seq3shft2  10476  monoord  10479  monoord2  10480  iseqf1olemqval  10490  iseqf1olemab  10492  iseqf1olemqk  10497  iseqf1olemjpcl  10498  iseqf1olemqpcl  10499  iseqf1olemfvp  10500  seq3f1olemqsumkj  10501  seq3f1olemqsumk  10502  seq3f1olemqsum  10503  seq3f1olemp  10505  seq3f1oleml  10506  seq3homo  10513  exp3val  10525  expnegap0  10531  facnn2  10717  facwordi  10723  faclbnd6  10727  bcval  10732  bccmpl  10737  bcn0  10738  bcm1k  10743  bcp1n  10744  bcn2  10747  hashinfom  10761  hashennn  10763  hashsng  10781  omgadd  10785  hashprg  10791  fihashssdif  10801  hashdifpr  10803  hashfzo  10805  hashfzp1  10807  hashxp  10809  zfz1isolemiso  10822  zfz1iso  10824  shftval2  10838  shftval3  10839  shftval4  10840  shftval5  10841  seq3shft  10850  imval  10862  imre  10863  reim  10864  crim  10870  reim0  10873  mulreap  10876  recj  10879  reneg  10880  readd  10881  resub  10882  remullem  10883  redivap  10886  imcj  10887  imneg  10888  imadd  10889  imsub  10890  imdivap  10893  cjsub  10904  cjexp  10905  cjreim2  10916  cjap  10918  cjdivap  10921  cnrecnv  10922  cvg1nlemcau  10996  cvg1nlemres  10997  absval  11013  rennim  11014  sqrtdiv  11054  sqrtmsq  11057  absneg  11062  abscj  11064  absval2  11069  absreim  11080  absmul  11081  absdivap  11082  absid  11083  absre  11089  absexp  11091  absexpzap  11092  absimle  11096  abssub  11113  abs3dif  11117  abs2dif  11118  abs2dif2  11119  recan  11121  cau3lem  11126  max0addsup  11231  minabs  11247  bdtrilem  11250  clim  11292  clim2  11294  clim0  11296  clim0c  11297  climi0  11300  climconst  11301  climshftlemg  11313  climcn1  11319  climcn2  11320  addcn2  11321  subcn2  11322  mulcn2  11323  reccn2ap  11324  cjcn2  11327  recn2  11328  imcn2  11329  iser3shft  11357  climcau  11358  climcvg1nlem  11360  climcvg1n  11361  serf0  11363  summodclem3  11391  summodclem2a  11392  summodc  11394  fsumf1o  11401  sumsnf  11420  fsumm1  11427  fsumcnv  11448  fsumabs  11476  fsumrelem  11482  iserabs  11486  hash2iun1dif1  11491  isumshft  11501  isumsplit  11502  expcnvap0  11513  expcnv  11515  cvgratnnlemseq  11537  cvgratnnlemrate  11541  cvgratz  11543  mertenslemub  11545  mertenslemi1  11546  mertenslem2  11547  mertensabs  11548  prodmodclem3  11586  fprodf1o  11599  prodsnf  11603  fprodm1  11609  fprodabs  11627  fprodcnv  11636  efcllemp  11669  efcj  11684  efaddlem  11685  efcan  11687  efsub  11692  efexp  11693  efzval  11694  efgt0  11695  eftlub  11701  efltim  11709  sinval  11713  cosval  11714  tanval3ap  11725  resinval  11726  recosval  11727  resin4p  11729  recos4p  11730  sinneg  11737  cosneg  11738  efmival  11744  efeul  11745  sinadd  11747  cosadd  11748  sinsub  11751  cossub  11752  addsin  11753  subsin  11754  addcos  11757  subcos  11758  sincossq  11759  sin2t  11760  cos2t  11761  sin01bnd  11768  cos01bnd  11769  sin02gt0  11774  cos12dec  11778  absefi  11779  absef  11780  absefib  11781  efieq1re  11782  demoivre  11783  demoivreALT  11784  flodddiv4  11942  alginv  12050  algcvg  12051  eucalgval  12057  eucalginv  12059  eucalglt  12060  eucalgcvga  12061  eucalg  12062  lcmgcd  12081  lcm1  12084  sqpweven  12178  2sqpwodd  12179  sqne2sq  12180  qnumval  12188  qdenval  12189  qden1elz  12208  nn0sqrtelqelz  12209  phival  12216  dfphi2  12223  phiprmpw  12225  phiprm  12226  eulerthlemth  12235  hashgcdeq  12242  phisum  12243  pythagtriplem6  12273  pythagtriplem7  12274  pythagtriplem12  12278  pythagtriplem14  12280  fldivp1  12349  ennnfonelemg  12407  ennnfonelemp1  12410  ennnfonelemkh  12416  ennnfonelemhf1o  12417  ennnfonelemnn0  12426  ctinfomlemom  12431  ctiunctlemu1st  12438  ctiunctlemu2nd  12439  ctiunctlemudc  12441  ctiunctlemfo  12443  isstruct2im  12475  isstruct2r  12476  strslfv3  12511  setsslid  12516  ressbasd  12530  resseqnbasd  12535  ressplusgd  12590  ptex  12719  prdsex  12724  imasex  12732  imasival  12733  f1ocpbl  12738  f1ovscpbl  12739  imasaddvallemg  12742  qusval  12750  fvprif  12769  xpsff1o  12775  ismhm  12860  mhmpropd  12864  mhmlin  12865  mhmf1o  12868  mhmco  12881  grpinvsub  12959  imasgrp2  12985  mhmlem  12987  mhmid  12988  mhmmnd  12989  ghmgrp  12991  mulgfvalg  12994  mulgval  12995  mulgnegnn  13003  mulgneg  13011  mulgnegneg  13012  mulgm1  13013  mulginvcom  13018  mulgz  13021  mulgnndir  13022  mulgdir  13025  mulgass  13030  mhmmulg  13034  subgmulg  13058  isnsg  13072  eqgfval  13092  ablsub2inv  13125  mgpplusgg  13145  mgpbasg  13147  mgpscag  13148  mgptsetg  13149  mgpdsg  13151  isring  13194  ringm2neg  13243  opprmulfvalg  13253  opprsllem  13257  isunitd  13286  opprunitd  13290  invrfvald  13302  rdivmuldivd  13324  islmod  13392  islmodd  13394  scaffvalg  13407  lmodpropd  13450  lsssetm  13455  islssmd  13457  lssats2  13512  lspsnneg  13518  lspsnsub  13519  lspun0  13523  lmodindp1  13526  sralemg  13536  srascag  13540  sravscag  13541  sraipg  13542  ixpsnbasval  13563  zlmlemg  13651  zlmsca  13655  zlmvscag  13656  istps  13693  tpspropd  13697  eltpsg  13701  txvalex  13915  txval  13916  txbasval  13928  upxp  13933  uptx  13935  txrest  13937  cnmpt11  13944  cnmpt21  13952  hmeontr  13974  txhmeo  13980  psmetxrge0  13993  xmetunirn  14019  mopnval  14103  mopntopon  14104  isxms  14112  isxms2  14113  isms  14114  msrtri  14137  xmspropd  14138  mspropd  14139  setsmsbasg  14140  setsmsdsg  14141  setsmstsetg  14142  comet  14160  metcnpi  14176  metcnpi2  14177  cnbl0  14195  cnblcld  14196  resubmet  14209  elcncf  14221  cncfi  14226  rescncf  14229  mulc1cncf  14237  cncfco  14239  cncfmptid  14244  addccncf  14247  cdivcncfap  14248  negcncf  14249  mulcncflem  14251  ivthinclemlopn  14275  ivthinclemuopn  14277  limccl  14289  ellimc3apf  14290  limcimolemlt  14294  cnplimclemle  14298  limccnpcntop  14305  reldvg  14309  dvfvalap  14311  dveflem  14348  dvef  14349  sin0pilem1  14363  ef2kpi  14388  sinperlem  14390  sin2kpi  14393  cos2kpi  14394  sin2pim  14395  cos2pim  14396  ptolemy  14406  sincosq2sgn  14409  sincosq3sgn  14410  sincosq4sgn  14411  sinq12gt0  14412  tangtx  14420  sincosq1eq  14421  abssinper  14428  sinkpi  14429  coskpi  14430  cosq34lt1  14432  relogeftb  14447  relogoprlem  14450  relogexp  14454  rpcxpef  14476  logcxp  14479  1cxp  14482  ecxp  14483  rpcxpadd  14487  rpmulcxp  14491  cxpmul  14494  abscxp  14496  logsqrt  14504  rpabscxpbnd  14520  rpcxplogb  14543  lgsval  14566  lgsval2lem  14572  lgsval4a  14584  lgsdi  14599  nnsf  14916  peano4nninf  14917  peano3nninf  14918  nninfalllem1  14919  nninfall  14920  nninfsellemdc  14921  nninfsellemeq  14925  nninfsellemqall  14926  nninfsellemeqinf  14927  nninfsel  14928  exmidsbthr  14933  qdencn  14937  refeq  14938  isomninnlem  14940  apdifflemr  14957  apdiff  14958  ismkvnnlem  14962  nconstwlpolem  14975