Theorem fveq2d 3719

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

Syntax hints:   -> wi 3   = wceq 954  ` cfv 3177

This theorem is referenced by:  hbfvd 3721  hbfvd2 3722  csbfv12g 3733  csbfvg 3735  fopabco 3823  fopabcos 3824  tfrlem1 3902  tfrlem3 3904  tfrlem5 3906  tfrlem9 3910  tfrlem11 3912  tfrlem12 3913  tfr2 3916  tz7.44-1 3919  tz7.44-2 3920  tz7.44-3 3921  rdglem1 3928  rdglem2 3929  rdgsuct 3936  frsuct 3944  opreq1 3959  opreq2 3960  oprprc2 3976  op1stg 4077  op2ndg 4078  curry1 4088  oasuc 4153  omsuc 4155  oesuc 4156  omsmolem 4246  xpdom2 4428  inf3lem1 4593  rankid 4652  rankr1 4654  ranklim 4665  rankr1id 4677  rankuni 4678  rankxpl 4690  rankxplim2 4693  rankxplim3 4694  rankxpsuc 4695  aceq3lem 4712  ac6lem 4734  unidom 4788  cardidm 4829  cardiun 4839  alephcard 4847  alephfp 4880  monoord 6239  om2uzsuc 6241  uzrdgsuc 6249  uzrdginip1 6250  seq1lem1 6254  seq1rval 6256  seq1val 6257  seq1val2 6259  seq1suclem 6261  seq1m1 6264  shftfval 6287  shftvalt 6291  shftval2t 6292  shftval3t 6293  shftval4t 6294  shftval5t 6295  2shft 6297  shftcan2t 6298  seq1seq02t 6483  seqz1 6487  seqzp1 6488  seqzm1 6489  seq0p1 6491  seqzval2t 6493  sqrmul 6643  sqrsqt 6660  absvalt 6702  imret 6718  reret 6742  renegt 6747  readdt 6748  resubt 6749  imnegt 6750  imaddt 6751  imsubt 6752  cjcjt 6754  cjaddt 6755  cjmult 6756  cjnegt 6757  cjsubt 6759  cjexpt 6760  absnegt 6775  abscjt 6777  absval2t 6795  absreimt 6800  absmult 6801  absdivz 6802  absdivt 6803  absret 6809  absexpt 6811  cjdiv 6834  cjdivt 6835  abssubt 6840  abstrit 6843  abs3dift 6844  abs2dift 6847  recant 6850  abs3lemt 6852  abslem2 6854  seq1bnd 6855  seq1ublem 6856  cau2 6858  caubnd 6871  caure 6872  cauim 6873  ser1absdiflem 6874  ser1absdif 6875  facp1t 6881  facnn2t 6884  facwordit 6889  faclbnd4lem2 6894  faclbnd6 6899  bcvalt 6903  bccmplt 6908  bcn0t 6909  bcnp11t 6911  clim 6923  fsumabs 6989  fsumabs2mul 6990  serzrelem 7007  clm0 7029  clmnns 7030  clm0nns 7031  clm0i 7035  climfnn 7038  climconst 7039  2climnn 7047  2climnn0 7048  climshft 7049  climres 7050  climshft2 7051  iserzshft2 7052  climrecl 7055  climge0 7057  climaddlem3 7060  climmullem3 7066  climmullem5 7068  climmullem8 7071  climabslem 7092  climcj 7094  climre 7095  climim 7096  climubi 7097  climcau 7100  caucvglem2 7102  caucvg 7107  caucvg3 7111  caucvg3t 7112  serzf0 7113  ser1f0 7114  ser1clim0 7117  iserzabslem 7122  iserzabs 7123  cvgcmp3ce 7131  cvgcmp3cetlem1 7132  cvgcmp3cetlem2 7133  cvgratlem1ALT 7190  cvgratlem2ALT 7191  cvgratlem3ALT 7192  cvgratlem1 7193  cvgratlem2 7194  cvgratlem3 7195  cvgratlem4 7196  elcncf 7208  negfcncf 7212  rescncf 7215  recncf 7219  imcncf 7220  cjcncf 7221  mulc1cncf 7222  ivthlem6 7229  ivthlem7 7230  ivthlem8 7231  ivthlem6OLD 7238  ivthlem7OLD 7239  ivthlem8OLD 7240  efcltlem1 7254  efcj 7286  efcjt 7287  efaddlem24 7311  efaddlem27 7314  efaddt 7317  efcant 7318  efsubt 7321  efexpt 7322  efnn0valt 7323  ef1tllem 7331  absef01tllem 7336  absef01tlub 7337  abspef01tlub 7344  absefm1le 7360  efcnlem4 7370  sinvalt 7379  cosvalt 7380  resinvalt 7383  recosvalt 7384  resin4pt 7386  recos4pt 7387  sinnegt 7392  cosnegt 7393  efmivalt 7398  efeult 7399  sinaddt 7403  cosaddt 7404  sinsubt 7405  cossubt 7406  addsint 7407  subsint 7408  addcost 7409  subcost 7410  sincossqt 7411  sin2tt 7412  cos2tt 7413  sin02gt0 7428  absefit 7432  demoivre 7434  demoivreALT 7435  acdc3 7437  acdc 7445  ruclem18 7478  ruclem19 7479  ruclem20 7480  ruclem21 7481  ruclem25 7485  ruclem29 7489  ruclem32 7492  ntrval2 7636  lpval 7693  islp 7694  metcnp4lem1 7918  metcn4i 7922  xplmi 7923  xplm 7925  bopcnlem2 7932  bopcnlem3 7933  bcthlem15 7963  bcthlem16 7964  bcthlem17 7965  bcthlem18 7966  bcthlem20 7968  bcthlem33 7981  bcth 7982  grpinvdiv 8034  ghgrpilem1 8085  ghgrpilem3 8087  ghgrpilem4 8088  ghgrpi 8089  ghsubgi 8090  vafval 8174  smfval 8176  0vfval 8177  isnvlem 8181  nvi 8185  vsfval 8206  nvnegneg 8223  nvs 8242  nvdif 8245  nvpi 8246  nvsub 8247  nvz0 8248  nvtri 8250  nvmtri 8251  nvmtri2 8252  nvabs 8253  nvge0 8254  imsdval2 8269  nvnd 8270  imsmetlem 8274  nvelbl2 8277  sqcn 8283  nmcn 8287  va1cnlem 8292  sm1cnilem 8294  ipfval 8299  ipval 8300  ipval2lem3 8302  ipval2 8304  ipval3 8306  ipval2lem6 8308  ipid 8310  ipnm 8311  ipcj 8314  ip0r 8317  ip0l 8318  ip1cnilem4 8323  ip1cnilem6 8325  sspival 8344  sspimsval 8346  lnoval 8360  lnolin 8362  lno0 8364  lnocoi 8365  lnosub 8366  lnomul 8367  nvcnpi4 8368  nmoval 8371  nmosetn0 8373  nmolb 8379  nmoubi 8380  nmobndseqi 8385  nmo0 8396  nmlno0lem 8398  nmlnoubi 8401  nmblolbii 8403  nmblolbi 8404  blometi 8407  blocnilem 8408  isphg 8420  cnph 8422  isph 8425  phpar2 8426  phpar 8427  ipdi 8447  ipassr 8450  ipsubdi 8453  siilem2 8456  siii 8457  sii 8458  sspph 8459  ipblnfi 8460  ubthlem1 8473  ubthlem3 8475  ubthlem9 8481  ubthlem10 8482  ubthlem11 8483  ubthlem12 8484  ubthi 8488  minveclem7 8495  minveclem8 8496  minveclem13 8501  minveclem18 8506  minveclem19 8507  minveclem20 8508  minveclem23 8511  minveclem28 8516  minveclem33 8521  minvecex 8522  minveclem35 8523  minveclem36 8524  minveceu 8527  minvecdist 8529  minveclem39 8531  htthlem6 8568  htthlem9 8571  sincolem 8603  sinperlem2 8625  sin2pim 8630  cos2pim 8631  sincosq2sgn 8641  sincosq3sgn 8642  sincosq4sgn 8643  sinq12gt0t 8644  sincosq1eq 8645  efgh 8652  efghgrpilem 8653  efif 8655  efifo 8663  efif1lem6 8669  efif1 8671  shftefif1olem 8680  eff1lem 8682  eff1i 8683  effoi 8684  efper 8686  logeft 8701  relogoprlem 8708  relogexpt 8713  his5t 8892  his7t 8895  his2sub2t 8898  hi02t 8902  abshicomt 8906  normvalt 8929  normgt0tOLD 8932  normgt0t 8933  norm0 8934  normsub0t 8942  norm-iit 8944  norm-iiit 8946  normsubt 8949  normnegt 8950  normpytht 8951  norm3dift 8956  norm3lemt 8958  norm3adift 8959  normpart 8961  polidt 8965  hhph 8984  bcsALT 8985  bcst 8987  hcau 8990  hcau2 8994  hlim 8995  hlim2 8999  hlim0 9044  hlimcaui 9045  hhssnv 9073  hhssmetdval 9088  occllem2 9113  occllem6 9117  projlem7 9131  projlem8 9132  projlem10 9134  projlem15 9139  projlem16 9140  projlem17 9141  projlem20 9144  projlem22 9146  projlem23 9147  projlem25 9149  projlem26 9150  projlem28 9152  pjthlem8 9164  pjthlem9 9165  pjthlem12 9168  pjth 9171  ococt 9186  axpjpjt 9194  pjoc1t 9205  sshjvalt 9258  sshjval3t 9264  chdmm1t 9386  chdmj1t 9390  spanunt 9406  h1de2ctlem 9417  spansnt 9421  elspansnt 9428  elspansn2t 9429  spansneleq 9432  spansneleqOLD 9433  h1datomt 9445  cmcmlem 9474  osumlem2 9519  spansnjt 9532  spansncvt 9538  pjaddt 9571  pjinormt 9572  pjsubt 9573  pjmult 9574  pjcjt2 9577  pjsumt 9595  pjds 9597  pjds3 9598  pjoi0t 9602  pjopytht 9605  pjnormt 9609  pjpytht 9610  pjnelt 9611  hoid1 9655  nmopvalt 9722  elcnopt 9723  nmopsetn0 9732  nmfnvalt 9743  nmfnsetn0 9745  elcnfnt 9749  hhlno 9766  nmoplbt 9771  nmopubt 9772  cnopct 9776  lnoplt 9777  nmfnlbt 9787  nmfnleubt 9788  cnfnct 9793  lnfnlt 9794  nmopneg 9828  lnopmult 9830  lnopadd 9834  lnopsub 9837  homco2t 9840  0cnop 9842  0cnfn 9843  idcnop 9844  nmop0 9849  nmfn0 9850  hoddi 9852  nmop0h 9854  nmlnop0ALT 9858  lnopco 9866  lnopco0 9867  lnopeq0lem2 9869  lnopunilem1 9873  lnopunilem2 9874  elunop2t 9876  nmbdoplb 9887  nmbdoplbt 9888  nmcopexlem2 9890  nmcopexlem3 9891  nmcopexlem6 9894  nmcoplb 9896  nmcoplbt 9898  nmophm 9899  lnopcon 9901  lnopcont 9902  lnfnadd 9910  lnfnmul 9911  lnfnsub 9913  nmbdfnlb 9916  nmbdfnlbt 9917  nmcfnexlem2 9919  nmcfnexlem3 9920  nmcfnexlem6 9923  nmcfnlb 9925  nmcfnlbt 9927  lnfncon 9928  lnfncont 9929  nlelch 9932  cnlnadjlem2 9939  cnlnadjlem7 9944  nmopadjle 9959  nmoptri 9965  nmopco 9966  nmopcoadj 9972  branmfnt 9976  cnvbramult 9986  kbass6t 9992  pjnmop 10013  pjbdln 10014  hmopidmchlem 10016  hmopidmch 10017  hmopidmpj 10018  hmopidmpjt 10020  pjsdi 10021  pjddi 10022  pjss2co 10030  pjdifnormt 10033  pjssum 10037  pjclem4 10065  pj3s 10073  pjs14 10076  hstelt 10080  hstel2t 10084  hstoct 10087  hstnmoct 10088  hstpytht 10094  stjt 10100  strlem2 10116  strlem3a 10117  strlem4 10119  hstrlem3a 10125  hstrlem4 10127  hstrlem5 10128  hstr 10130  stcltrlem1 10141  superpos 10218  sumdmdlem2 10282  cdj1 10294  cdj3lem1 10295  cdj3lem2b 10298  cdj3lem3 10299  cdj3lem3b 10301  cdj3 10302  elghomlem1 10316  ghomgrpilem1 10319  ghomgrpilem2 10320  ghomlin 10327  ghomid 10328  ghomf1olem 10330  cayleylem2 10344  cayleythlem 10347  domval 10535  codval 10536  idval 10537  cmpval 10538  isded 10549  dedi 10550  1ded 10551  idosd 10557  domcmpd 10559  codcmpd 10560  1cat 10572  homib 10604  imonclem 10619  isfuna 10628  isfunb 10629

This theorem was proved from axioms:  ax-1 4  ax-2 5  ax-3 6  ax-mp 7  ax-7 960  ax-gen 961  ax-8 962  ax-10 964  ax-11 965  ax-12 966  ax-13 967  ax-14 968  ax-17 969  ax-4 971  ax-5o 973  ax-6o 976  ax-9o 1121  ax-10o 1138  ax-16 1208  ax-11o 1216  ax-ext 1457  ax-sep 2698  ax-pow 2737  ax-pr 2774

This theorem depends on definitions:  df-bi 147  df-or 224  df-an 225  df-ex 979  df-sb 1170  df-eu 1380  df-mo 1381  df-clab 1462  df-cleq 1467  df-clel 1470  df-ne 1584  df-v 1808  df-dif 2045  df-un 2046  df-in 2047  df-ss 2049  df-nul 2277  df-pw 2398  df-sn 2408  df-pr 2409  df-op 2412  df-uni 2499  df-br 2615  df-opab 2662  df-xp 3179  df-cnv 3181  df-dm 3183  df-rn 3184  df-res 3185  df-ima 3186  df-fv 3193

Copyright terms: Public domain