Theorem fveq2d 5652

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

Syntax hints:   -> wi 4   = wceq 1398   ` cfv 5333

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 717  ax-5 1496  ax-7 1497  ax-gen 1498  ax-ie1 1542  ax-ie2 1543  ax-8 1553  ax-10 1554  ax-11 1555  ax-i12 1556  ax-bndl 1558  ax-4 1559  ax-17 1575  ax-i9 1579  ax-ial 1583  ax-i5r 1584  ax-ext 2213

This theorem depends on definitions:  df-bi 117  df-3an 1007  df-tru 1401  df-nf 1510  df-sb 1811  df-clab 2218  df-cleq 2224  df-clel 2227  df-nfc 2364  df-rex 2517  df-v 2805  df-un 3205  df-sn 3679  df-pr 3680  df-op 3682  df-uni 3899  df-br 4094  df-iota 5293  df-fv 5341

This theorem is referenced by:  2fveq3  5653  fveq12d  5655  fveqeq2d  5656  csbfvg  5690  fvmptdf  5743  fvmptt  5747  resfvresima  5901  fcof1  5934  oveq1  6035  oveq2  6036  fvoveq1d  6050  caofinvl  6270  op1stg  6322  op2ndg  6323  ot1stg  6324  ot2ndg  6325  eloprabi  6370  1stconst  6395  algrflemg  6404  tfrlem1  6517  tfrlem3ag  6518  tfrlem3a  6519  tfrlem9  6528  tfr0dm  6531  tfrlemisucaccv  6534  tfrlemiubacc  6539  tfrlemiex  6540  tfrlemi1  6541  tfr1onlem3ag  6546  tfr1onlemsucaccv  6550  tfr1onlemubacc  6555  tfr1onlemex  6556  tfr1onlemaccex  6557  tfrcllemsucaccv  6563  tfrcllembxssdm  6565  tfrcllemubacc  6568  tfrcllemex  6569  tfrcllemaccex  6570  tfrcllemres  6571  tfrcldm  6572  rdgivallem  6590  rdgival  6591  rdgss  6592  rdgisuc1  6593  rdgon  6595  rdg0  6596  frec0g  6606  frecabcl  6608  freccllem  6611  frecfcllem  6613  frecsuclem  6615  frecsuc  6616  frecrdg  6617  oav2  6674  omv2  6676  xpdom2  7058  xpmapenlem  7078  xpmapen  7079  ac6sfi  7130  1stinl  7333  2ndinl  7334  1stinr  7335  2ndinr  7336  updjudhcoinlf  7339  updjudhcoinrg  7340  caseinl  7350  caseinr  7351  omp1eomlem  7353  omp1eom  7354  difinfsn  7359  ctmlemr  7367  ctm  7368  ctssdclemn0  7369  ctssdccl  7370  nninfninc  7382  nnnninfeq  7387  nnnninfeq2  7388  enomnilem  7397  enmkvlem  7420  enwomnilem  7428  exmidfodomrlemeldju  7470  exmidfodomrlemreseldju  7471  exmidfodomrlemr  7473  exmidfodomrlemrALT  7474  exmidaclem  7483  cc2  7546  cc3  7547  ltdfpr  7786  genpelvl  7792  genpelvu  7793  recexpr  7918  cauappcvgprlem1  7939  caucvgprlemnkj  7946  caucvgprlemnbj  7947  caucvgprlemm  7948  caucvgprlemdisj  7954  caucvgprlemloc  7955  caucvgprlemcl  7956  caucvgprlemladdfu  7957  caucvgprlemladdrl  7958  caucvgprlem1  7959  caucvgprlem2  7960  caucvgpr  7962  caucvgprprlemell  7965  caucvgprprlemelu  7966  caucvgprprlemcbv  7967  caucvgprprlemval  7968  caucvgprprlemnkeqj  7970  caucvgprprlemmu  7975  caucvgprprlemopl  7977  caucvgprprlemlol  7978  caucvgprprlemopu  7979  caucvgprprlemloc  7983  caucvgprprlemclphr  7985  caucvgprprlemexbt  7986  caucvgprprlem1  7989  caucvgprprlem2  7990  caucvgsr  8082  axcaucvglemval  8177  axcaucvglemres  8179  fv0p1e1  9317  uzin  9850  cnref1o  9946  fzsuc2  10376  fseq1m1p1  10392  fzoss2  10471  elfzonlteqm1  10518  divfl0  10619  flqzadd  10621  fldiv4p1lem1div2  10628  ceilqval  10631  flqdiv  10646  modqval  10649  modqfrac  10662  modqmulnn  10667  modqid  10674  modqcyc  10684  modqdi  10717  frec2uzuzd  10727  frec2uzrdg  10734  frecuzrdgrcl  10735  frecuzrdgtcl  10737  frecuzrdgsuc  10739  frecuzrdgrclt  10740  frecuzrdgg  10741  frecuzrdgfunlem  10744  frecuzrdgsuctlem  10748  iseqovex  10783  iseqvalcbv  10784  seq3val  10785  seqvalcd  10786  seq3m1  10798  seq3shft2  10806  seqshft2g  10807  monoord  10810  monoord2  10811  iseqf1olemqval  10825  iseqf1olemab  10827  iseqf1olemqk  10832  iseqf1olemjpcl  10833  iseqf1olemqpcl  10834  iseqf1olemfvp  10835  seq3f1olemqsumkj  10836  seq3f1olemqsumk  10837  seq3f1olemqsum  10838  seq3f1olemp  10840  seq3f1oleml  10841  seqf1oglem1  10844  seqf1oglem2  10845  seqf1og  10846  seq3homo  10852  seqhomog  10855  exp3val  10866  expnegap0  10872  facnn2  11059  facwordi  11065  faclbnd6  11069  bcval  11074  bccmpl  11079  bcn0  11080  bcm1k  11085  bcp1n  11086  bcn2  11089  hashinfom  11103  hashennn  11105  hashsng  11123  omgadd  11128  hashprg  11135  fihashssdif  11145  hashdifpr  11147  hashfzo  11149  hashfzp1  11151  hashxp  11153  zfz1isolemiso  11166  zfz1iso  11168  hashtpglem  11173  lsw1  11229  ccatfvalfi  11235  ccatlen  11238  ccatval3  11242  ccatval21sw  11248  ccatlid  11249  ccatass  11251  lswccatn0lsw  11254  lswccat0lsw  11255  ccatalpha  11256  s1leng  11267  ccats1val2  11283  lswccats1  11286  swrdfv0  11301  swrdfv2  11310  swrdsbslen  11313  swrds1  11315  ccatswrd  11317  pfxmpt  11327  pfxfv  11331  pfxtrcfvl  11344  ccatpfx  11348  swrdswrd  11352  lenpfxcctswrd  11358  ccatopth  11363  cats1un  11368  swrdccatin2  11376  pfxccatin12lem2  11378  shftval2  11466  shftval3  11467  shftval4  11468  shftval5  11469  seq3shft  11478  imval  11490  imre  11491  reim  11492  crim  11498  reim0  11501  mulreap  11504  recj  11507  reneg  11508  readd  11509  resub  11510  remullem  11511  redivap  11514  imcj  11515  imneg  11516  imadd  11517  imsub  11518  imdivap  11521  cjsub  11532  cjexp  11533  cjreim2  11544  cjap  11546  cjdivap  11549  cnrecnv  11550  cvg1nlemcau  11624  cvg1nlemres  11625  absval  11641  rennim  11642  sqrtdiv  11682  sqrtmsq  11685  absneg  11690  abscj  11692  absval2  11697  absreim  11708  absmul  11709  absdivap  11710  absid  11711  absre  11717  absexp  11719  absexpzap  11720  absimle  11724  abssub  11741  abs3dif  11745  abs2dif  11746  abs2dif2  11747  recan  11749  cau3lem  11754  max0addsup  11859  minabs  11876  bdtrilem  11879  clim  11921  clim2  11923  clim0  11925  clim0c  11926  climi0  11929  climconst  11930  climshftlemg  11942  climcn1  11948  climcn2  11949  addcn2  11950  subcn2  11951  mulcn2  11952  reccn2ap  11953  cjcn2  11956  recn2  11957  imcn2  11958  iser3shft  11986  climcau  11987  climcvg1nlem  11989  climcvg1n  11990  serf0  11992  fzf1o  12016  summodclem3  12021  summodclem2a  12022  summodc  12024  fsumf1o  12031  sumsnf  12050  fsumm1  12057  fsumcnv  12078  fsumabs  12106  fsumrelem  12112  iserabs  12116  hash2iun1dif1  12121  isumshft  12131  isumsplit  12132  expcnvap0  12143  expcnv  12145  cvgratnnlemseq  12167  cvgratnnlemrate  12171  cvgratz  12173  mertenslemub  12175  mertenslemi1  12176  mertenslem2  12177  mertensabs  12178  prodmodclem3  12216  fprodf1o  12229  prodsnf  12233  fprodm1  12239  fprodabs  12257  fprodcnv  12266  efcllemp  12299  efcj  12314  efaddlem  12315  efcan  12317  efsub  12322  efexp  12323  efzval  12324  efgt0  12325  eftlub  12331  efltim  12339  sinval  12343  cosval  12344  tanval3ap  12355  resinval  12356  recosval  12357  resin4p  12359  recos4p  12360  sinneg  12367  cosneg  12368  efmival  12374  efeul  12375  sinadd  12377  cosadd  12378  sinsub  12381  cossub  12382  addsin  12383  subsin  12384  addcos  12387  subcos  12388  sincossq  12389  sin2t  12390  cos2t  12391  sin01bnd  12398  cos01bnd  12399  sin02gt0  12405  cos12dec  12409  absefi  12410  absef  12411  absefib  12412  efieq1re  12413  demoivre  12414  demoivreALT  12415  flodddiv4  12577  bitsval  12584  bits0  12589  bitsp1  12592  bitsp1e  12593  bitsp1o  12594  bitsmod  12597  nninfctlemfo  12691  alginv  12699  algcvg  12700  eucalgval  12706  eucalginv  12708  eucalglt  12709  eucalgcvga  12710  eucalg  12711  lcmgcd  12730  lcm1  12733  sqpweven  12827  2sqpwodd  12828  sqne2sq  12829  qnumval  12837  qdenval  12838  qden1elz  12857  nn0sqrtelqelz  12858  phival  12865  dfphi2  12872  phiprmpw  12874  phiprm  12875  eulerthlemth  12884  hashgcdeq  12892  phisum  12893  pythagtriplem6  12923  pythagtriplem7  12924  pythagtriplem12  12928  pythagtriplem14  12930  fldivp1  13001  4sqlem11  13054  ennnfonelemg  13104  ennnfonelemp1  13107  ennnfonelemkh  13113  ennnfonelemhf1o  13114  ennnfonelemnn0  13123  ctinfomlemom  13128  ctiunctlemu1st  13135  ctiunctlemu2nd  13136  ctiunctlemudc  13138  ctiunctlemfo  13140  isstruct2im  13172  isstruct2r  13173  setsslid  13213  ressbasd  13230  resseqnbasd  13236  ressplusgd  13292  ptex  13427  prdsex  13432  prdsval  13436  prdsbas3  13450  pwsval  13454  pwsbas  13455  pwsplusgval  13458  pwsmulrval  13459  imasex  13468  imasival  13469  f1ocpbl  13474  f1ovscpbl  13475  imasaddvallemg  13478  qusval  13486  fvprif  13506  xpsff1o  13512  igsumvalx  13552  gsumprval  13562  pws0g  13614  imasmnd  13616  ismhm  13624  mhmpropd  13629  mhmlin  13630  mhmf1o  13633  resmhm  13650  mhmco  13653  gsumwmhm  13661  grpinvsub  13745  pwsinvg  13775  imasgrp2  13777  imasgrp  13778  mhmlem  13781  mhmid  13782  mhmmnd  13783  ghmgrp  13785  mulgfvalg  13788  mulgval  13789  mulgnegnn  13799  mulgneg  13807  mulgnegneg  13808  mulgm1  13809  mulginvcom  13814  mulgz  13817  mulgnndir  13818  mulgdir  13821  mulgass  13826  mhmmulg  13830  subgmulg  13855  isnsg  13869  eqgfval  13889  ghmlin  13915  ghmid  13916  ghminv  13917  ghmsub  13918  ghmmulg  13923  resghm  13927  ghmeql  13934  ablsub2inv  13978  ghmcmn  13994  invghm  13996  imasabl  14003  gsumfzreidx  14004  gsumfzmhm  14010  gsumsplit0  14013  mgpplusgg  14018  mgpbasg  14020  mgpscag  14021  mgptsetg  14022  mgpdsg  14024  rngm2neg  14043  imasrng  14050  isring  14094  ringm2neg  14149  imasring  14158  opprmulfvalg  14164  opprsllem  14168  isunitd  14201  opprunitd  14205  invrfvald  14217  rdivmuldivd  14239  rhmmul  14259  isrhm2d  14260  rhm1  14262  rhmdvdsr  14270  rhmopp  14271  rhmunitinv  14273  islmod  14387  islmodd  14389  scaffvalg  14402  lmodpropd  14445  lsssetm  14452  islssmd  14455  lssats2  14510  lspsnneg  14516  lspsnsub  14517  lspun0  14521  lmodindp1  14524  sralemg  14534  srascag  14538  sravscag  14539  sraipg  14540  rlmscabas  14556  ixpsnbasval  14562  2idlval  14598  2idlvalg  14599  mulgrhm2  14706  zlmlemg  14724  zlmsca  14728  zlmvscag  14729  znval  14732  znle  14733  znbaslemnn  14735  znidomb  14754  psrval  14762  psrbasg  14775  psrplusgg  14779  mplvalcoe  14791  mplsubgfileminv  14801  mpl0fi  14803  mplnegfi  14806  istps  14843  tpspropd  14847  eltpsg  14851  txvalex  15065  txval  15066  txbasval  15078  upxp  15083  uptx  15085  txrest  15087  cnmpt11  15094  cnmpt21  15102  hmeontr  15124  txhmeo  15130  psmetxrge0  15143  xmetunirn  15169  mopnval  15253  mopntopon  15254  isxms  15262  isxms2  15263  isms  15264  msrtri  15287  xmspropd  15288  mspropd  15289  setsmsbasg  15290  setsmsdsg  15291  setsmstsetg  15292  comet  15310  metcnpi  15326  metcnpi2  15327  cnbl0  15345  cnblcld  15346  resubmet  15367  mpomulcn  15377  elcncf  15384  cncfi  15389  rescncf  15392  mulc1cncf  15400  cncfco  15402  cncfmptid  15408  addccncf  15411  cdivcncfap  15415  negcncf  15416  mulcncflem  15418  ivthinclemlopn  15447  ivthinclemuopn  15449  limccl  15470  ellimc3apf  15471  limcimolemlt  15475  cnplimclemle  15479  limccnpcntop  15486  reldvg  15490  dvfvalap  15492  dveflem  15537  dvef  15538  plymullem1  15559  plycjlemc  15571  plycj  15572  plyrecj  15574  plyreres  15575  sin0pilem1  15592  ef2kpi  15617  sinperlem  15619  sin2kpi  15622  cos2kpi  15623  sin2pim  15624  cos2pim  15625  ptolemy  15635  sincosq2sgn  15638  sincosq3sgn  15639  sincosq4sgn  15640  sinq12gt0  15641  tangtx  15649  sincosq1eq  15650  abssinper  15657  sinkpi  15658  coskpi  15659  cosq34lt1  15661  relogeftb  15676  relogoprlem  15679  relogexp  15683  rpcxpef  15705  logcxp  15708  1cxp  15711  ecxp  15712  rpcxpadd  15716  rpmulcxp  15720  cxpmul  15723  abscxp  15726  logsqrt  15734  rpabscxpbnd  15751  rpcxplogb  15775  pellexlem1  15791  pellexlem2  15792  pellexlem3  15793  lgsval  15823  lgsval2lem  15829  lgsval4a  15841  lgsdi  15856  lgseisenlem3  15891  lgseisenlem4  15892  lgsquadlem1  15896  lgsquadlem2  15897  lgsquadlem3  15898  2lgslem1  15910  2lgslem3a  15912  2lgslem3b  15913  2lgslem3c  15914  2lgslem3d  15915  vtxdgfval  16229  vtxdgfifival  16232  vtxdgop  16233  vtxdgfi0e  16236  vtxdeqd  16237  vtxdfifiun  16238  vtxdumgrfival  16239  1hevtxdg1en  16249  iswlk  16264  2wlklem  16317  wlkres  16320  clwwlkccatlem  16341  clwwlkn2  16362  clwwlkext2edg  16363  umgr2cwwk2dif  16365  clwwlknonex2lem2  16379  eupth2fi  16420  eulerpathprum  16421  depindlem1  16447  depind  16450  nnsf  16731  peano4nninf  16732  peano3nninf  16733  nninfalllem1  16734  nninfall  16735  nninfsellemdc  16736  nninfsellemeq  16740  nninfsellemqall  16741  nninfsellemeqinf  16742  nninfsel  16743  nnnninfex  16748  exmidsbthr  16751  qdencn  16755  refeq  16756  repiecele0  16758  repiecege0  16759  repiecef  16760  isomninnlem  16762  apdifflemr  16779  apdiff  16780  qdiff  16781  ismkvnnlem  16785  nconstwlpolem  16798  gfsumval  16809  gsumgfsumlem  16812  gfsump1  16815