Theorem fveq2d 5490

Description: Equality deduction for function value. (Contributed by NM, 29-May-1999.)

Hypothesis

Ref	Expression
fveq2d.1	|- ( ph -> A = B )

Assertion

Ref	Expression
fveq2d	|- ( ph -> ( F ` A ) = ( F ` B ) )

Proof of Theorem fveq2d

Step	Hyp	Ref	Expression
1		fveq2d.1	. 2 |- ( ph -> A = B )
2		fveq2 5486	. 2 |- ( A = B -> ( F ` A ) = ( F ` B ) )
3	1, 2	syl 14	1 |- ( ph -> ( F ` A ) = ( F ` B ) )

Syntax hints:   -> wi 4   = wceq 1343   ` cfv 5188

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 2297  df-rex 2450  df-v 2728  df-un 3120  df-sn 3582  df-pr 3583  df-op 3585  df-uni 3790  df-br 3983  df-iota 5153  df-fv 5196

This theorem is referenced by:  2fveq3  5491  fveq12d  5493  fveqeq2d  5494  csbfvg  5524  fvmptdf  5573  fvmptt  5577  fcof1  5751  oveq1  5849  oveq2  5850  fvoveq1d  5864  caofinvl  6072  op1stg  6118  op2ndg  6119  ot1stg  6120  ot2ndg  6121  eloprabi  6164  1stconst  6189  algrflemg  6198  tfrlem1  6276  tfrlem3ag  6277  tfrlem3a  6278  tfrlem9  6287  tfr0dm  6290  tfrlemisucaccv  6293  tfrlemiubacc  6298  tfrlemiex  6299  tfrlemi1  6300  tfr1onlem3ag  6305  tfr1onlemsucaccv  6309  tfr1onlemubacc  6314  tfr1onlemex  6315  tfr1onlemaccex  6316  tfrcllemsucaccv  6322  tfrcllembxssdm  6324  tfrcllemubacc  6327  tfrcllemex  6328  tfrcllemaccex  6329  tfrcllemres  6330  tfrcldm  6331  rdgivallem  6349  rdgival  6350  rdgss  6351  rdgisuc1  6352  rdgon  6354  rdg0  6355  frec0g  6365  frecabcl  6367  freccllem  6370  frecfcllem  6372  frecsuclem  6374  frecsuc  6375  frecrdg  6376  oav2  6431  omv2  6433  xpdom2  6797  xpmapenlem  6815  xpmapen  6816  ac6sfi  6864  1stinl  7039  2ndinl  7040  1stinr  7041  2ndinr  7042  updjudhcoinlf  7045  updjudhcoinrg  7046  caseinl  7056  caseinr  7057  omp1eomlem  7059  omp1eom  7060  difinfsn  7065  ctmlemr  7073  ctm  7074  ctssdclemn0  7075  ctssdccl  7076  nnnninfeq  7092  nnnninfeq2  7093  enomnilem  7102  enmkvlem  7125  enwomnilem  7133  exmidfodomrlemeldju  7155  exmidfodomrlemreseldju  7156  exmidfodomrlemr  7158  exmidfodomrlemrALT  7159  exmidaclem  7164  cc2  7208  cc3  7209  ltdfpr  7447  genpelvl  7453  genpelvu  7454  recexpr  7579  cauappcvgprlem1  7600  caucvgprlemnkj  7607  caucvgprlemnbj  7608  caucvgprlemm  7609  caucvgprlemdisj  7615  caucvgprlemloc  7616  caucvgprlemcl  7617  caucvgprlemladdfu  7618  caucvgprlemladdrl  7619  caucvgprlem1  7620  caucvgprlem2  7621  caucvgpr  7623  caucvgprprlemell  7626  caucvgprprlemelu  7627  caucvgprprlemcbv  7628  caucvgprprlemval  7629  caucvgprprlemnkeqj  7631  caucvgprprlemmu  7636  caucvgprprlemopl  7638  caucvgprprlemlol  7639  caucvgprprlemopu  7640  caucvgprprlemloc  7644  caucvgprprlemclphr  7646  caucvgprprlemexbt  7647  caucvgprprlem1  7650  caucvgprprlem2  7651  caucvgsr  7743  axcaucvglemval  7838  axcaucvglemres  7840  fv0p1e1  8972  uzin  9498  cnref1o  9588  fzsuc2  10014  fseq1m1p1  10030  fzoss2  10107  elfzonlteqm1  10145  divfl0  10231  flqzadd  10233  fldiv4p1lem1div2  10240  ceilqval  10241  flqdiv  10256  modqval  10259  modqfrac  10272  modqmulnn  10277  modqid  10284  modqcyc  10294  modqdi  10327  frec2uzuzd  10337  frec2uzrdg  10344  frecuzrdgrcl  10345  frecuzrdgtcl  10347  frecuzrdgsuc  10349  frecuzrdgrclt  10350  frecuzrdgg  10351  frecuzrdgfunlem  10354  frecuzrdgsuctlem  10358  iseqovex  10391  iseqvalcbv  10392  seq3val  10393  seqvalcd  10394  seq3m1  10403  seq3shft2  10408  monoord  10411  monoord2  10412  iseqf1olemqval  10422  iseqf1olemab  10424  iseqf1olemqk  10429  iseqf1olemjpcl  10430  iseqf1olemqpcl  10431  iseqf1olemfvp  10432  seq3f1olemqsumkj  10433  seq3f1olemqsumk  10434  seq3f1olemqsum  10435  seq3f1olemp  10437  seq3f1oleml  10438  seq3homo  10445  exp3val  10457  expnegap0  10463  facnn2  10647  facwordi  10653  faclbnd6  10657  bcval  10662  bccmpl  10667  bcn0  10668  bcm1k  10673  bcp1n  10674  bcn2  10677  hashinfom  10691  hashennn  10693  hashsng  10711  omgadd  10715  hashprg  10721  fihashssdif  10731  hashdifpr  10733  hashfzo  10735  hashfzp1  10737  hashxp  10739  zfz1isolemiso  10752  zfz1iso  10754  shftval2  10768  shftval3  10769  shftval4  10770  shftval5  10771  seq3shft  10780  imval  10792  imre  10793  reim  10794  crim  10800  reim0  10803  mulreap  10806  recj  10809  reneg  10810  readd  10811  resub  10812  remullem  10813  redivap  10816  imcj  10817  imneg  10818  imadd  10819  imsub  10820  imdivap  10823  cjsub  10834  cjexp  10835  cjreim2  10846  cjap  10848  cjdivap  10851  cnrecnv  10852  cvg1nlemcau  10926  cvg1nlemres  10927  absval  10943  rennim  10944  sqrtdiv  10984  sqrtmsq  10987  absneg  10992  abscj  10994  absval2  10999  absreim  11010  absmul  11011  absdivap  11012  absid  11013  absre  11019  absexp  11021  absexpzap  11022  absimle  11026  abssub  11043  abs3dif  11047  abs2dif  11048  abs2dif2  11049  recan  11051  cau3lem  11056  max0addsup  11161  minabs  11177  bdtrilem  11180  clim  11222  clim2  11224  clim0  11226  clim0c  11227  climi0  11230  climconst  11231  climshftlemg  11243  climcn1  11249  climcn2  11250  addcn2  11251  subcn2  11252  mulcn2  11253  reccn2ap  11254  cjcn2  11257  recn2  11258  imcn2  11259  iser3shft  11287  climcau  11288  climcvg1nlem  11290  climcvg1n  11291  serf0  11293  summodclem3  11321  summodclem2a  11322  summodc  11324  fsumf1o  11331  sumsnf  11350  fsumm1  11357  fsumcnv  11378  fsumabs  11406  fsumrelem  11412  iserabs  11416  hash2iun1dif1  11421  isumshft  11431  isumsplit  11432  expcnvap0  11443  expcnv  11445  cvgratnnlemseq  11467  cvgratnnlemrate  11471  cvgratz  11473  mertenslemub  11475  mertenslemi1  11476  mertenslem2  11477  mertensabs  11478  prodmodclem3  11516  fprodf1o  11529  prodsnf  11533  fprodm1  11539  fprodabs  11557  fprodcnv  11566  efcllemp  11599  efcj  11614  efaddlem  11615  efcan  11617  efsub  11622  efexp  11623  efzval  11624  efgt0  11625  eftlub  11631  efltim  11639  sinval  11643  cosval  11644  tanval3ap  11655  resinval  11656  recosval  11657  resin4p  11659  recos4p  11660  sinneg  11667  cosneg  11668  efmival  11674  efeul  11675  sinadd  11677  cosadd  11678  sinsub  11681  cossub  11682  addsin  11683  subsin  11684  addcos  11687  subcos  11688  sincossq  11689  sin2t  11690  cos2t  11691  sin01bnd  11698  cos01bnd  11699  sin02gt0  11704  cos12dec  11708  absefi  11709  absef  11710  absefib  11711  efieq1re  11712  demoivre  11713  demoivreALT  11714  flodddiv4  11871  alginv  11979  algcvg  11980  eucalgval  11986  eucalginv  11988  eucalglt  11989  eucalgcvga  11990  eucalg  11991  lcmgcd  12010  lcm1  12013  sqpweven  12107  2sqpwodd  12108  sqne2sq  12109  qnumval  12117  qdenval  12118  qden1elz  12137  nn0sqrtelqelz  12138  phival  12145  dfphi2  12152  phiprmpw  12154  phiprm  12155  eulerthlemth  12164  hashgcdeq  12171  phisum  12172  pythagtriplem6  12202  pythagtriplem7  12203  pythagtriplem12  12207  pythagtriplem14  12209  fldivp1  12278  ennnfonelemg  12336  ennnfonelemp1  12339  ennnfonelemkh  12345  ennnfonelemhf1o  12346  ennnfonelemnn0  12355  ctinfomlemom  12360  ctiunctlemu1st  12367  ctiunctlemu2nd  12368  ctiunctlemudc  12370  ctiunctlemfo  12372  isstruct2im  12404  isstruct2r  12405  strslfv3  12439  setsslid  12444  ressid2  12454  ressval2  12455  istps  12680  tpspropd  12684  eltpsg  12688  txvalex  12904  txval  12905  txbasval  12917  upxp  12922  uptx  12924  txrest  12926  cnmpt11  12933  cnmpt21  12941  hmeontr  12963  txhmeo  12969  psmetxrge0  12982  xmetunirn  13008  mopnval  13092  mopntopon  13093  isxms  13101  isxms2  13102  isms  13103  msrtri  13126  xmspropd  13127  mspropd  13128  setsmsbasg  13129  setsmsdsg  13130  setsmstsetg  13131  comet  13149  metcnpi  13165  metcnpi2  13166  cnbl0  13184  cnblcld  13185  resubmet  13198  elcncf  13210  cncfi  13215  rescncf  13218  mulc1cncf  13226  cncfco  13228  cncfmptid  13233  addccncf  13236  cdivcncfap  13237  negcncf  13238  mulcncflem  13240  ivthinclemlopn  13264  ivthinclemuopn  13266  limccl  13278  ellimc3apf  13279  limcimolemlt  13283  cnplimclemle  13287  limccnpcntop  13294  reldvg  13298  dvfvalap  13300  dveflem  13337  dvef  13338  sin0pilem1  13352  ef2kpi  13377  sinperlem  13379  sin2kpi  13382  cos2kpi  13383  sin2pim  13384  cos2pim  13385  ptolemy  13395  sincosq2sgn  13398  sincosq3sgn  13399  sincosq4sgn  13400  sinq12gt0  13401  tangtx  13409  sincosq1eq  13410  abssinper  13417  sinkpi  13418  coskpi  13419  cosq34lt1  13421  relogeftb  13436  relogoprlem  13439  relogexp  13443  rpcxpef  13465  logcxp  13468  1cxp  13471  ecxp  13472  rpcxpadd  13476  rpmulcxp  13480  cxpmul  13483  abscxp  13485  logsqrt  13493  rpabscxpbnd  13509  rpcxplogb  13532  lgsval  13555  lgsval2lem  13561  lgsval4a  13573  lgsdi  13588  nnsf  13895  peano4nninf  13896  peano3nninf  13897  nninfalllem1  13898  nninfall  13899  nninfsellemdc  13900  nninfsellemeq  13904  nninfsellemqall  13905  nninfsellemeqinf  13906  nninfsel  13907  exmidsbthr  13912  qdencn  13916  refeq  13917  isomninnlem  13919  apdifflemr  13936  apdiff  13937  ismkvnnlem  13941  nconstwlpolem  13953