Theorem fveq2d 3804

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

Syntax hints:   -> wi 3   = wceq 988  ` cfv 3237

This theorem is referenced by:  hbfvd 3806  hbfvd2 3807  csbfv12g 3818  csbfvg 3820  fopabco 3908  fopabcos 3909  tfrlem1 3987  tfrlem3 3989  tfrlem5 3991  tfrlem9 3995  tfrlem11 3997  tfrlem12 3998  tfr2 4001  tz7.44-1 4004  tz7.44-2 4005  tz7.44-3 4006  rdglem1 4013  rdglem2 4014  rdgsuc 4021  frsuc 4029  opreq1 4044  opreq2 4045  oprprc2 4061  op1stg 4165  op2ndg 4166  curry1 4208  curry2 4211  oasuc 4247  omsuc 4249  oesuc 4250  omsmolem 4340  xpdom2 4529  inf3lem1 4699  rankid 4758  rankr1 4760  ranklim 4771  rankr1id 4783  rankuni 4784  rankxpl 4796  rankxplim2 4799  rankxplim3 4800  rankxpsuc 4801  aceq3lem 4818  ac6lem 4840  unidom 4894  cardidm 4938  cardiun 4948  alephcard 4956  alephfp 4989  fldiv 6396  fldiv2 6397  modval 6400  modfrac 6404  modid 6409  modcyc 6410  modcycOLD 6411  monoord 6415  om2uzsuci 6588  uzrdgsuci 6597  uzrdginip1i 6598  seq1lem1 6602  seq1rval 6604  seq1val 6605  seq1val2 6607  seq1suclem 6609  seq1m1 6612  shftfval 6635  shftval 6639  shftval2 6640  shftval3 6641  shftval4 6642  shftval5 6643  2shfti 6645  shftcan2 6646  seq1seq02 6666  seqz1 6670  seqzp1 6671  seqzm1 6672  seq0p1 6674  seqzval2 6676  sqrmuli 6828  sqrsq 6845  absval 6885  imre 6896  mulre 6900  reneg 6927  readd 6928  resub 6929  imneg 6930  imadd 6931  imsub 6932  cjcj 6934  cjadd 6935  cjmul 6936  cjneg 6937  cjsub 6939  cjexp 6940  absneg 6955  abscj 6957  absval2 6975  absreim 6980  absmul 6981  absdivzi 6982  absdiv 6983  absre 6989  absexp 6991  cjdivi 7011  cjdiv 7012  abssub 7017  abstri 7021  abs3dif 7022  abs2dif 7025  recan 7028  abs3lem 7030  abslem2 7032  seq1bndi 7033  seq1ublem 7034  cau2i 7036  caubndi 7049  caurei 7050  cauimi 7051  ser1absdiflem 7052  ser1absdifi 7053  facp1 7059  facnn2 7062  facwordi 7067  faclbnd4lem2 7072  faclbnd6 7077  bcval 7081  bccmpl 7085  bcn0 7086  bcnp11 7088  clim 7100  fsumabs 7166  fsumabs2mul 7167  serzrelem 7184  clm0i 7206  clmnnsi 7207  clm0nnsi 7208  clm0ii 7212  climfnn 7215  climconsti 7217  2climnn 7225  2climnn0 7226  climshfti 7227  climresi 7228  climshft2i 7229  iserzshft2i 7230  climrecl 7233  climge0 7235  climaddlem3 7239  climmullem3 7245  climmullem5 7247  climmullem8 7250  climabslem 7271  climcji 7273  climrei 7274  climimi 7275  climubii 7276  climcaui 7279  caucvglem2 7281  caucvgi 7286  caucvg3i 7290  caucvg3 7291  serzf0i 7292  ser1f0i 7293  ser1clim0 7296  iserzabslem 7301  iserzabsi 7302  cvgcmp3cei 7310  cvgcmp3cetlem1 7311  cvgcmp3cetlem2 7312  cvgratlem1ALT 7370  cvgratlem2ALT 7371  cvgratlem3ALT 7372  cvgratlem1 7373  cvgratlem2 7374  cvgratlem3 7375  cvgratlem4 7376  elcncf 7388  negfcncfi 7392  rescncf 7395  recncf 7399  imcncf 7400  cjcncf 7401  mulc1cncf 7402  ivthlem6 7409  ivthlem7 7410  ivthlem8 7411  efcltlem1 7427  efcji 7459  efcj 7460  efaddlem24 7484  efaddlem27 7487  efadd 7490  efcan 7491  efsub 7494  efexp 7495  efnn0val 7496  ef1tllem 7504  absef01tllem 7510  absef01tlubi 7511  abspef01tlubi 7519  absefm1lei 7536  efcnlem4 7546  sinval 7553  cosval 7554  resinval 7557  recosval 7558  resin4p 7560  recos4p 7561  sinneg 7566  cosneg 7567  efmival 7572  efeul 7573  sinadd 7577  cosadd 7578  sinsub 7579  cossub 7580  addsin 7581  subsin 7582  addcos 7583  subcos 7584  sincossq 7585  sin2t 7586  cos2t 7587  sin02gt0 7603  absefi 7607  demoivre 7609  demoivreALT 7610  acdc3 7612  acdc 7620  ruclem18 7652  ruclem19 7653  ruclem20 7654  ruclem21 7655  ruclem25 7659  ruclem29 7663  ruclem32 7666  ntrval2 7806  lpval 7863  islp 7864  metcnp4lem1 8088  metcn4i 8092  xplmi 8093  xplm 8095  bopcnlem2 8102  bopcnlem3 8103  bcthlem15 8133  bcthlem16 8134  bcthlem17 8135  bcthlem18 8136  bcthlem20 8138  bcthlem33 8151  bcth 8152  grpinvdiv 8203  ghgrpilem1 8252  ghgrpilem3 8254  ghgrpilem4 8255  ghgrpi 8256  ghsubgi 8257  vafval 8341  smfval 8343  0vfval 8344  isnvlem 8348  nvi 8352  vsfval 8373  nvnegneg 8390  nvs 8409  nvdif 8412  nvpi 8413  nvsub 8414  nvz0 8415  nvtri 8417  nvmtri 8418  nvmtri2 8419  nvabs 8420  nvge0 8421  imsdval2 8437  nvnd 8438  imsmetlem 8442  nvelbl2 8445  sqcn 8454  nmcn 8458  va1cnlem 8464  sm1cnilem 8466  ipfval 8471  ipval 8472  ipval2lem3 8474  ipval2 8476  ipval3 8478  ipval2lem6 8480  ipid 8482  ipnm 8483  ipcj 8486  ip0r 8489  ip0l 8490  ip1cnilem4 8495  ip1cnilem6 8497  sspival 8516  sspimsval 8518  lnoval 8532  lnolin 8534  lno0 8536  lnocoi 8537  lnoadd 8538  lnosub 8539  lnomul 8540  nvcnpi3 8541  nvcnpi4 8542  nmoval 8545  nmosetn0 8547  nmolb 8553  nmoubi 8554  nmobndseqi 8559  nmo0 8570  nmlno0lem 8572  nmlnoubi 8575  nmblolbii 8578  nmblolbi 8579  blometi 8582  blocnilem 8583  isphg 8595  cnph 8597  isph 8600  phpar2 8601  phpar 8602  ipdi 8622  ipassr 8625  ipsubdi 8628  siilem2 8631  siii 8632  sii 8633  sspph 8634  ipblnfi 8635  ubthlem1 8648  ubthlem3 8650  ubthlem9 8656  ubthlem10 8657  ubthlem11 8658  ubthlem12 8659  ubthi 8663  minveclem7 8670  minveclem8 8671  minveclem13 8676  minveclem18 8681  minveclem19 8682  minveclem20 8683  minveclem23 8686  minveclem28 8691  minveclem33 8696  minvecex 8697  minveclem35 8698  minveclem36 8699  minveceu 8702  minvecdist 8704  minveclem39 8706  htthlem6 8744  htthlem9 8747  sincolem 8783  sinperlem2 8805  sin2pim 8810  cos2pim 8811  sinkpi 8816  sincosq2sgn 8824  sincosq3sgn 8825  sincosq4sgn 8826  sinq12gt0t 8827  sincosq1eq 8828  abssinper 8831  sineq0 8832  efgh 8837  efghgrpilem 8838  efif 8840  efifo 8848  efif1lem6 8854  efif1 8856  shftefif1olem 8860  eff1lem 8862  eff1i 8863  effoi 8864  efper 8866  logef 8881  relogoprlem 8888  relogexp 8893  his5 9073  his7 9076  his2sub2 9079  hi02 9083  abshicom 9087  normval 9110  normgt0OLD 9113  normgt0 9114  norm0 9115  normsub0 9123  norm-ii 9125  norm-iii 9127  normsub 9130  normneg 9131  normpyth 9132  norm3dif 9137  norm3lemt 9139  norm3adifi 9140  normpar 9142  polid 9146  hhph 9165  bcsiALT 9166  bcs 9168  hcau 9171  hcau2 9175  hlimi 9176  hlim2 9180  hlim0 9225  hlimcauii 9226  hhssnv 9254  hhssmetdval 9269  occllem2 9294  occllem6 9298  projlem7 9312  projlem8 9313  projlem10 9315  projlem15 9320  projlem16 9321  projlem17 9322  projlem20 9325  projlem22 9327  projlem23 9328  projlem25 9330  projlem26 9331  projlem28 9333  pjthlem8 9346  pjthlem9 9347  pjthlem12 9350  pjthi 9353  ococ 9368  axpjpj 9376  pjoc1 9387  sshjval 9440  sshjval3 9446  chdmm1 9568  chdmj1 9572  spanun 9588  h1de2ctlem 9598  spansn 9602  elspansn 9609  elspansn2 9610  spansneleq 9613  h1datom 9625  cmcmlem 9654  osumlem2 9699  spansnj 9712  spansncv 9718  pjaddi 9751  pjinormi 9752  pjsubi 9753  pjmuli 9754  pjcjt2 9757  pjsumi 9775  pjdsi 9777  pjds3i 9778  pjoi0 9782  pjopyth 9785  pjnorm 9789  pjpyth 9790  pjnel 9791  hoid1i 9835  nmopval 9900  elcnop 9901  nmopsetn0 9910  nmfnval 9921  nmfnsetn0 9923  elcnfn 9927  hhlnoi 9944  nmoplb 9949  nmopub 9950  cnopc 9955  lnopl 9956  nmfnlb 9966  nmfnleub 9967  cnfnc 9972  lnfnl 9973  nmopnegi 10006  lnopmul 10008  lnopaddi 10012  lnopsubi 10015  homco2 10018  0cnop 10020  0cnfn 10021  idcnop 10022  nmop0 10027  nmfn0 10028  hoddii 10031  nmop0h 10033  nmlnop0iALT 10037  lnopcoi 10045  lnopco0i 10046  lnopeq0lem2 10048  lnopunilem1 10052  lnopunilem2 10053  elunop2 10055  nmbdoplbi 10066  nmbdoplb 10067  nmcopexlem2 10069  nmcopexlem3 10070  nmcopexlem6 10073  nmcoplbi 10075  nmcoplb 10077  nmophmi 10078  lnopconi 10080  lnopcon 10081  lnfnaddi 10089  lnfnmuli 10090  lnfnsubi 10092  nmbdfnlbi 10095  nmbdfnlb 10096  nmcfnexlem2 10098  nmcfnexlem3 10099  nmcfnexlem6 10102  nmcfnlbi 10104  nmcfnlb 10106  lnfnconi 10107  lnfncon 10108  nlelchi 10111  cnlnadjlem2 10118  cnlnadjlem7 10123  nmopadjlei 10138  nmoptrii 10144  nmopcoi 10145  nmopcoadji 10151  branmfn 10155  cnvbramul 10165  kbass6 10171  pjnmopi 10192  pjbdlni 10193  hmopidmchlem 10195  hmopidmchi 10196  hmopidmpji 10197  hmopidmpj 10199  pjsdii 10200  pjddii 10201  pjss2coi 10209  pjdifnormi 10212  pjssumi 10216  pjclem4 10245  pj3si 10253  pjs14i 10256  hstel 10260  hstel2 10264  hstoc 10267  hstnmoc 10268  hstpyth 10274  stj 10280  strlem2 10296  strlem3a 10297  strlem4 10299  hstrlem3a 10305  hstrlem4 10307  hstrlem5 10308  hstri 10310  stcltrlem1 10321  superpos 10399  sumdmdlem2 10464  cdj1i 10478  cdj3lem1 10479  cdj3lem2b 10482  cdj3lem3 10483  cdj3lem3b 10485  cdj3i 10486  elghomlem1 10503  ghomgrpilem1 10506  ghomgrpilem2 10507  ghomlin 10514  ghomid 10515  ghomf1olem 10517  cayleylem2 10531  cayleythlem 10534  fveq12d 10607  subspemp2 10693  plimfilOLD 10733  domval 10790  codval 10791  idval 10792  cmpval 10793  isded 10804  dedi 10805  1ded 10806  idosd 10812  domcmpd 10814  codcmpd 10815  1cat 10827  homib 10859  imonclem 10876  iepiclem 10886  cinvlem2 10891  isfuna 10896  isfunb 10897  idfisf 10902

This theorem was proved from axioms:  ax-1 4  ax-2 5  ax-3 6  ax-mp 7  ax-7 994  ax-gen 995  ax-8 996  ax-10 998  ax-11 999  ax-12 1000  ax-13 1001  ax-14 1002  ax-17 1003  ax-4 1005  ax-5o 1007  ax-6o 1010  ax-9o 1155  ax-10o 1173  ax-16 1243  ax-11o 1251  ax-ext 1494  ax-sep 2754  ax-pow 2794  ax-pr 2832

This theorem depends on definitions:  df-bi 145  df-or 222  df-an 223  df-ex 1013  df-sb 1205  df-eu 1415  df-mo 1416  df-clab 1500  df-cleq 1505  df-clel 1508  df-ne 1624  df-v 1850  df-dif 2093  df-un 2094  df-in 2095  df-ss 2097  df-nul 2325  df-pw 2447  df-sn 2457  df-pr 2458  df-op 2461  df-uni 2552  df-br 2670  df-opab 2718  df-xp 3239  df-cnv 3241  df-dm 3243  df-rn 3244  df-res 3245  df-ima 3246  df-fv 3253

Copyright terms: Public domain