Theorem fveq2d 5631

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

Syntax hints:   -> wi 4   = wceq 1395   ` cfv 5318

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 714  ax-5 1493  ax-7 1494  ax-gen 1495  ax-ie1 1539  ax-ie2 1540  ax-8 1550  ax-10 1551  ax-11 1552  ax-i12 1553  ax-bndl 1555  ax-4 1556  ax-17 1572  ax-i9 1576  ax-ial 1580  ax-i5r 1581  ax-ext 2211

This theorem depends on definitions:  df-bi 117  df-3an 1004  df-tru 1398  df-nf 1507  df-sb 1809  df-clab 2216  df-cleq 2222  df-clel 2225  df-nfc 2361  df-rex 2514  df-v 2801  df-un 3201  df-sn 3672  df-pr 3673  df-op 3675  df-uni 3889  df-br 4084  df-iota 5278  df-fv 5326

This theorem is referenced by:  2fveq3  5632  fveq12d  5634  fveqeq2d  5635  csbfvg  5669  fvmptdf  5722  fvmptt  5726  fcof1  5907  oveq1  6008  oveq2  6009  fvoveq1d  6023  caofinvl  6244  op1stg  6296  op2ndg  6297  ot1stg  6298  ot2ndg  6299  eloprabi  6342  1stconst  6367  algrflemg  6376  tfrlem1  6454  tfrlem3ag  6455  tfrlem3a  6456  tfrlem9  6465  tfr0dm  6468  tfrlemisucaccv  6471  tfrlemiubacc  6476  tfrlemiex  6477  tfrlemi1  6478  tfr1onlem3ag  6483  tfr1onlemsucaccv  6487  tfr1onlemubacc  6492  tfr1onlemex  6493  tfr1onlemaccex  6494  tfrcllemsucaccv  6500  tfrcllembxssdm  6502  tfrcllemubacc  6505  tfrcllemex  6506  tfrcllemaccex  6507  tfrcllemres  6508  tfrcldm  6509  rdgivallem  6527  rdgival  6528  rdgss  6529  rdgisuc1  6530  rdgon  6532  rdg0  6533  frec0g  6543  frecabcl  6545  freccllem  6548  frecfcllem  6550  frecsuclem  6552  frecsuc  6553  frecrdg  6554  oav2  6609  omv2  6611  xpdom2  6990  xpmapenlem  7010  xpmapen  7011  ac6sfi  7060  1stinl  7241  2ndinl  7242  1stinr  7243  2ndinr  7244  updjudhcoinlf  7247  updjudhcoinrg  7248  caseinl  7258  caseinr  7259  omp1eomlem  7261  omp1eom  7262  difinfsn  7267  ctmlemr  7275  ctm  7276  ctssdclemn0  7277  ctssdccl  7278  nninfninc  7290  nnnninfeq  7295  nnnninfeq2  7296  enomnilem  7305  enmkvlem  7328  enwomnilem  7336  exmidfodomrlemeldju  7377  exmidfodomrlemreseldju  7378  exmidfodomrlemr  7380  exmidfodomrlemrALT  7381  exmidaclem  7390  cc2  7453  cc3  7454  ltdfpr  7693  genpelvl  7699  genpelvu  7700  recexpr  7825  cauappcvgprlem1  7846  caucvgprlemnkj  7853  caucvgprlemnbj  7854  caucvgprlemm  7855  caucvgprlemdisj  7861  caucvgprlemloc  7862  caucvgprlemcl  7863  caucvgprlemladdfu  7864  caucvgprlemladdrl  7865  caucvgprlem1  7866  caucvgprlem2  7867  caucvgpr  7869  caucvgprprlemell  7872  caucvgprprlemelu  7873  caucvgprprlemcbv  7874  caucvgprprlemval  7875  caucvgprprlemnkeqj  7877  caucvgprprlemmu  7882  caucvgprprlemopl  7884  caucvgprprlemlol  7885  caucvgprprlemopu  7886  caucvgprprlemloc  7890  caucvgprprlemclphr  7892  caucvgprprlemexbt  7893  caucvgprprlem1  7896  caucvgprprlem2  7897  caucvgsr  7989  axcaucvglemval  8084  axcaucvglemres  8086  fv0p1e1  9225  uzin  9755  cnref1o  9846  fzsuc2  10275  fseq1m1p1  10291  fzoss2  10370  elfzonlteqm1  10416  divfl0  10516  flqzadd  10518  fldiv4p1lem1div2  10525  ceilqval  10528  flqdiv  10543  modqval  10546  modqfrac  10559  modqmulnn  10564  modqid  10571  modqcyc  10581  modqdi  10614  frec2uzuzd  10624  frec2uzrdg  10631  frecuzrdgrcl  10632  frecuzrdgtcl  10634  frecuzrdgsuc  10636  frecuzrdgrclt  10637  frecuzrdgg  10638  frecuzrdgfunlem  10641  frecuzrdgsuctlem  10645  iseqovex  10680  iseqvalcbv  10681  seq3val  10682  seqvalcd  10683  seq3m1  10695  seq3shft2  10703  seqshft2g  10704  monoord  10707  monoord2  10708  iseqf1olemqval  10722  iseqf1olemab  10724  iseqf1olemqk  10729  iseqf1olemjpcl  10730  iseqf1olemqpcl  10731  iseqf1olemfvp  10732  seq3f1olemqsumkj  10733  seq3f1olemqsumk  10734  seq3f1olemqsum  10735  seq3f1olemp  10737  seq3f1oleml  10738  seqf1oglem1  10741  seqf1oglem2  10742  seqf1og  10743  seq3homo  10749  seqhomog  10752  exp3val  10763  expnegap0  10769  facnn2  10956  facwordi  10962  faclbnd6  10966  bcval  10971  bccmpl  10976  bcn0  10977  bcm1k  10982  bcp1n  10983  bcn2  10986  hashinfom  11000  hashennn  11002  hashsng  11020  omgadd  11024  hashprg  11030  fihashssdif  11040  hashdifpr  11042  hashfzo  11044  hashfzp1  11046  hashxp  11048  zfz1isolemiso  11061  zfz1iso  11063  lsw1  11121  ccatfvalfi  11127  ccatlen  11130  ccatval3  11134  ccatval21sw  11140  ccatlid  11141  ccatass  11143  lswccatn0lsw  11146  lswccat0lsw  11147  s1leng  11157  ccats1val2  11171  lswccats1  11174  swrdfv0  11186  swrdfv2  11195  swrdsbslen  11198  swrds1  11200  ccatswrd  11202  pfxmpt  11212  pfxfv  11216  pfxtrcfvl  11229  ccatpfx  11233  swrdswrd  11237  lenpfxcctswrd  11243  ccatopth  11248  cats1un  11253  swrdccatin2  11261  pfxccatin12lem2  11263  shftval2  11337  shftval3  11338  shftval4  11339  shftval5  11340  seq3shft  11349  imval  11361  imre  11362  reim  11363  crim  11369  reim0  11372  mulreap  11375  recj  11378  reneg  11379  readd  11380  resub  11381  remullem  11382  redivap  11385  imcj  11386  imneg  11387  imadd  11388  imsub  11389  imdivap  11392  cjsub  11403  cjexp  11404  cjreim2  11415  cjap  11417  cjdivap  11420  cnrecnv  11421  cvg1nlemcau  11495  cvg1nlemres  11496  absval  11512  rennim  11513  sqrtdiv  11553  sqrtmsq  11556  absneg  11561  abscj  11563  absval2  11568  absreim  11579  absmul  11580  absdivap  11581  absid  11582  absre  11588  absexp  11590  absexpzap  11591  absimle  11595  abssub  11612  abs3dif  11616  abs2dif  11617  abs2dif2  11618  recan  11620  cau3lem  11625  max0addsup  11730  minabs  11747  bdtrilem  11750  clim  11792  clim2  11794  clim0  11796  clim0c  11797  climi0  11800  climconst  11801  climshftlemg  11813  climcn1  11819  climcn2  11820  addcn2  11821  subcn2  11822  mulcn2  11823  reccn2ap  11824  cjcn2  11827  recn2  11828  imcn2  11829  iser3shft  11857  climcau  11858  climcvg1nlem  11860  climcvg1n  11861  serf0  11863  summodclem3  11891  summodclem2a  11892  summodc  11894  fsumf1o  11901  sumsnf  11920  fsumm1  11927  fsumcnv  11948  fsumabs  11976  fsumrelem  11982  iserabs  11986  hash2iun1dif1  11991  isumshft  12001  isumsplit  12002  expcnvap0  12013  expcnv  12015  cvgratnnlemseq  12037  cvgratnnlemrate  12041  cvgratz  12043  mertenslemub  12045  mertenslemi1  12046  mertenslem2  12047  mertensabs  12048  prodmodclem3  12086  fprodf1o  12099  prodsnf  12103  fprodm1  12109  fprodabs  12127  fprodcnv  12136  efcllemp  12169  efcj  12184  efaddlem  12185  efcan  12187  efsub  12192  efexp  12193  efzval  12194  efgt0  12195  eftlub  12201  efltim  12209  sinval  12213  cosval  12214  tanval3ap  12225  resinval  12226  recosval  12227  resin4p  12229  recos4p  12230  sinneg  12237  cosneg  12238  efmival  12244  efeul  12245  sinadd  12247  cosadd  12248  sinsub  12251  cossub  12252  addsin  12253  subsin  12254  addcos  12257  subcos  12258  sincossq  12259  sin2t  12260  cos2t  12261  sin01bnd  12268  cos01bnd  12269  sin02gt0  12275  cos12dec  12279  absefi  12280  absef  12281  absefib  12282  efieq1re  12283  demoivre  12284  demoivreALT  12285  flodddiv4  12447  bitsval  12454  bits0  12459  bitsp1  12462  bitsp1e  12463  bitsp1o  12464  bitsmod  12467  nninfctlemfo  12561  alginv  12569  algcvg  12570  eucalgval  12576  eucalginv  12578  eucalglt  12579  eucalgcvga  12580  eucalg  12581  lcmgcd  12600  lcm1  12603  sqpweven  12697  2sqpwodd  12698  sqne2sq  12699  qnumval  12707  qdenval  12708  qden1elz  12727  nn0sqrtelqelz  12728  phival  12735  dfphi2  12742  phiprmpw  12744  phiprm  12745  eulerthlemth  12754  hashgcdeq  12762  phisum  12763  pythagtriplem6  12793  pythagtriplem7  12794  pythagtriplem12  12798  pythagtriplem14  12800  fldivp1  12871  4sqlem11  12924  ennnfonelemg  12974  ennnfonelemp1  12977  ennnfonelemkh  12983  ennnfonelemhf1o  12984  ennnfonelemnn0  12993  ctinfomlemom  12998  ctiunctlemu1st  13005  ctiunctlemu2nd  13006  ctiunctlemudc  13008  ctiunctlemfo  13010  isstruct2im  13042  isstruct2r  13043  setsslid  13083  ressbasd  13100  resseqnbasd  13106  ressplusgd  13162  ptex  13297  prdsex  13302  prdsval  13306  prdsbas3  13320  pwsval  13324  pwsbas  13325  pwsplusgval  13328  pwsmulrval  13329  imasex  13338  imasival  13339  f1ocpbl  13344  f1ovscpbl  13345  imasaddvallemg  13348  qusval  13356  fvprif  13376  xpsff1o  13382  igsumvalx  13422  gsumprval  13432  pws0g  13484  imasmnd  13486  ismhm  13494  mhmpropd  13499  mhmlin  13500  mhmf1o  13503  resmhm  13520  mhmco  13523  gsumwmhm  13531  grpinvsub  13615  pwsinvg  13645  imasgrp2  13647  imasgrp  13648  mhmlem  13651  mhmid  13652  mhmmnd  13653  ghmgrp  13655  mulgfvalg  13658  mulgval  13659  mulgnegnn  13669  mulgneg  13677  mulgnegneg  13678  mulgm1  13679  mulginvcom  13684  mulgz  13687  mulgnndir  13688  mulgdir  13691  mulgass  13696  mhmmulg  13700  subgmulg  13725  isnsg  13739  eqgfval  13759  ghmlin  13785  ghmid  13786  ghminv  13787  ghmsub  13788  ghmmulg  13793  resghm  13797  ghmeql  13804  ablsub2inv  13848  ghmcmn  13864  invghm  13866  imasabl  13873  gsumfzreidx  13874  gsumfzmhm  13880  mgpplusgg  13887  mgpbasg  13889  mgpscag  13890  mgptsetg  13891  mgpdsg  13893  rngm2neg  13912  imasrng  13919  isring  13963  ringm2neg  14018  imasring  14027  opprmulfvalg  14033  opprsllem  14037  isunitd  14070  opprunitd  14074  invrfvald  14086  rdivmuldivd  14108  rhmmul  14128  isrhm2d  14129  rhm1  14131  rhmdvdsr  14139  rhmopp  14140  rhmunitinv  14142  islmod  14255  islmodd  14257  scaffvalg  14270  lmodpropd  14313  lsssetm  14320  islssmd  14323  lssats2  14378  lspsnneg  14384  lspsnsub  14385  lspun0  14389  lmodindp1  14392  sralemg  14402  srascag  14406  sravscag  14407  sraipg  14408  rlmscabas  14424  ixpsnbasval  14430  2idlval  14466  2idlvalg  14467  mulgrhm2  14574  zlmlemg  14592  zlmsca  14596  zlmvscag  14597  znval  14600  znle  14601  znbaslemnn  14603  znidomb  14622  psrval  14630  psrbasg  14638  psrplusgg  14642  mplvalcoe  14654  mplsubgfileminv  14664  mpl0fi  14666  mplnegfi  14669  istps  14706  tpspropd  14710  eltpsg  14714  txvalex  14928  txval  14929  txbasval  14941  upxp  14946  uptx  14948  txrest  14950  cnmpt11  14957  cnmpt21  14965  hmeontr  14987  txhmeo  14993  psmetxrge0  15006  xmetunirn  15032  mopnval  15116  mopntopon  15117  isxms  15125  isxms2  15126  isms  15127  msrtri  15150  xmspropd  15151  mspropd  15152  setsmsbasg  15153  setsmsdsg  15154  setsmstsetg  15155  comet  15173  metcnpi  15189  metcnpi2  15190  cnbl0  15208  cnblcld  15209  resubmet  15230  mpomulcn  15240  elcncf  15247  cncfi  15252  rescncf  15255  mulc1cncf  15263  cncfco  15265  cncfmptid  15271  addccncf  15274  cdivcncfap  15278  negcncf  15279  mulcncflem  15281  ivthinclemlopn  15310  ivthinclemuopn  15312  limccl  15333  ellimc3apf  15334  limcimolemlt  15338  cnplimclemle  15342  limccnpcntop  15349  reldvg  15353  dvfvalap  15355  dveflem  15400  dvef  15401  plymullem1  15422  plycjlemc  15434  plycj  15435  plyrecj  15437  plyreres  15438  sin0pilem1  15455  ef2kpi  15480  sinperlem  15482  sin2kpi  15485  cos2kpi  15486  sin2pim  15487  cos2pim  15488  ptolemy  15498  sincosq2sgn  15501  sincosq3sgn  15502  sincosq4sgn  15503  sinq12gt0  15504  tangtx  15512  sincosq1eq  15513  abssinper  15520  sinkpi  15521  coskpi  15522  cosq34lt1  15524  relogeftb  15539  relogoprlem  15542  relogexp  15546  rpcxpef  15568  logcxp  15571  1cxp  15574  ecxp  15575  rpcxpadd  15579  rpmulcxp  15583  cxpmul  15586  abscxp  15589  logsqrt  15597  rpabscxpbnd  15614  rpcxplogb  15638  lgsval  15683  lgsval2lem  15689  lgsval4a  15701  lgsdi  15716  lgseisenlem3  15751  lgseisenlem4  15752  lgsquadlem1  15756  lgsquadlem2  15757  lgsquadlem3  15758  2lgslem1  15770  2lgslem3a  15772  2lgslem3b  15773  2lgslem3c  15774  2lgslem3d  15775  iswlk  16036  nnsf  16371  peano4nninf  16372  peano3nninf  16373  nninfalllem1  16374  nninfall  16375  nninfsellemdc  16376  nninfsellemeq  16380  nninfsellemqall  16381  nninfsellemeqinf  16382  nninfsel  16383  nnnninfex  16388  exmidsbthr  16391  qdencn  16395  refeq  16396  isomninnlem  16398  apdifflemr  16415  apdiff  16416  ismkvnnlem  16420  nconstwlpolem  16433