Theorem fveq2d 5699

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

This proof depends on syntax axioms:   -> wi 4   = wceq 1402   ` cfv 5377

This proof depends on axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-ia1 106  ax-ia2 107  ax-ia3 108  ax-io 721  ax-5 1500  ax-7 1501  ax-gen 1502  ax-ie1 1546  ax-ie2 1547  ax-8 1557  ax-10 1558  ax-11 1559  ax-i12 1560  ax-bndl 1562  ax-4 1563  ax-17 1579  ax-i9 1583  ax-ial 1587  ax-i5r 1588  ax-ext 2220

This proof depends on definitions:  df-bi 117  df-3an 1011  df-tru 1405  df-nf 1514  df-sb 1816  df-clab 2225  df-cleq 2231  df-clel 2234  df-nfc 2381  df-rex 2534  df-v 2823  df-un 3224  df-sn 3715  df-pr 3716  df-op 3718  df-uni 3936  df-br 4131  df-iota 5337  df-fv 5385

This theorem is used by:  2fveq3  5700  fveq12d  5702  fveqeq2d  5703  csbfvg  5738  fvmptdf  5793  fvmptt  5797  resfvresima  5956  fcof1  5989  oveq1  6092  oveq2  6093  fvoveq1d  6107  caofinvl  6328  op1stg  6384  op2ndg  6385  ot1stg  6386  ot2ndg  6387  eloprabi  6432  1stconst  6457  algrflemg  6466  tfrlem1  6579  tfrlem3ag  6580  tfrlem3a  6581  tfrlem9  6590  tfr0dm  6593  tfrlemisucaccv  6596  tfrlemiubacc  6601  tfrlemiex  6602  tfrlemi1  6603  tfr1onlem3ag  6608  tfr1onlemsucaccv  6612  tfr1onlemubacc  6617  tfr1onlemex  6618  tfr1onlemaccex  6619  tfrcllemsucaccv  6625  tfrcllembxssdm  6627  tfrcllemubacc  6630  tfrcllemex  6631  tfrcllemaccex  6632  tfrcllemres  6633  tfrcldm  6634  rdgivallem  6652  rdgival  6653  rdgss  6654  rdgisuc1  6655  rdgon  6657  rdg0  6658  frec0g  6668  frecabcl  6670  freccllem  6673  frecfcllem  6675  frecsuclem  6677  frecsuc  6678  frecrdg  6679  oav2  6736  omv2  6738  xpdom2  7129  xpmapenlem  7149  xpmapen  7150  ac6sfi  7202  1stinl  7415  2ndinl  7416  1stinr  7417  2ndinr  7418  updjudhcoinlf  7421  updjudhcoinrg  7422  caseinl  7432  caseinr  7433  omp1eomlem  7435  omp1eom  7436  difinfsn  7441  ctmlemr  7449  ctm  7450  ctssdclemn0  7451  ctssdccl  7452  nninfninc  7464  nnnninfeq  7469  nnnninfeq2  7470  enomnilem  7479  enmkvlem  7502  enwomnilem  7510  exmidfodomrlemeldju  7552  exmidfodomrlemreseldju  7553  exmidfodomrlemr  7555  exmidfodomrlemrALT  7556  exmidaclem  7565  cc2  7634  cc3  7635  ltdfpr  7874  genpelvl  7880  genpelvu  7881  recexpr  8006  cauappcvgprlem1  8027  caucvgprlemnkj  8034  caucvgprlemnbj  8035  caucvgprlemm  8036  caucvgprlemdisj  8042  caucvgprlemloc  8043  caucvgprlemcl  8044  caucvgprlemladdfu  8045  caucvgprlemladdrl  8046  caucvgprlem1  8047  caucvgprlem2  8048  caucvgpr  8050  caucvgprprlemell  8053  caucvgprprlemelu  8054  caucvgprprlemcbv  8055  caucvgprprlemval  8056  caucvgprprlemnkeqj  8058  caucvgprprlemmu  8063  caucvgprprlemopl  8065  caucvgprprlemlol  8066  caucvgprprlemopu  8067  caucvgprprlemloc  8071  caucvgprprlemclphr  8073  caucvgprprlemexbt  8074  caucvgprprlem1  8077  caucvgprprlem2  8078  caucvgsr  8170  axcaucvglemval  8265  axcaucvglemres  8267  fv0p1e1  9422  uzin  9965  cnref1o  10062  fzsuc2  10497  fseq1m1p1  10513  fzoss2  10592  elfzonlteqm1  10639  divfl0  10746  flqzadd  10748  fldiv4p1lem1div2  10755  ceilqval  10758  flqdiv  10773  modqval  10776  modqfrac  10789  modqmulnn  10794  modqid  10801  modqcyc  10811  modqdi  10844  frec2uzuzd  10854  frec2uzrdg  10861  frecuzrdgrcl  10862  frecuzrdgtcl  10864  frecuzrdgsuc  10866  frecuzrdgrclt  10867  frecuzrdgg  10868  frecuzrdgfunlem  10871  frecuzrdgsuctlem  10875  iseqovex  10910  iseqvalcbv  10911  seq3val  10912  seqvalcd  10913  seq3m1  10925  seq3shft2  10933  seqshft2g  10934  monoord  10937  monoord2  10938  iseqf1olemqval  10952  iseqf1olemab  10954  iseqf1olemqk  10959  iseqf1olemjpcl  10960  iseqf1olemqpcl  10961  iseqf1olemfvp  10962  seq3f1olemqsumkj  10963  seq3f1olemqsumk  10964  seq3f1olemqsum  10965  seq3f1olemp  10967  seq3f1oleml  10968  seqf1oglem1  10971  seqf1oglem2  10972  seqf1og  10973  seq3homo  10979  seqhomog  10982  exp3val  10993  expnegap0  10999  facnn2  11188  facwordi  11194  faclbnd6  11198  bcval  11203  bccmpl  11208  bcn0  11209  bcm1k  11214  bcp1n  11215  bcn2  11218  hashinfom  11233  hashennn  11235  hashsng  11253  omgadd  11258  hashprg  11265  fihashssdif  11275  hashdifpr  11277  hashfzo  11279  hashfzp1  11281  hashxp  11283  hashmap  11284  hashfibclem  11298  hashfibc  11299  hashf1lem2  11302  hashf1  11303  hashfac  11304  zfz1isolemiso  11307  zfz1iso  11309  hashtpglem  11314  lsw1  11370  ccatfvalfi  11376  ccatlen  11379  ccatval3  11383  ccatval21sw  11389  ccatlid  11390  ccatass  11392  lswccatn0lsw  11395  lswccat0lsw  11396  ccatalpha  11397  s1leng  11408  ccats1val2  11424  lswccats1  11427  swrdfv0  11442  swrdfv2  11451  swrdsbslen  11454  swrds1  11456  ccatswrd  11458  pfxmpt  11468  pfxfv  11472  pfxtrcfvl  11485  ccatpfx  11489  swrdswrd  11493  lenpfxcctswrd  11499  ccatopth  11504  cats1un  11509  swrdccatin2  11517  pfxccatin12lem2  11519  shftval2  11607  shftval3  11608  shftval4  11609  shftval5  11610  seq3shft  11619  imval  11631  imre  11632  reim  11633  crim  11639  reim0  11642  mulreap  11645  recj  11648  reneg  11649  readd  11650  resub  11651  remullem  11652  redivap  11655  imcj  11656  imneg  11657  imadd  11658  imsub  11659  imdivap  11662  cjsub  11673  cjexp  11674  cjreim2  11686  cjap  11688  cjdivap  11691  cnrecnv  11692  cvg1nlemcau  11766  cvg1nlemres  11767  absval  11783  rennim  11784  sqrtdiv  11824  sqrtmsq  11827  absneg  11832  abscj  11834  absval2  11839  absreim  11850  absmul  11851  absdivap  11852  absid  11853  absre  11860  absexp  11862  absexpzap  11863  absimle  11867  abssub  11884  abs3dif  11888  abs2dif  11889  abs2dif2  11890  recan  11892  cau3lem  11897  max0addsup  12002  minabs  12020  bdtrilem  12024  clim  12066  clim2  12068  clim0  12070  clim0c  12071  climi0  12074  climconst  12075  climshftlemg  12087  climcn1  12093  climcn2  12094  addcn2  12095  subcn2  12096  mulcn2  12097  reccn2ap  12098  cjcn2  12101  recn2  12102  imcn2  12103  iser3shft  12131  climcau  12132  climcvg1nlem  12134  climcvg1n  12135  serf0  12137  fzf1o  12161  summodclem3  12166  summodclem2a  12167  summodc  12169  fsumf1o  12176  sumsnf  12195  fsumm1  12202  fsumcnv  12223  fsumabs  12251  fsumrelem  12257  iserabs  12261  hash2iun1dif1  12266  isumshft  12276  isumsplit  12277  expcnvap0  12288  expcnv  12290  cvgratnnlemseq  12312  cvgratnnlemrate  12316  cvgratz  12318  mertenslemub  12320  mertenslemi1  12321  mertenslem2  12322  mertensabs  12323  prodmodclem3  12361  fprodf1o  12374  prodsnf  12378  fprodm1  12384  fprodabs  12402  fprodcnv  12411  efcllemp  12444  efcj  12459  efaddlem  12460  efcan  12462  efsub  12467  efexp  12468  efzval  12469  efgt0  12470  eftlub  12476  efltim  12484  sinval  12488  cosval  12489  tanval3ap  12500  resinval  12501  recosval  12502  resin4p  12504  recos4p  12505  sinneg  12512  cosneg  12513  efmival  12519  efeul  12520  sinadd  12522  cosadd  12523  sinsub  12526  cossub  12527  addsin  12528  subsin  12529  addcos  12532  subcos  12533  sincossq  12534  sin2t  12535  cos2t  12536  sin01bnd  12543  cos01bnd  12544  sin02gt0  12550  cos12dec  12554  absefi  12555  absef  12556  absefib  12557  efieq1re  12558  demoivre  12559  demoivreALT  12560  flodddiv4  12722  bitsval  12729  bits0  12734  bitsp1  12737  bitsp1e  12738  bitsp1o  12739  bitsmod  12742  nninfctlemfo  12836  alginv  12844  algcvg  12845  eucalgval  12851  eucalginv  12853  eucalglt  12854  eucalgcvga  12855  eucalg  12856  lcmgcd  12875  lcm1  12878  sqpweven  12974  2sqpwodd  12975  sqne2sq  12976  qnumval  12984  qdenval  12985  qden1elz  13004  nn0sqrtelqelz  13005  nn0sqdcq  13007  sqrtrirr  13008  phival  13014  dfphi2  13021  phiprmpw  13023  phiprm  13024  eulerthlemth  13033  hashgcdeq  13041  phisum  13042  pythagtriplem6  13072  pythagtriplem7  13073  pythagtriplem12  13077  pythagtriplem14  13079  fldivp1  13150  4sqlem11  13203  prmlem0  13243  ballotfilemfval  13281  ballotfilemfp1  13283  ballotfilemfc0  13284  ballotfilemfcc  13285  ballotfilemfmpn  13286  ballotfilemsval  13304  ballotfilemgval  13319  ballotfilemgun  13320  ballotfilemfrc  13322  ballotfilemrinv0  13328  ennnfonelemg  13346  ennnfonelemp1  13349  ennnfonelemkh  13355  ennnfonelemhf1o  13356  ennnfonelemnn0  13365  ctinfomlemom  13370  ctiunctlemu1st  13377  ctiunctlemu2nd  13378  ctiunctlemudc  13380  ctiunctlemfo  13382  isstruct2im  13414  isstruct2r  13415  setsslid  13455  ressbasd  13474  resseqnbasd  13480  ressplusgd  13536  ptex  13671  imasex  13679  imasival  13680  f1ocpbl  13685  f1ovscpbl  13686  imasaddvallemg  13689  qusval  13697  fvprif  13717  xpsff1o  13723  gzsumvalx  13762  imasmnd  13813  ismhm  13821  mhmpropd  13826  mhmlin  13827  mhmf1o  13830  resmhm  13847  mhmco  13850  gzsumwmhm  13856  grpinvsub  13940  imasgrp2  13966  imasgrp  13967  mhmlem  13970  mhmid  13971  mhmmnd  13972  ghmgrp  13974  mulgfvalg  13977  mulgval  13978  mulgnegnn  13988  mulgneg  13996  mulgnegneg  13997  mulgm1  13998  mulginvcom  14003  mulgz  14006  mulgnndir  14007  mulgdir  14010  mulgass  14015  mhmmulg  14019  subgmulg  14044  isnsg  14058  eqgfval  14078  ghmlin  14104  ghmid  14105  ghminv  14106  ghmsub  14107  ghmmulg  14112  resghm  14116  ghmeql  14123  cntzmhm  14167  ablsub2inv  14199  ghmcmn  14215  invghm  14217  imasabl  14224  gzsumreidx  14225  gzsummhm  14229  gzsumsplit0  14232  gzsumshift  14233  gsumvalfi  14236  gsump1  14241  gsumf1ofi  14244  gsummhmfi  14248  prdsex  14256  prdsval  14257  prdsbas3  14271  pwsval  14288  pwsbas  14289  pwsplusgval  14292  pwsmulrval  14293  pws0g  14297  pwsinvg  14299  mgpplusgg  14305  mgpbasg  14308  mgpscag  14310  mgptsetg  14311  mgpdsg  14313  rngm2neg  14332  imasrng  14339  isring  14388  ringm2neg  14444  imasring  14453  opprmulfvalg  14459  opprsllem  14463  isunitd  14497  opprunitd  14501  invrfvald  14513  rdivmuldivd  14535  rhmmul  14555  isrhm2d  14556  rhm1  14558  rhmdvdsr  14566  rhmopp  14567  rhmunitinv  14569  islmod  14711  islmodd  14713  scaffvalg  14727  lmodpropd  14770  lsssetm  14777  islssmd  14780  lssats2  14835  lspsnneg  14841  lspsnsub  14842  lspun0  14846  lmodindp1  14849  sralemg  14859  srascag  14863  sravscag  14864  sraipg  14865  rlmscabas  14881  ixpsnbasval  14887  2idlval  14923  2idlvalg  14924  mulgrhm2  15029  zlmlemg  15047  zlmsca  15051  zlmvscag  15052  znval  15055  znle  15056  znbaslemnn  15058  znidomb  15077  isassad  15095  assapropd  15098  asclfval  15105  ressascl  15123  assamulgscmlem2  15126  psrval  15134  psrbasg  15150  psrplusgg  15154  mplvalcoe  15172  mplsubgfileminv  15182  mpl0fi  15184  mplnegfi  15187  istps  15224  tpspropd  15228  eltpsg  15232  txvalex  15446  txval  15447  txbasval  15459  upxp  15464  uptx  15466  txrest  15468  cnmpt11  15475  cnmpt21  15483  hmeontr  15505  txhmeo  15511  psmetxrge0  15524  xmetunirn  15550  mopnval  15634  mopntopon  15635  isxms  15643  isxms2  15644  isms  15645  msrtri  15668  xmspropd  15669  mspropd  15670  setsmsbasg  15671  setsmsdsg  15672  setsmstsetg  15673  comet  15691  metcnpi  15707  metcnpi2  15708  cnbl0  15726  cnblcld  15727  resubmet  15748  mpomulcn  15758  elcncf  15765  cncfi  15770  rescncf  15773  mulc1cncf  15781  cncfco  15783  cncfmptid  15789  addccncf  15792  cdivcncfap  15796  negcncf  15797  mulcncflem  15799  ivthinclemlopn  15828  ivthinclemuopn  15830  limccl  15851  ellimc3apf  15852  limcimolemlt  15856  cnplimclemle  15860  limccnpcntop  15867  reldvg  15871  dvfvalap  15873  dveflem  15918  dvef  15919  plymullem1  15940  plycjlemc  15952  plycj  15953  plyrecj  15955  plyreres  15956  sin0pilem1  15974  ef2kpi  15999  sinperlem  16001  sin2kpi  16004  cos2kpi  16005  sin2pim  16006  cos2pim  16007  ptolemy  16017  sincosq2sgn  16020  sincosq3sgn  16021  sincosq4sgn  16022  sinq12gt0  16023  tangtx  16031  sincosq1eq  16032  abssinper  16039  sinkpi  16040  coskpi  16041  cosq34lt1  16043  relogeftb  16058  relogoprlem  16062  relogexp  16066  logfac  16090  rpcxpef  16091  logcxp  16094  1cxp  16097  ecxp  16098  rpcxpadd  16102  rpmulcxp  16106  cxpmul  16109  abscxp  16112  logsqrt  16120  rpabscxpbnd  16137  rpcxplogb  16161  zprmlogbaplem3  16178  birthdaylem2  16187  birthdaylem3  16188  pellexlem1  16190  pellexlem2  16191  pellexlem3  16192  efchtqcl  16207  ppiqval  16209  ppival2  16210  ppival2g  16211  ppiprm  16220  ppinprm  16221  ppiqfl  16227  ppiqp1le  16228  ppidif  16230  ppiqltx  16242  prmorcht  16243  chtublem  16256  chtqub  16257  bcctr  16263  bcmono  16265  bposlem2  16273  bposlem6  16277  bposlem7  16278  bposlem8  16279  bposlem9  16280  lgsval  16289  lgsval2lem  16295  lgsval4a  16307  lgsdi  16322  lgseisenlem3  16357  lgseisenlem4  16358  lgsquadlem1  16362  lgsquadlem2  16363  lgsquadlem3  16364  2lgslem1  16376  2lgslem3a  16378  2lgslem3b  16379  2lgslem3c  16380  2lgslem3d  16381  vtxdgfval  16695  vtxdgfifival  16698  vtxdgop  16699  vtxdgfi0e  16702  vtxdeqd  16703  vtxdfifiun  16704  vtxdumgrfival  16705  1hevtxdg1en  16715  iswlk  16730  2wlklem  16783  wlkres  16786  clwwlkccatlem  16807  clwwlkn2  16828  clwwlkext2edg  16829  umgr2cwwk2dif  16831  clwwlknonex2lem2  16845  eupth2fi  16886  eulerpathprum  16887  depindlem1  16913  depind  16916  nnsf  17214  peano4nninf  17215  peano3nninf  17216  nninfalllem1  17217  nninfall  17218  nninfsellemdc  17219  nninfsellemeq  17223  nninfsellemqall  17224  nninfsellemeqinf  17225  nninfsel  17226  nnnninfex  17231  exmidsbthr  17234  qdencn  17238  refeq  17239  repiecele0  17241  repiecege0  17242  repiecef  17243  isomninnlem  17245  apdifflemr  17263  apdiff  17264  qdiff  17265  ismkvnnlem  17269  nconstwlpolem  17282