Theorem fveq2d 5489

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

Syntax hints:   → wi 4   = wceq 1343  ‘cfv 5187

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-ia1 105  ax-ia2 106  ax-ia3 107  ax-io 699  ax-5 1435  ax-7 1436  ax-gen 1437  ax-ie1 1481  ax-ie2 1482  ax-8 1492  ax-10 1493  ax-11 1494  ax-i12 1495  ax-bndl 1497  ax-4 1498  ax-17 1514  ax-i9 1518  ax-ial 1522  ax-i5r 1523  ax-ext 2147

This theorem depends on definitions:  df-bi 116  df-3an 970  df-tru 1346  df-nf 1449  df-sb 1751  df-clab 2152  df-cleq 2158  df-clel 2161  df-nfc 2296  df-rex 2449  df-v 2727  df-un 3119  df-sn 3581  df-pr 3582  df-op 3584  df-uni 3789  df-br 3982  df-iota 5152  df-fv 5195

This theorem is referenced by:  2fveq3  5490  fveq12d  5492  fveqeq2d  5493  csbfvg  5523  fvmptdf  5572  fvmptt  5576  fcof1  5750  oveq1  5848  oveq2  5849  fvoveq1d  5863  caofinvl  6071  op1stg  6115  op2ndg  6116  ot1stg  6117  ot2ndg  6118  eloprabi  6161  1stconst  6185  algrflemg  6194  tfrlem1  6272  tfrlem3ag  6273  tfrlem3a  6274  tfrlem9  6283  tfr0dm  6286  tfrlemisucaccv  6289  tfrlemiubacc  6294  tfrlemiex  6295  tfrlemi1  6296  tfr1onlem3ag  6301  tfr1onlemsucaccv  6305  tfr1onlemubacc  6310  tfr1onlemex  6311  tfr1onlemaccex  6312  tfrcllemsucaccv  6318  tfrcllembxssdm  6320  tfrcllemubacc  6323  tfrcllemex  6324  tfrcllemaccex  6325  tfrcllemres  6326  tfrcldm  6327  rdgivallem  6345  rdgival  6346  rdgss  6347  rdgisuc1  6348  rdgon  6350  rdg0  6351  frec0g  6361  frecabcl  6363  freccllem  6366  frecfcllem  6368  frecsuclem  6370  frecsuc  6371  frecrdg  6372  oav2  6427  omv2  6429  xpdom2  6793  xpmapenlem  6811  xpmapen  6812  ac6sfi  6860  1stinl  7035  2ndinl  7036  1stinr  7037  2ndinr  7038  updjudhcoinlf  7041  updjudhcoinrg  7042  caseinl  7052  caseinr  7053  omp1eomlem  7055  omp1eom  7056  difinfsn  7061  ctmlemr  7069  ctm  7070  ctssdclemn0  7071  ctssdccl  7072  nnnninfeq  7088  nnnninfeq2  7089  enomnilem  7098  enmkvlem  7121  enwomnilem  7129  exmidfodomrlemeldju  7151  exmidfodomrlemreseldju  7152  exmidfodomrlemr  7154  exmidfodomrlemrALT  7155  exmidaclem  7160  cc2  7204  cc3  7205  ltdfpr  7443  genpelvl  7449  genpelvu  7450  recexpr  7575  cauappcvgprlem1  7596  caucvgprlemnkj  7603  caucvgprlemnbj  7604  caucvgprlemm  7605  caucvgprlemdisj  7611  caucvgprlemloc  7612  caucvgprlemcl  7613  caucvgprlemladdfu  7614  caucvgprlemladdrl  7615  caucvgprlem1  7616  caucvgprlem2  7617  caucvgpr  7619  caucvgprprlemell  7622  caucvgprprlemelu  7623  caucvgprprlemcbv  7624  caucvgprprlemval  7625  caucvgprprlemnkeqj  7627  caucvgprprlemmu  7632  caucvgprprlemopl  7634  caucvgprprlemlol  7635  caucvgprprlemopu  7636  caucvgprprlemloc  7640  caucvgprprlemclphr  7642  caucvgprprlemexbt  7643  caucvgprprlem1  7646  caucvgprprlem2  7647  caucvgsr  7739  axcaucvglemval  7834  axcaucvglemres  7836  fv0p1e1  8968  uzin  9494  cnref1o  9584  fzsuc2  10010  fseq1m1p1  10026  fzoss2  10103  elfzonlteqm1  10141  divfl0  10227  flqzadd  10229  fldiv4p1lem1div2  10236  ceilqval  10237  flqdiv  10252  modqval  10255  modqfrac  10268  modqmulnn  10273  modqid  10280  modqcyc  10290  modqdi  10323  frec2uzuzd  10333  frec2uzrdg  10340  frecuzrdgrcl  10341  frecuzrdgtcl  10343  frecuzrdgsuc  10345  frecuzrdgrclt  10346  frecuzrdgg  10347  frecuzrdgfunlem  10350  frecuzrdgsuctlem  10354  iseqovex  10387  iseqvalcbv  10388  seq3val  10389  seqvalcd  10390  seq3m1  10399  seq3shft2  10404  monoord  10407  monoord2  10408  iseqf1olemqval  10418  iseqf1olemab  10420  iseqf1olemqk  10425  iseqf1olemjpcl  10426  iseqf1olemqpcl  10427  iseqf1olemfvp  10428  seq3f1olemqsumkj  10429  seq3f1olemqsumk  10430  seq3f1olemqsum  10431  seq3f1olemp  10433  seq3f1oleml  10434  seq3homo  10441  exp3val  10453  expnegap0  10459  facnn2  10643  facwordi  10649  faclbnd6  10653  bcval  10658  bccmpl  10663  bcn0  10664  bcm1k  10669  bcp1n  10670  bcn2  10673  hashinfom  10687  hashennn  10689  hashsng  10707  omgadd  10711  hashprg  10717  fihashssdif  10727  hashdifpr  10729  hashfzo  10731  hashfzp1  10733  hashxp  10735  zfz1isolemiso  10748  zfz1iso  10750  shftval2  10764  shftval3  10765  shftval4  10766  shftval5  10767  seq3shft  10776  imval  10788  imre  10789  reim  10790  crim  10796  reim0  10799  mulreap  10802  recj  10805  reneg  10806  readd  10807  resub  10808  remullem  10809  redivap  10812  imcj  10813  imneg  10814  imadd  10815  imsub  10816  imdivap  10819  cjsub  10830  cjexp  10831  cjreim2  10842  cjap  10844  cjdivap  10847  cnrecnv  10848  cvg1nlemcau  10922  cvg1nlemres  10923  absval  10939  rennim  10940  sqrtdiv  10980  sqrtmsq  10983  absneg  10988  abscj  10990  absval2  10995  absreim  11006  absmul  11007  absdivap  11008  absid  11009  absre  11015  absexp  11017  absexpzap  11018  absimle  11022  abssub  11039  abs3dif  11043  abs2dif  11044  abs2dif2  11045  recan  11047  cau3lem  11052  max0addsup  11157  minabs  11173  bdtrilem  11176  clim  11218  clim2  11220  clim0  11222  clim0c  11223  climi0  11226  climconst  11227  climshftlemg  11239  climcn1  11245  climcn2  11246  addcn2  11247  subcn2  11248  mulcn2  11249  reccn2ap  11250  cjcn2  11253  recn2  11254  imcn2  11255  iser3shft  11283  climcau  11284  climcvg1nlem  11286  climcvg1n  11287  serf0  11289  summodclem3  11317  summodclem2a  11318  summodc  11320  fsumf1o  11327  sumsnf  11346  fsumm1  11353  fsumcnv  11374  fsumabs  11402  fsumrelem  11408  iserabs  11412  hash2iun1dif1  11417  isumshft  11427  isumsplit  11428  expcnvap0  11439  expcnv  11441  cvgratnnlemseq  11463  cvgratnnlemrate  11467  cvgratz  11469  mertenslemub  11471  mertenslemi1  11472  mertenslem2  11473  mertensabs  11474  prodmodclem3  11512  fprodf1o  11525  prodsnf  11529  fprodm1  11535  fprodabs  11553  fprodcnv  11562  efcllemp  11595  efcj  11610  efaddlem  11611  efcan  11613  efsub  11618  efexp  11619  efzval  11620  efgt0  11621  eftlub  11627  efltim  11635  sinval  11639  cosval  11640  tanval3ap  11651  resinval  11652  recosval  11653  resin4p  11655  recos4p  11656  sinneg  11663  cosneg  11664  efmival  11670  efeul  11671  sinadd  11673  cosadd  11674  sinsub  11677  cossub  11678  addsin  11679  subsin  11680  addcos  11683  subcos  11684  sincossq  11685  sin2t  11686  cos2t  11687  sin01bnd  11694  cos01bnd  11695  sin02gt0  11700  cos12dec  11704  absefi  11705  absef  11706  absefib  11707  efieq1re  11708  demoivre  11709  demoivreALT  11710  flodddiv4  11867  alginv  11975  algcvg  11976  eucalgval  11982  eucalginv  11984  eucalglt  11985  eucalgcvga  11986  eucalg  11987  lcmgcd  12006  lcm1  12009  sqpweven  12103  2sqpwodd  12104  sqne2sq  12105  qnumval  12113  qdenval  12114  qden1elz  12133  nn0sqrtelqelz  12134  phival  12141  dfphi2  12148  phiprmpw  12150  phiprm  12151  eulerthlemth  12160  hashgcdeq  12167  phisum  12168  pythagtriplem6  12198  pythagtriplem7  12199  pythagtriplem12  12203  pythagtriplem14  12205  fldivp1  12274  ennnfonelemg  12332  ennnfonelemp1  12335  ennnfonelemkh  12341  ennnfonelemhf1o  12342  ennnfonelemnn0  12351  ctinfomlemom  12356  ctiunctlemu1st  12363  ctiunctlemu2nd  12364  ctiunctlemudc  12366  ctiunctlemfo  12368  isstruct2im  12400  isstruct2r  12401  strslfv3  12435  setsslid  12440  ressid2  12449  ressval2  12450  istps  12630  tpspropd  12634  eltpsg  12638  txvalex  12854  txval  12855  txbasval  12867  upxp  12872  uptx  12874  txrest  12876  cnmpt11  12883  cnmpt21  12891  hmeontr  12913  txhmeo  12919  psmetxrge0  12932  xmetunirn  12958  mopnval  13042  mopntopon  13043  isxms  13051  isxms2  13052  isms  13053  msrtri  13076  xmspropd  13077  mspropd  13078  setsmsbasg  13079  setsmsdsg  13080  setsmstsetg  13081  comet  13099  metcnpi  13115  metcnpi2  13116  cnbl0  13134  cnblcld  13135  resubmet  13148  elcncf  13160  cncfi  13165  rescncf  13168  mulc1cncf  13176  cncfco  13178  cncfmptid  13183  addccncf  13186  cdivcncfap  13187  negcncf  13188  mulcncflem  13190  ivthinclemlopn  13214  ivthinclemuopn  13216  limccl  13228  ellimc3apf  13229  limcimolemlt  13233  cnplimclemle  13237  limccnpcntop  13244  reldvg  13248  dvfvalap  13250  dveflem  13287  dvef  13288  sin0pilem1  13302  ef2kpi  13327  sinperlem  13329  sin2kpi  13332  cos2kpi  13333  sin2pim  13334  cos2pim  13335  ptolemy  13345  sincosq2sgn  13348  sincosq3sgn  13349  sincosq4sgn  13350  sinq12gt0  13351  tangtx  13359  sincosq1eq  13360  abssinper  13367  sinkpi  13368  coskpi  13369  cosq34lt1  13371  relogeftb  13386  relogoprlem  13389  relogexp  13393  rpcxpef  13415  logcxp  13418  1cxp  13421  ecxp  13422  rpcxpadd  13426  rpmulcxp  13430  cxpmul  13433  abscxp  13435  logsqrt  13443  rpabscxpbnd  13459  rpcxplogb  13482  lgsval  13505  lgsval2lem  13511  lgsval4a  13523  lgsdi  13538  nnsf  13845  peano4nninf  13846  peano3nninf  13847  nninfalllem1  13848  nninfall  13849  nninfsellemdc  13850  nninfsellemeq  13854  nninfsellemqall  13855  nninfsellemeqinf  13856  nninfsel  13857  exmidsbthr  13862  qdencn  13866  refeq  13867  isomninnlem  13869  apdifflemr  13886  apdiff  13887  ismkvnnlem  13891  nconstwlpolem  13903