Theorem fveq2d 5603

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 5599	. 2 |- ( A = B -> ( F ` A ) = ( F ` B ) )
3	1, 2	syl 14	1 |- ( ph -> ( F ` A ) = ( F ` B ) )

Syntax hints:   -> wi 4   = wceq 1373   ` cfv 5290

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 2189

This theorem depends on definitions:  df-bi 117  df-3an 983  df-tru 1376  df-nf 1485  df-sb 1787  df-clab 2194  df-cleq 2200  df-clel 2203  df-nfc 2339  df-rex 2492  df-v 2778  df-un 3178  df-sn 3649  df-pr 3650  df-op 3652  df-uni 3865  df-br 4060  df-iota 5251  df-fv 5298

This theorem is referenced by:  2fveq3  5604  fveq12d  5606  fveqeq2d  5607  csbfvg  5639  fvmptdf  5690  fvmptt  5694  fcof1  5875  oveq1  5974  oveq2  5975  fvoveq1d  5989  caofinvl  6207  op1stg  6259  op2ndg  6260  ot1stg  6261  ot2ndg  6262  eloprabi  6305  1stconst  6330  algrflemg  6339  tfrlem1  6417  tfrlem3ag  6418  tfrlem3a  6419  tfrlem9  6428  tfr0dm  6431  tfrlemisucaccv  6434  tfrlemiubacc  6439  tfrlemiex  6440  tfrlemi1  6441  tfr1onlem3ag  6446  tfr1onlemsucaccv  6450  tfr1onlemubacc  6455  tfr1onlemex  6456  tfr1onlemaccex  6457  tfrcllemsucaccv  6463  tfrcllembxssdm  6465  tfrcllemubacc  6468  tfrcllemex  6469  tfrcllemaccex  6470  tfrcllemres  6471  tfrcldm  6472  rdgivallem  6490  rdgival  6491  rdgss  6492  rdgisuc1  6493  rdgon  6495  rdg0  6496  frec0g  6506  frecabcl  6508  freccllem  6511  frecfcllem  6513  frecsuclem  6515  frecsuc  6516  frecrdg  6517  oav2  6572  omv2  6574  xpdom2  6951  xpmapenlem  6971  xpmapen  6972  ac6sfi  7021  1stinl  7202  2ndinl  7203  1stinr  7204  2ndinr  7205  updjudhcoinlf  7208  updjudhcoinrg  7209  caseinl  7219  caseinr  7220  omp1eomlem  7222  omp1eom  7223  difinfsn  7228  ctmlemr  7236  ctm  7237  ctssdclemn0  7238  ctssdccl  7239  nninfninc  7251  nnnninfeq  7256  nnnninfeq2  7257  enomnilem  7266  enmkvlem  7289  enwomnilem  7297  exmidfodomrlemeldju  7338  exmidfodomrlemreseldju  7339  exmidfodomrlemr  7341  exmidfodomrlemrALT  7342  exmidaclem  7351  cc2  7414  cc3  7415  ltdfpr  7654  genpelvl  7660  genpelvu  7661  recexpr  7786  cauappcvgprlem1  7807  caucvgprlemnkj  7814  caucvgprlemnbj  7815  caucvgprlemm  7816  caucvgprlemdisj  7822  caucvgprlemloc  7823  caucvgprlemcl  7824  caucvgprlemladdfu  7825  caucvgprlemladdrl  7826  caucvgprlem1  7827  caucvgprlem2  7828  caucvgpr  7830  caucvgprprlemell  7833  caucvgprprlemelu  7834  caucvgprprlemcbv  7835  caucvgprprlemval  7836  caucvgprprlemnkeqj  7838  caucvgprprlemmu  7843  caucvgprprlemopl  7845  caucvgprprlemlol  7846  caucvgprprlemopu  7847  caucvgprprlemloc  7851  caucvgprprlemclphr  7853  caucvgprprlemexbt  7854  caucvgprprlem1  7857  caucvgprprlem2  7858  caucvgsr  7950  axcaucvglemval  8045  axcaucvglemres  8047  fv0p1e1  9186  uzin  9716  cnref1o  9807  fzsuc2  10236  fseq1m1p1  10252  fzoss2  10331  elfzonlteqm1  10376  divfl0  10476  flqzadd  10478  fldiv4p1lem1div2  10485  ceilqval  10488  flqdiv  10503  modqval  10506  modqfrac  10519  modqmulnn  10524  modqid  10531  modqcyc  10541  modqdi  10574  frec2uzuzd  10584  frec2uzrdg  10591  frecuzrdgrcl  10592  frecuzrdgtcl  10594  frecuzrdgsuc  10596  frecuzrdgrclt  10597  frecuzrdgg  10598  frecuzrdgfunlem  10601  frecuzrdgsuctlem  10605  iseqovex  10640  iseqvalcbv  10641  seq3val  10642  seqvalcd  10643  seq3m1  10655  seq3shft2  10663  seqshft2g  10664  monoord  10667  monoord2  10668  iseqf1olemqval  10682  iseqf1olemab  10684  iseqf1olemqk  10689  iseqf1olemjpcl  10690  iseqf1olemqpcl  10691  iseqf1olemfvp  10692  seq3f1olemqsumkj  10693  seq3f1olemqsumk  10694  seq3f1olemqsum  10695  seq3f1olemp  10697  seq3f1oleml  10698  seqf1oglem1  10701  seqf1oglem2  10702  seqf1og  10703  seq3homo  10709  seqhomog  10712  exp3val  10723  expnegap0  10729  facnn2  10916  facwordi  10922  faclbnd6  10926  bcval  10931  bccmpl  10936  bcn0  10937  bcm1k  10942  bcp1n  10943  bcn2  10946  hashinfom  10960  hashennn  10962  hashsng  10980  omgadd  10984  hashprg  10990  fihashssdif  11000  hashdifpr  11002  hashfzo  11004  hashfzp1  11006  hashxp  11008  zfz1isolemiso  11021  zfz1iso  11023  lsw1  11080  ccatfvalfi  11086  ccatlen  11089  ccatval3  11093  ccatval21sw  11099  ccatlid  11100  ccatass  11102  lswccatn0lsw  11105  lswccat0lsw  11106  s1leng  11116  ccats1val2  11130  lswccats1  11133  swrdfv0  11145  swrdfv2  11154  swrdsbslen  11157  swrds1  11159  ccatswrd  11161  pfxmpt  11171  pfxfv  11175  pfxtrcfvl  11188  ccatpfx  11192  swrdswrd  11196  lenpfxcctswrd  11202  ccatopth  11207  cats1un  11212  swrdccatin2  11220  pfxccatin12lem2  11222  shftval2  11252  shftval3  11253  shftval4  11254  shftval5  11255  seq3shft  11264  imval  11276  imre  11277  reim  11278  crim  11284  reim0  11287  mulreap  11290  recj  11293  reneg  11294  readd  11295  resub  11296  remullem  11297  redivap  11300  imcj  11301  imneg  11302  imadd  11303  imsub  11304  imdivap  11307  cjsub  11318  cjexp  11319  cjreim2  11330  cjap  11332  cjdivap  11335  cnrecnv  11336  cvg1nlemcau  11410  cvg1nlemres  11411  absval  11427  rennim  11428  sqrtdiv  11468  sqrtmsq  11471  absneg  11476  abscj  11478  absval2  11483  absreim  11494  absmul  11495  absdivap  11496  absid  11497  absre  11503  absexp  11505  absexpzap  11506  absimle  11510  abssub  11527  abs3dif  11531  abs2dif  11532  abs2dif2  11533  recan  11535  cau3lem  11540  max0addsup  11645  minabs  11662  bdtrilem  11665  clim  11707  clim2  11709  clim0  11711  clim0c  11712  climi0  11715  climconst  11716  climshftlemg  11728  climcn1  11734  climcn2  11735  addcn2  11736  subcn2  11737  mulcn2  11738  reccn2ap  11739  cjcn2  11742  recn2  11743  imcn2  11744  iser3shft  11772  climcau  11773  climcvg1nlem  11775  climcvg1n  11776  serf0  11778  summodclem3  11806  summodclem2a  11807  summodc  11809  fsumf1o  11816  sumsnf  11835  fsumm1  11842  fsumcnv  11863  fsumabs  11891  fsumrelem  11897  iserabs  11901  hash2iun1dif1  11906  isumshft  11916  isumsplit  11917  expcnvap0  11928  expcnv  11930  cvgratnnlemseq  11952  cvgratnnlemrate  11956  cvgratz  11958  mertenslemub  11960  mertenslemi1  11961  mertenslem2  11962  mertensabs  11963  prodmodclem3  12001  fprodf1o  12014  prodsnf  12018  fprodm1  12024  fprodabs  12042  fprodcnv  12051  efcllemp  12084  efcj  12099  efaddlem  12100  efcan  12102  efsub  12107  efexp  12108  efzval  12109  efgt0  12110  eftlub  12116  efltim  12124  sinval  12128  cosval  12129  tanval3ap  12140  resinval  12141  recosval  12142  resin4p  12144  recos4p  12145  sinneg  12152  cosneg  12153  efmival  12159  efeul  12160  sinadd  12162  cosadd  12163  sinsub  12166  cossub  12167  addsin  12168  subsin  12169  addcos  12172  subcos  12173  sincossq  12174  sin2t  12175  cos2t  12176  sin01bnd  12183  cos01bnd  12184  sin02gt0  12190  cos12dec  12194  absefi  12195  absef  12196  absefib  12197  efieq1re  12198  demoivre  12199  demoivreALT  12200  flodddiv4  12362  bitsval  12369  bits0  12374  bitsp1  12377  bitsp1e  12378  bitsp1o  12379  bitsmod  12382  nninfctlemfo  12476  alginv  12484  algcvg  12485  eucalgval  12491  eucalginv  12493  eucalglt  12494  eucalgcvga  12495  eucalg  12496  lcmgcd  12515  lcm1  12518  sqpweven  12612  2sqpwodd  12613  sqne2sq  12614  qnumval  12622  qdenval  12623  qden1elz  12642  nn0sqrtelqelz  12643  phival  12650  dfphi2  12657  phiprmpw  12659  phiprm  12660  eulerthlemth  12669  hashgcdeq  12677  phisum  12678  pythagtriplem6  12708  pythagtriplem7  12709  pythagtriplem12  12713  pythagtriplem14  12715  fldivp1  12786  4sqlem11  12839  ennnfonelemg  12889  ennnfonelemp1  12892  ennnfonelemkh  12898  ennnfonelemhf1o  12899  ennnfonelemnn0  12908  ctinfomlemom  12913  ctiunctlemu1st  12920  ctiunctlemu2nd  12921  ctiunctlemudc  12923  ctiunctlemfo  12925  isstruct2im  12957  isstruct2r  12958  setsslid  12998  ressbasd  13014  resseqnbasd  13020  ressplusgd  13076  ptex  13211  prdsex  13216  prdsval  13220  prdsbas3  13234  pwsval  13238  pwsbas  13239  pwsplusgval  13242  pwsmulrval  13243  imasex  13252  imasival  13253  f1ocpbl  13258  f1ovscpbl  13259  imasaddvallemg  13262  qusval  13270  fvprif  13290  xpsff1o  13296  igsumvalx  13336  gsumprval  13346  pws0g  13398  imasmnd  13400  ismhm  13408  mhmpropd  13413  mhmlin  13414  mhmf1o  13417  resmhm  13434  mhmco  13437  gsumwmhm  13445  grpinvsub  13529  pwsinvg  13559  imasgrp2  13561  imasgrp  13562  mhmlem  13565  mhmid  13566  mhmmnd  13567  ghmgrp  13569  mulgfvalg  13572  mulgval  13573  mulgnegnn  13583  mulgneg  13591  mulgnegneg  13592  mulgm1  13593  mulginvcom  13598  mulgz  13601  mulgnndir  13602  mulgdir  13605  mulgass  13610  mhmmulg  13614  subgmulg  13639  isnsg  13653  eqgfval  13673  ghmlin  13699  ghmid  13700  ghminv  13701  ghmsub  13702  ghmmulg  13707  resghm  13711  ghmeql  13718  ablsub2inv  13762  ghmcmn  13778  invghm  13780  imasabl  13787  gsumfzreidx  13788  gsumfzmhm  13794  mgpplusgg  13801  mgpbasg  13803  mgpscag  13804  mgptsetg  13805  mgpdsg  13807  rngm2neg  13826  imasrng  13833  isring  13877  ringm2neg  13932  imasring  13941  opprmulfvalg  13947  opprsllem  13951  isunitd  13983  opprunitd  13987  invrfvald  13999  rdivmuldivd  14021  rhmmul  14041  isrhm2d  14042  rhm1  14044  rhmdvdsr  14052  rhmopp  14053  rhmunitinv  14055  islmod  14168  islmodd  14170  scaffvalg  14183  lmodpropd  14226  lsssetm  14233  islssmd  14236  lssats2  14291  lspsnneg  14297  lspsnsub  14298  lspun0  14302  lmodindp1  14305  sralemg  14315  srascag  14319  sravscag  14320  sraipg  14321  rlmscabas  14337  ixpsnbasval  14343  2idlval  14379  2idlvalg  14380  mulgrhm2  14487  zlmlemg  14505  zlmsca  14509  zlmvscag  14510  znval  14513  znle  14514  znbaslemnn  14516  znidomb  14535  psrval  14543  psrbasg  14551  psrplusgg  14555  mplvalcoe  14567  mplsubgfileminv  14577  mpl0fi  14579  mplnegfi  14582  istps  14619  tpspropd  14623  eltpsg  14627  txvalex  14841  txval  14842  txbasval  14854  upxp  14859  uptx  14861  txrest  14863  cnmpt11  14870  cnmpt21  14878  hmeontr  14900  txhmeo  14906  psmetxrge0  14919  xmetunirn  14945  mopnval  15029  mopntopon  15030  isxms  15038  isxms2  15039  isms  15040  msrtri  15063  xmspropd  15064  mspropd  15065  setsmsbasg  15066  setsmsdsg  15067  setsmstsetg  15068  comet  15086  metcnpi  15102  metcnpi2  15103  cnbl0  15121  cnblcld  15122  resubmet  15143  mpomulcn  15153  elcncf  15160  cncfi  15165  rescncf  15168  mulc1cncf  15176  cncfco  15178  cncfmptid  15184  addccncf  15187  cdivcncfap  15191  negcncf  15192  mulcncflem  15194  ivthinclemlopn  15223  ivthinclemuopn  15225  limccl  15246  ellimc3apf  15247  limcimolemlt  15251  cnplimclemle  15255  limccnpcntop  15262  reldvg  15266  dvfvalap  15268  dveflem  15313  dvef  15314  plymullem1  15335  plycjlemc  15347  plycj  15348  plyrecj  15350  plyreres  15351  sin0pilem1  15368  ef2kpi  15393  sinperlem  15395  sin2kpi  15398  cos2kpi  15399  sin2pim  15400  cos2pim  15401  ptolemy  15411  sincosq2sgn  15414  sincosq3sgn  15415  sincosq4sgn  15416  sinq12gt0  15417  tangtx  15425  sincosq1eq  15426  abssinper  15433  sinkpi  15434  coskpi  15435  cosq34lt1  15437  relogeftb  15452  relogoprlem  15455  relogexp  15459  rpcxpef  15481  logcxp  15484  1cxp  15487  ecxp  15488  rpcxpadd  15492  rpmulcxp  15496  cxpmul  15499  abscxp  15502  logsqrt  15510  rpabscxpbnd  15527  rpcxplogb  15551  lgsval  15596  lgsval2lem  15602  lgsval4a  15614  lgsdi  15629  lgseisenlem3  15664  lgseisenlem4  15665  lgsquadlem1  15669  lgsquadlem2  15670  lgsquadlem3  15671  2lgslem1  15683  2lgslem3a  15685  2lgslem3b  15686  2lgslem3c  15687  2lgslem3d  15688  nnsf  16144  peano4nninf  16145  peano3nninf  16146  nninfalllem1  16147  nninfall  16148  nninfsellemdc  16149  nninfsellemeq  16153  nninfsellemqall  16154  nninfsellemeqinf  16155  nninfsel  16156  nnnninfex  16161  exmidsbthr  16164  qdencn  16168  refeq  16169  isomninnlem  16171  apdifflemr  16188  apdiff  16189  ismkvnnlem  16193  nconstwlpolem  16206