Theorem fveq2d 5582

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 5578	. 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 5272

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 1470  ax-7 1471  ax-gen 1472  ax-ie1 1516  ax-ie2 1517  ax-8 1527  ax-10 1528  ax-11 1529  ax-i12 1530  ax-bndl 1532  ax-4 1533  ax-17 1549  ax-i9 1553  ax-ial 1557  ax-i5r 1558  ax-ext 2187

This theorem depends on definitions:  df-bi 117  df-3an 983  df-tru 1376  df-nf 1484  df-sb 1786  df-clab 2192  df-cleq 2198  df-clel 2201  df-nfc 2337  df-rex 2490  df-v 2774  df-un 3170  df-sn 3639  df-pr 3640  df-op 3642  df-uni 3851  df-br 4046  df-iota 5233  df-fv 5280

This theorem is referenced by:  2fveq3  5583  fveq12d  5585  fveqeq2d  5586  csbfvg  5618  fvmptdf  5669  fvmptt  5673  fcof1  5854  oveq1  5953  oveq2  5954  fvoveq1d  5968  caofinvl  6186  op1stg  6238  op2ndg  6239  ot1stg  6240  ot2ndg  6241  eloprabi  6284  1stconst  6309  algrflemg  6318  tfrlem1  6396  tfrlem3ag  6397  tfrlem3a  6398  tfrlem9  6407  tfr0dm  6410  tfrlemisucaccv  6413  tfrlemiubacc  6418  tfrlemiex  6419  tfrlemi1  6420  tfr1onlem3ag  6425  tfr1onlemsucaccv  6429  tfr1onlemubacc  6434  tfr1onlemex  6435  tfr1onlemaccex  6436  tfrcllemsucaccv  6442  tfrcllembxssdm  6444  tfrcllemubacc  6447  tfrcllemex  6448  tfrcllemaccex  6449  tfrcllemres  6450  tfrcldm  6451  rdgivallem  6469  rdgival  6470  rdgss  6471  rdgisuc1  6472  rdgon  6474  rdg0  6475  frec0g  6485  frecabcl  6487  freccllem  6490  frecfcllem  6492  frecsuclem  6494  frecsuc  6495  frecrdg  6496  oav2  6551  omv2  6553  xpdom2  6928  xpmapenlem  6948  xpmapen  6949  ac6sfi  6997  1stinl  7178  2ndinl  7179  1stinr  7180  2ndinr  7181  updjudhcoinlf  7184  updjudhcoinrg  7185  caseinl  7195  caseinr  7196  omp1eomlem  7198  omp1eom  7199  difinfsn  7204  ctmlemr  7212  ctm  7213  ctssdclemn0  7214  ctssdccl  7215  nninfninc  7227  nnnninfeq  7232  nnnninfeq2  7233  enomnilem  7242  enmkvlem  7265  enwomnilem  7273  exmidfodomrlemeldju  7309  exmidfodomrlemreseldju  7310  exmidfodomrlemr  7312  exmidfodomrlemrALT  7313  exmidaclem  7322  cc2  7381  cc3  7382  ltdfpr  7621  genpelvl  7627  genpelvu  7628  recexpr  7753  cauappcvgprlem1  7774  caucvgprlemnkj  7781  caucvgprlemnbj  7782  caucvgprlemm  7783  caucvgprlemdisj  7789  caucvgprlemloc  7790  caucvgprlemcl  7791  caucvgprlemladdfu  7792  caucvgprlemladdrl  7793  caucvgprlem1  7794  caucvgprlem2  7795  caucvgpr  7797  caucvgprprlemell  7800  caucvgprprlemelu  7801  caucvgprprlemcbv  7802  caucvgprprlemval  7803  caucvgprprlemnkeqj  7805  caucvgprprlemmu  7810  caucvgprprlemopl  7812  caucvgprprlemlol  7813  caucvgprprlemopu  7814  caucvgprprlemloc  7818  caucvgprprlemclphr  7820  caucvgprprlemexbt  7821  caucvgprprlem1  7824  caucvgprprlem2  7825  caucvgsr  7917  axcaucvglemval  8012  axcaucvglemres  8014  fv0p1e1  9153  uzin  9683  cnref1o  9774  fzsuc2  10203  fseq1m1p1  10219  fzoss2  10298  elfzonlteqm1  10341  divfl0  10441  flqzadd  10443  fldiv4p1lem1div2  10450  ceilqval  10453  flqdiv  10468  modqval  10471  modqfrac  10484  modqmulnn  10489  modqid  10496  modqcyc  10506  modqdi  10539  frec2uzuzd  10549  frec2uzrdg  10556  frecuzrdgrcl  10557  frecuzrdgtcl  10559  frecuzrdgsuc  10561  frecuzrdgrclt  10562  frecuzrdgg  10563  frecuzrdgfunlem  10566  frecuzrdgsuctlem  10570  iseqovex  10605  iseqvalcbv  10606  seq3val  10607  seqvalcd  10608  seq3m1  10620  seq3shft2  10628  seqshft2g  10629  monoord  10632  monoord2  10633  iseqf1olemqval  10647  iseqf1olemab  10649  iseqf1olemqk  10654  iseqf1olemjpcl  10655  iseqf1olemqpcl  10656  iseqf1olemfvp  10657  seq3f1olemqsumkj  10658  seq3f1olemqsumk  10659  seq3f1olemqsum  10660  seq3f1olemp  10662  seq3f1oleml  10663  seqf1oglem1  10666  seqf1oglem2  10667  seqf1og  10668  seq3homo  10674  seqhomog  10677  exp3val  10688  expnegap0  10694  facnn2  10881  facwordi  10887  faclbnd6  10891  bcval  10896  bccmpl  10901  bcn0  10902  bcm1k  10907  bcp1n  10908  bcn2  10911  hashinfom  10925  hashennn  10927  hashsng  10945  omgadd  10949  hashprg  10955  fihashssdif  10965  hashdifpr  10967  hashfzo  10969  hashfzp1  10971  hashxp  10973  zfz1isolemiso  10986  zfz1iso  10988  lsw1  11045  ccatfvalfi  11051  ccatlen  11054  ccatval3  11058  ccatval21sw  11064  ccatlid  11065  ccatass  11067  lswccatn0lsw  11070  lswccat0lsw  11071  s1leng  11081  ccats1val2  11095  lswccats1  11098  swrdfv0  11110  swrdfv2  11119  swrdsbslen  11122  swrds1  11124  ccatswrd  11126  pfxmpt  11134  pfxfv  11138  pfxtrcfvl  11151  ccatpfx  11155  shftval2  11170  shftval3  11171  shftval4  11172  shftval5  11173  seq3shft  11182  imval  11194  imre  11195  reim  11196  crim  11202  reim0  11205  mulreap  11208  recj  11211  reneg  11212  readd  11213  resub  11214  remullem  11215  redivap  11218  imcj  11219  imneg  11220  imadd  11221  imsub  11222  imdivap  11225  cjsub  11236  cjexp  11237  cjreim2  11248  cjap  11250  cjdivap  11253  cnrecnv  11254  cvg1nlemcau  11328  cvg1nlemres  11329  absval  11345  rennim  11346  sqrtdiv  11386  sqrtmsq  11389  absneg  11394  abscj  11396  absval2  11401  absreim  11412  absmul  11413  absdivap  11414  absid  11415  absre  11421  absexp  11423  absexpzap  11424  absimle  11428  abssub  11445  abs3dif  11449  abs2dif  11450  abs2dif2  11451  recan  11453  cau3lem  11458  max0addsup  11563  minabs  11580  bdtrilem  11583  clim  11625  clim2  11627  clim0  11629  clim0c  11630  climi0  11633  climconst  11634  climshftlemg  11646  climcn1  11652  climcn2  11653  addcn2  11654  subcn2  11655  mulcn2  11656  reccn2ap  11657  cjcn2  11660  recn2  11661  imcn2  11662  iser3shft  11690  climcau  11691  climcvg1nlem  11693  climcvg1n  11694  serf0  11696  summodclem3  11724  summodclem2a  11725  summodc  11727  fsumf1o  11734  sumsnf  11753  fsumm1  11760  fsumcnv  11781  fsumabs  11809  fsumrelem  11815  iserabs  11819  hash2iun1dif1  11824  isumshft  11834  isumsplit  11835  expcnvap0  11846  expcnv  11848  cvgratnnlemseq  11870  cvgratnnlemrate  11874  cvgratz  11876  mertenslemub  11878  mertenslemi1  11879  mertenslem2  11880  mertensabs  11881  prodmodclem3  11919  fprodf1o  11932  prodsnf  11936  fprodm1  11942  fprodabs  11960  fprodcnv  11969  efcllemp  12002  efcj  12017  efaddlem  12018  efcan  12020  efsub  12025  efexp  12026  efzval  12027  efgt0  12028  eftlub  12034  efltim  12042  sinval  12046  cosval  12047  tanval3ap  12058  resinval  12059  recosval  12060  resin4p  12062  recos4p  12063  sinneg  12070  cosneg  12071  efmival  12077  efeul  12078  sinadd  12080  cosadd  12081  sinsub  12084  cossub  12085  addsin  12086  subsin  12087  addcos  12090  subcos  12091  sincossq  12092  sin2t  12093  cos2t  12094  sin01bnd  12101  cos01bnd  12102  sin02gt0  12108  cos12dec  12112  absefi  12113  absef  12114  absefib  12115  efieq1re  12116  demoivre  12117  demoivreALT  12118  flodddiv4  12280  bitsval  12287  bits0  12292  bitsp1  12295  bitsp1e  12296  bitsp1o  12297  bitsmod  12300  nninfctlemfo  12394  alginv  12402  algcvg  12403  eucalgval  12409  eucalginv  12411  eucalglt  12412  eucalgcvga  12413  eucalg  12414  lcmgcd  12433  lcm1  12436  sqpweven  12530  2sqpwodd  12531  sqne2sq  12532  qnumval  12540  qdenval  12541  qden1elz  12560  nn0sqrtelqelz  12561  phival  12568  dfphi2  12575  phiprmpw  12577  phiprm  12578  eulerthlemth  12587  hashgcdeq  12595  phisum  12596  pythagtriplem6  12626  pythagtriplem7  12627  pythagtriplem12  12631  pythagtriplem14  12633  fldivp1  12704  4sqlem11  12757  ennnfonelemg  12807  ennnfonelemp1  12810  ennnfonelemkh  12816  ennnfonelemhf1o  12817  ennnfonelemnn0  12826  ctinfomlemom  12831  ctiunctlemu1st  12838  ctiunctlemu2nd  12839  ctiunctlemudc  12841  ctiunctlemfo  12843  isstruct2im  12875  isstruct2r  12876  setsslid  12916  ressbasd  12932  resseqnbasd  12938  ressplusgd  12994  ptex  13129  prdsex  13134  prdsval  13138  prdsbas3  13152  pwsval  13156  pwsbas  13157  pwsplusgval  13160  pwsmulrval  13161  imasex  13170  imasival  13171  f1ocpbl  13176  f1ovscpbl  13177  imasaddvallemg  13180  qusval  13188  fvprif  13208  xpsff1o  13214  igsumvalx  13254  gsumprval  13264  pws0g  13316  imasmnd  13318  ismhm  13326  mhmpropd  13331  mhmlin  13332  mhmf1o  13335  resmhm  13352  mhmco  13355  gsumwmhm  13363  grpinvsub  13447  pwsinvg  13477  imasgrp2  13479  imasgrp  13480  mhmlem  13483  mhmid  13484  mhmmnd  13485  ghmgrp  13487  mulgfvalg  13490  mulgval  13491  mulgnegnn  13501  mulgneg  13509  mulgnegneg  13510  mulgm1  13511  mulginvcom  13516  mulgz  13519  mulgnndir  13520  mulgdir  13523  mulgass  13528  mhmmulg  13532  subgmulg  13557  isnsg  13571  eqgfval  13591  ghmlin  13617  ghmid  13618  ghminv  13619  ghmsub  13620  ghmmulg  13625  resghm  13629  ghmeql  13636  ablsub2inv  13680  ghmcmn  13696  invghm  13698  imasabl  13705  gsumfzreidx  13706  gsumfzmhm  13712  mgpplusgg  13719  mgpbasg  13721  mgpscag  13722  mgptsetg  13723  mgpdsg  13725  rngm2neg  13744  imasrng  13751  isring  13795  ringm2neg  13850  imasring  13859  opprmulfvalg  13865  opprsllem  13869  isunitd  13901  opprunitd  13905  invrfvald  13917  rdivmuldivd  13939  rhmmul  13959  isrhm2d  13960  rhm1  13962  rhmdvdsr  13970  rhmopp  13971  rhmunitinv  13973  islmod  14086  islmodd  14088  scaffvalg  14101  lmodpropd  14144  lsssetm  14151  islssmd  14154  lssats2  14209  lspsnneg  14215  lspsnsub  14216  lspun0  14220  lmodindp1  14223  sralemg  14233  srascag  14237  sravscag  14238  sraipg  14239  rlmscabas  14255  ixpsnbasval  14261  2idlval  14297  2idlvalg  14298  mulgrhm2  14405  zlmlemg  14423  zlmsca  14427  zlmvscag  14428  znval  14431  znle  14432  znbaslemnn  14434  znidomb  14453  psrval  14461  psrbasg  14469  psrplusgg  14473  mplvalcoe  14485  mplsubgfileminv  14495  mpl0fi  14497  mplnegfi  14500  istps  14537  tpspropd  14541  eltpsg  14545  txvalex  14759  txval  14760  txbasval  14772  upxp  14777  uptx  14779  txrest  14781  cnmpt11  14788  cnmpt21  14796  hmeontr  14818  txhmeo  14824  psmetxrge0  14837  xmetunirn  14863  mopnval  14947  mopntopon  14948  isxms  14956  isxms2  14957  isms  14958  msrtri  14981  xmspropd  14982  mspropd  14983  setsmsbasg  14984  setsmsdsg  14985  setsmstsetg  14986  comet  15004  metcnpi  15020  metcnpi2  15021  cnbl0  15039  cnblcld  15040  resubmet  15061  mpomulcn  15071  elcncf  15078  cncfi  15083  rescncf  15086  mulc1cncf  15094  cncfco  15096  cncfmptid  15102  addccncf  15105  cdivcncfap  15109  negcncf  15110  mulcncflem  15112  ivthinclemlopn  15141  ivthinclemuopn  15143  limccl  15164  ellimc3apf  15165  limcimolemlt  15169  cnplimclemle  15173  limccnpcntop  15180  reldvg  15184  dvfvalap  15186  dveflem  15231  dvef  15232  plymullem1  15253  plycjlemc  15265  plycj  15266  plyrecj  15268  plyreres  15269  sin0pilem1  15286  ef2kpi  15311  sinperlem  15313  sin2kpi  15316  cos2kpi  15317  sin2pim  15318  cos2pim  15319  ptolemy  15329  sincosq2sgn  15332  sincosq3sgn  15333  sincosq4sgn  15334  sinq12gt0  15335  tangtx  15343  sincosq1eq  15344  abssinper  15351  sinkpi  15352  coskpi  15353  cosq34lt1  15355  relogeftb  15370  relogoprlem  15373  relogexp  15377  rpcxpef  15399  logcxp  15402  1cxp  15405  ecxp  15406  rpcxpadd  15410  rpmulcxp  15414  cxpmul  15417  abscxp  15420  logsqrt  15428  rpabscxpbnd  15445  rpcxplogb  15469  lgsval  15514  lgsval2lem  15520  lgsval4a  15532  lgsdi  15547  lgseisenlem3  15582  lgseisenlem4  15583  lgsquadlem1  15587  lgsquadlem2  15588  lgsquadlem3  15589  2lgslem1  15601  2lgslem3a  15603  2lgslem3b  15604  2lgslem3c  15605  2lgslem3d  15606  nnsf  15979  peano4nninf  15980  peano3nninf  15981  nninfalllem1  15982  nninfall  15983  nninfsellemdc  15984  nninfsellemeq  15988  nninfsellemqall  15989  nninfsellemeqinf  15990  nninfsel  15991  nnnninfex  15996  exmidsbthr  15999  qdencn  16003  refeq  16004  isomninnlem  16006  apdifflemr  16023  apdiff  16024  ismkvnnlem  16028  nconstwlpolem  16041