Theorem fveq2d 3713

Description: Equality deduction for function value.

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

Syntax hints:   -> wi 3   = wceq 953  ` cfv 3172

This theorem is referenced by:  hbfvd 3715  hbfvd2 3716  csbfv12g 3727  csbfvg 3729  fopabco 3817  fopabcos 3818  tfrlem1 3896  tfrlem3 3898  tfrlem5 3900  tfrlem9 3904  tfrlem11 3906  tfrlem12 3907  tfr2 3910  tz7.44-1 3913  tz7.44-2 3914  tz7.44-3 3915  rdglem1 3922  rdglem2 3923  rdgsuct 3930  frsuct 3938  opreq1 3953  opreq2 3954  oprprc2 3970  op1stg 4071  op2ndg 4072  curry1 4082  oasuc 4147  omsuc 4149  oesuc 4150  omsmolem 4240  xpdom2 4422  inf3lem1 4585  rankid 4644  rankr1 4646  ranklim 4657  rankr1id 4669  rankuni 4670  rankxpl 4682  rankxplim2 4685  rankxplim3 4686  rankxpsuc 4687  aceq3lem 4704  ac6lem 4726  unidom 4780  cardidm 4821  cardiun 4831  alephcard 4839  alephfp 4872  monoord 6231  om2uzsuc 6233  uzrdgsuc 6241  uzrdginip1 6242  seq1lem1 6246  seq1rval 6248  seq1val 6249  seq1val2 6251  seq1suclem 6253  seq1m1 6256  shftfval 6279  shftvalt 6283  shftval2t 6284  shftval3t 6285  shftval4t 6286  shftval5t 6287  2shft 6289  shftcan2t 6290  seq1seq02t 6475  seqz1 6479  seqzp1 6480  seqzm1 6481  seq0p1 6483  seqzval2t 6485  sqrmul 6635  sqrsqt 6652  absvalt 6694  imret 6710  reret 6734  renegt 6739  readdt 6740  resubt 6741  imnegt 6742  imaddt 6743  imsubt 6744  cjcjt 6746  cjaddt 6747  cjmult 6748  cjnegt 6749  cjsubt 6751  cjexpt 6752  absnegt 6767  abscjt 6769  absval2t 6787  absreimt 6792  absmult 6793  absdivz 6794  absdivt 6795  absret 6801  absexpt 6803  cjdiv 6826  cjdivt 6827  abssubt 6832  abstrit 6835  abs3dift 6836  abs2dift 6839  recant 6842  abs3lemt 6844  abslem2 6846  seq1bnd 6847  seq1ublem 6848  cau2 6850  caubnd 6863  caure 6864  cauim 6865  ser1absdiflem 6866  ser1absdif 6867  facp1t 6873  facnn2t 6876  facwordit 6881  faclbnd4lem2 6886  faclbnd6 6891  bcvalt 6895  bccmplt 6900  bcn0t 6901  bcnp11t 6903  clim 6915  fsumabs 6981  fsumabs2mul 6982  serzrelem 6999  clm0 7021  clmnns 7022  clm0nns 7023  clm0i 7027  climfnn 7030  climconst 7031  2climnn 7039  2climnn0 7040  climshft 7041  climres 7042  climshft2 7043  iserzshft2 7044  climrecl 7047  climge0 7049  climaddlem3 7052  climmullem3 7058  climmullem5 7060  climmullem8 7063  climabslem 7084  climcj 7086  climre 7087  climim 7088  climubi 7089  climcau 7092  caucvglem2 7094  caucvg 7099  caucvg3 7103  caucvg3t 7104  serzf0 7105  ser1f0 7106  ser1clim0 7109  iserzabslem 7114  iserzabs 7115  cvgcmp3ce 7123  cvgcmp3cetlem1 7124  cvgcmp3cetlem2 7125  cvgratlem1ALT 7182  cvgratlem2ALT 7183  cvgratlem3ALT 7184  cvgratlem1 7185  cvgratlem2 7186  cvgratlem3 7187  cvgratlem4 7188  elcncf 7200  negfcncf 7204  rescncf 7207  recncf 7211  imcncf 7212  cjcncf 7213  mulc1cncf 7214  ivthlem6 7221  ivthlem7 7222  ivthlem8 7223  ivthlem6OLD 7230  ivthlem7OLD 7231  ivthlem8OLD 7232  efcltlem1 7246  efcj 7278  efcjt 7279  efaddlem24 7303  efaddlem27 7306  efaddt 7309  efcant 7310  efsubt 7313  efexpt 7314  efnn0valt 7315  ef1tllem 7323  absef01tllem 7328  absef01tlub 7329  abspef01tlub 7336  absefm1le 7352  efcnlem4 7362  sinvalt 7371  cosvalt 7372  resinvalt 7375  recosvalt 7376  resin4pt 7378  recos4pt 7379  sinnegt 7384  cosnegt 7385  efmivalt 7390  efeult 7391  sinaddt 7395  cosaddt 7396  sinsubt 7397  cossubt 7398  addsint 7399  subsint 7400  addcost 7401  subcost 7402  sincossqt 7403  sin2tt 7404  cos2tt 7405  sin02gt0 7420  absefit 7424  demoivre 7426  demoivreALT 7427  acdc3 7429  acdc 7437  ruclem18 7470  ruclem19 7471  ruclem20 7472  ruclem21 7473  ruclem25 7477  ruclem29 7481  ruclem32 7484  ntrval2 7628  lpval 7684  islp 7685  metcnp4lem1 7902  metcn4i 7906  xplmi 7907  xplm 7909  bopcnlem2 7916  bopcnlem3 7917  bcthlem15 7947  bcthlem16 7948  bcthlem17 7949  bcthlem18 7950  bcthlem20 7952  bcthlem33 7965  bcth 7966  grpinvdiv 8019  ghgrpilem1 8070  ghgrpilem3 8072  ghgrpilem4 8073  ghgrpi 8074  ghsubgi 8075  vafval 8160  smfval 8162  0vfval 8163  isnvlem 8167  isnvgOLD 8168  nvi 8173  vsfval 8194  nvnegneg 8211  nvs 8229  nvdif 8232  nvpi 8233  nvsub 8234  nvz0 8235  nvtri 8237  nvmtri 8238  nvmtri2 8239  nvabs 8240  nvge0 8241  imsdval2 8256  nvnd 8257  imsmetlem 8261  nvelbl2 8264  sqcn 8270  nmcn 8274  va1cnlem 8279  sm1cnilem 8281  ipfval 8286  ipval 8287  ipval2lem3 8289  ipval2 8291  ipval3 8293  ipval2lem6 8295  ipid 8297  ipnm 8298  ipcj 8301  ip0r 8304  ip0l 8305  ip1cnilem4 8310  ip1cnilem6 8312  sspival 8331  sspimsval 8333  lnoval 8347  lnolin 8349  lno0 8351  lnocoi 8352  lnosub 8353  lnomul 8354  nvcnpi4 8355  nmoval 8358  nmosetn0 8360  nmolb 8366  nmoubi 8367  nmobndseqi 8372  nmo0 8383  nmlno0lem 8385  nmlnoubi 8388  nmblolbii 8390  nmblolbi 8391  blometi 8394  blocnilem 8395  isphg 8407  cnph 8409  isph 8412  phpar2 8413  phpar 8414  ipdi 8434  ipassr 8437  ipsubdi 8440  siilem2 8443  siii 8444  sii 8445  sspph 8446  ipblnfi 8447  ubthlem1 8460  ubthlem3 8462  ubthlem9 8468  ubthlem10 8469  ubthlem11 8470  ubthlem12 8471  ubthi 8475  minveclem7 8482  minveclem8 8483  minveclem13 8488  minveclem18 8493  minveclem19 8494  minveclem20 8495  minveclem23 8498  minveclem28 8503  minveclem33 8508  minvecex 8509  minveclem35 8510  minveclem36 8511  minveceu 8514  minvecdist 8516  minveclem39 8518  htthlem6 8555  htthlem9 8558  sincolem 8584  sinperlem2 8606  sin2pim 8611  cos2pim 8612  sincosq2sgn 8622  sincosq3sgn 8623  sincosq4sgn 8624  sinq12gt0t 8625  sincosq1eq 8626  efgh 8633  efghgrpilem 8634  efif 8636  efifo 8644  efif1lem6 8650  efif1 8652  shftefif1olem 8661  shftefif1olemOLD 8662  eff1lem 8664  eff1i 8665  effoi 8666  effoiOLD 8667  efper 8669  logeft 8684  relogoprlem 8691  relogexpt 8696  logeftOLD 8705  logoprlemOLD 8709  logexptOLD 8712  his5t 8874  his7t 8877  his2sub2t 8880  hi02t 8884  abshicomt 8888  normvalt 8911  normgt0tOLD 8914  normgt0t 8915  norm0 8916  normsub0t 8924  norm-iit 8926  norm-iiit 8928  normsubt 8931  normnegt 8932  normpytht 8933  norm3dift 8938  norm3lemt 8940  norm3adift 8941  normpart 8943  polidt 8947  hhph 8966  bcsALT 8967  bcst 8969  hcau 8972  hcau2 8976  hlim 8977  hlim2 8981  hlim0 9026  hlimcaui 9027  hhssnv 9054  hhssmetdval 9066  occllem2 9090  occllem6 9094  projlem7 9108  projlem8 9109  projlem10 9111  projlem15 9116  projlem16 9117  projlem17 9118  projlem20 9121  projlem22 9123  projlem23 9124  projlem25 9126  projlem26 9127  projlem28 9129  pjthlem8 9141  pjthlem9 9142  pjthlem12 9145  pjth 9148  ococt 9163  axpjpjt 9171  pjoc1t 9182  sshjvalt 9235  sshjval3t 9241  chdmm1t 9363  chdmj1t 9367  spanunt 9383  h1de2ctlem 9394  spansnt 9398  elspansnt 9405  elspansn2t 9406  spansneleq 9409  spansneleqOLD 9410  h1datomt 9422  cmcmlem 9451  osumlem2 9496  spansnjt 9509  spansncvt 9515  pjaddt 9548  pjinormt 9549  pjsubt 9550  pjmult 9551  pjcjt2 9554  pjsumt 9572  pjds 9574  pjds3 9575  pjoi0t 9579  pjopytht 9582  pjnormt 9586  pjpytht 9587  pjnelt 9588  hoid1 9632  nmopvalt 9699  elcnopt 9700  nmopsetn0 9709  nmfnvalt 9720  nmfnsetn0 9722  elcnfnt 9726  hhlno 9743  nmoplbt 9748  nmopubt 9749  cnopct 9753  lnoplt 9754  nmfnlbt 9764  nmfnleubt 9765  cnfnct 9770  lnfnlt 9771  nmopneg 9805  lnopmult 9807  lnopadd 9811  lnopsub 9814  homco2t 9817  0cnop 9819  0cnfn 9820  idcnop 9821  nmop0 9826  nmfn0 9827  hoddi 9829  nmop0h 9831  nmlnop0ALT 9835  lnopco 9843  lnopco0 9844  lnopeq0lem2 9846  lnopunilem1 9850  lnopunilem2 9851  elunop2t 9853  nmbdoplb 9864  nmbdoplbt 9865  nmcopexlem2 9867  nmcopexlem3 9868  nmcopexlem6 9871  nmcoplb 9873  nmcoplbt 9875  nmophm 9876  lnopcon 9878  lnopcont 9879  lnfnadd 9887  lnfnmul 9888  lnfnsub 9890  nmbdfnlb 9893  nmbdfnlbt 9894  nmcfnexlem2 9896  nmcfnexlem3 9897  nmcfnexlem6 9900  nmcfnlb 9902  nmcfnlbt 9904  lnfncon 9905  lnfncont 9906  nlelch 9909  cnlnadjlem2 9916  cnlnadjlem7 9921  nmopadjle 9936  nmoptri 9941  nmopco 9942  nmopcoadj 9948  branmfnt 9951  cnvbramult 9960  kbass6t 9966  pjnmop 9986  pjbdln 9987  hmopidmchlem 9989  hmopidmch 9990  hmopidmpj 9991  hmopidmpjt 9993  pjsdi 9994  pjddi 9995  pjss2co 10003  pjdifnormt 10006  pjssum 10010  pjclem4 10037  pj3s 10045  pjs14 10048  hstelt 10052  hstel2t 10056  hstoct 10059  hstnmoct 10060  hstpytht 10066  stjt 10072  strlem2 10088  strlem3a 10089  strlem4 10091  hstrlem3a 10097  hstrlem4 10099  hstrlem5 10100  hstr 10102  stcltrlem1 10113  superpos 10189  sumdmdlem2 10253  cdj1 10265  cdj3lem1 10266  cdj3lem2b 10269  cdj3lem3 10270  cdj3lem3b 10272  cdj3 10273  elghomlem1 10287  ghomgrpilem1 10290  ghomgrpilem2 10291  ghomlin 10298  ghomid 10299  ghomf1olem 10301  cayleylem2 10317  cayleythlem 10320  domval 10499  codval 10500  idval 10501  cmpval 10502  isded 10513  dedi 10514  1ded 10515  idosd 10521  domcmpd 10523  codcmpd 10524  1cat 10536  homib 10568  imonclem 10583  isfuna 10592  isfunb 10593

This theorem was proved from axioms:  ax-1 4  ax-2 5  ax-3 6  ax-mp 7  ax-7 959  ax-gen 960  ax-8 961  ax-10 963  ax-11 964  ax-12 965  ax-13 966  ax-14 967  ax-17 968  ax-4 970  ax-5o 972  ax-6o 975  ax-9o 1119  ax-10o 1136  ax-16 1206  ax-11o 1213  ax-ext 1452  ax-sep 2693  ax-pow 2732  ax-pr 2769

This theorem depends on definitions:  df-bi 147  df-or 224  df-an 225  df-ex 978  df-sb 1168  df-eu 1375  df-mo 1376  df-clab 1457  df-cleq 1462  df-clel 1465  df-ne 1579  df-v 1803  df-dif 2039  df-un 2040  df-in 2041  df-ss 2043  df-nul 2271  df-pw 2392  df-sn 2402  df-pr 2403  df-op 2406  df-uni 2494  df-br 2610  df-opab 2657  df-xp 3174  df-cnv 3176  df-dm 3178  df-rn 3179  df-res 3180  df-ima 3181  df-fv 3188

Copyright terms: Public domain