Theorem oveq2d 5983

Description: Equality deduction for operation value. (Contributed by NM, 13-Mar-1995.)

Hypothesis

Ref	Expression
oveq1d.1	⊢ (𝜑 → 𝐴 = 𝐵)

Assertion

Ref	Expression
oveq2d	⊢ (𝜑 → (𝐶𝐹𝐴) = (𝐶𝐹𝐵))

Proof of Theorem oveq2d

Step	Hyp	Ref	Expression
1		oveq1d.1	. 2 ⊢ (𝜑 → 𝐴 = 𝐵)
2		oveq2 5975	. 2 ⊢ (𝐴 = 𝐵 → (𝐶𝐹𝐴) = (𝐶𝐹𝐵))
3	1, 2	syl 14	1 ⊢ (𝜑 → (𝐶𝐹𝐴) = (𝐶𝐹𝐵))

Syntax hints:   → wi 4   = wceq 1373  (class class class)co 5967

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 711  ax-5 1471  ax-7 1472  ax-gen 1473  ax-ie1 1517  ax-ie2 1518  ax-8 1528  ax-10 1529  ax-11 1530  ax-i12 1531  ax-bndl 1533  ax-4 1534  ax-17 1550  ax-i9 1554  ax-ial 1558  ax-i5r 1559  ax-ext 2189

This theorem depends on definitions:  df-bi 117  df-3an 983  df-tru 1376  df-nf 1485  df-sb 1787  df-clab 2194  df-cleq 2200  df-clel 2203  df-nfc 2339  df-rex 2492  df-v 2778  df-un 3178  df-sn 3649  df-pr 3650  df-op 3652  df-uni 3865  df-br 4060  df-iota 5251  df-fv 5298  df-ov 5970

This theorem is referenced by:  csbov1g  6008  caovassg  6128  caovdig  6144  caovdirg  6147  caov32d  6150  caov4d  6154  caov42d  6156  nnaass  6594  nndi  6595  nnmass  6596  nnmsucr  6597  ecovass  6754  ecoviass  6755  ecovdi  6756  ecovidi  6757  addasspig  7478  mulasspig  7480  distrpig  7481  dfplpq2  7502  mulpipq2  7519  addassnqg  7530  prarloclemarch  7566  prarloclemarch2  7567  ltrnqg  7568  enq0sym  7580  addnq0mo  7595  mulnq0mo  7596  addnnnq0  7597  nq0a0  7605  distrnq0  7607  addassnq0  7610  prarloclemlo  7642  prarloclem3  7645  prarloclem5  7648  prarloclemcalc  7650  addnqprl  7677  addnqpru  7678  prmuloclemcalc  7713  mulnqprl  7716  mulnqpru  7717  distrlem4prl  7732  distrlem4pru  7733  1idprl  7738  1idpru  7739  ltexprlemloc  7755  addcanprleml  7762  addcanprlemu  7763  recexprlem1ssu  7782  ltmprr  7790  caucvgprlemcanl  7792  cauappcvgprlemladdru  7804  cauappcvgprlemladdrl  7805  cauappcvgprlem1  7807  cauappcvgprlemlim  7809  caucvgprlemnkj  7814  caucvgprlemnbj  7815  caucvgprlemdisj  7822  caucvgprlemloc  7823  caucvgprlemcl  7824  caucvgprlemladdrl  7826  caucvgprlem1  7827  caucvgpr  7830  caucvgprprlemell  7833  caucvgprprlemcbv  7835  caucvgprprlemval  7836  caucvgprprlemnkeqj  7838  caucvgprprlemopl  7845  caucvgprprlemlol  7846  caucvgprprlemloc  7851  caucvgprprlemclphr  7853  caucvgprprlemexb  7855  caucvgprprlemaddq  7856  caucvgprprlem1  7857  addcmpblnr  7887  mulcmpblnrlemg  7888  addsrmo  7891  mulsrmo  7892  addsrpr  7893  mulsrpr  7894  ltsrprg  7895  recexgt0sr  7921  mulgt0sr  7926  caucvgsrlemgt1  7943  caucvgsrlemoffval  7944  caucvgsr  7950  suplocsrlemb  7954  suplocsrlempr  7955  suplocsrlem  7956  suplocsr  7957  mulcnsr  7983  pitoregt0  7997  recidpirqlemcalc  8005  axmulcom  8019  axmulass  8021  axdistr  8022  ax0id  8026  axcnre  8029  recriota  8038  axcaucvglemcau  8046  axcaucvglemres  8047  mulrid  8104  adddirp1d  8134  mul32  8237  mul31  8238  add32  8266  add4  8268  add42  8269  cnegex  8285  addcan2  8288  addsubass  8317  subsub2  8335  nppcan2  8338  sub32  8341  nnncan  8342  sub4  8352  muladd  8491  subdi  8492  mul2neg  8505  submul2  8506  mulsub  8508  muls1d  8525  mulsubfacd  8526  add20  8582  recexre  8686  rereim  8694  apreap  8695  ltmul1  8700  cru  8710  apreim  8711  mulreim  8712  apadd1  8716  apneg  8719  mulap0  8762  divrecap  8796  divassap  8798  divmulasscomap  8804  divsubdirap  8816  divdivdivap  8821  divmul24ap  8824  divmuleqap  8825  divcanap6  8827  divdivap1  8831  divdivap2  8832  divsubdivap  8836  conjmulap  8837  div2negap  8843  apmul1  8896  cju  9069  nnmulcl  9092  add1p1  9322  sub1m1  9323  cnm2m1cnm3  9324  xp1d2m1eqxm1d2  9325  div4p1lem1div2  9326  un0addcl  9363  un0mulcl  9364  zaddcllemneg  9446  qapne  9795  cnref1o  9807  rexsub  10010  xnegid  10016  xaddcom  10018  xnegdi  10025  xaddass  10026  xaddass2  10027  xpncan  10028  xnpcan  10029  xleadd1a  10030  xsubge0  10038  xposdif  10039  xlesubadd  10040  xadd4d  10042  lincmb01cmp  10160  iccf1o  10161  ige3m2fz  10206  fztp  10235  fzsuc2  10236  fseq1m1p1  10252  fzm1  10257  ige2m1fz1  10266  nn0split  10293  nnsplit  10294  fzo0addelr  10355  elfzoext  10358  fzval3  10370  zpnn0elfzo1  10374  fzosplitsnm1  10375  fzosplitprm1  10400  fzoshftral  10404  rebtwn2zlemstep  10432  flhalf  10482  fldiv4lem1div2uz2  10486  modqval  10506  modqvalr  10507  modqdiffl  10517  modqfrac  10519  flqmod  10520  intqfrac  10521  zmod10  10522  modqmulnn  10524  modqvalp1  10525  modqid  10531  modqcyc  10541  modqcyc2  10542  modqmul1  10559  q2submod  10567  modqdi  10574  modqsubdir  10575  modqeqmodmin  10576  modsumfzodifsn  10578  addmodlteq  10580  frecuzrdgsuctlem  10605  uzsinds  10626  seqeq3  10634  iseqvalcbv  10641  seq3val  10642  seqvalcd  10643  seqf  10646  seq3p1  10647  seqovcd  10649  seqp1cd  10652  seq3m1  10655  seq3fveq2  10657  seqfveq2g  10659  seq3shft2  10663  seqshft2g  10664  monoord2  10668  ser3mono  10669  seq3split  10670  seqsplitg  10671  seq3caopr3  10673  seqcaopr3g  10674  seq3caopr2  10675  seqcaopr2g  10676  seq3caopr  10677  seqcaoprg  10678  seqf1oglem2a  10700  seqf1oglem2  10702  seq3id2  10708  seq3homo  10709  seq3z  10710  seqhomog  10712  exp3vallem  10722  exp3val  10723  expp1  10728  expnegap0  10729  expineg2  10730  expn1ap0  10731  expm1t  10749  1exp  10750  expnegzap  10755  mulexpzap  10761  expadd  10763  expaddzaplem  10764  expaddzap  10765  expmul  10766  expmulzap  10767  m1expeven  10768  expsubap  10769  expp1zap  10770  expm1ap  10771  expdivap  10772  iexpcyc  10826  subsq2  10829  binom2  10833  binom21  10834  binom2sub  10835  binom2sub1  10836  mulbinom2  10838  binom3  10839  zesq  10840  bernneq  10842  sqoddm1div8  10875  mulsubdivbinom2ap  10893  nn0opthlem1d  10902  nn0opthd  10904  facp1  10912  facnn2  10916  faclbnd  10923  faclbnd6  10926  bcval  10931  bccmpl  10936  bcn0  10937  bcnn  10939  bcnp1n  10941  bcm1k  10942  bcp1n  10943  bcp1nk  10944  bcval5  10945  bcp1m1  10947  bcpasc  10948  bcn2m1  10951  bcn2p1  10952  omgadd  10984  hashunlem  10986  hashunsng  10989  hashdifsn  11001  hashxp  11008  zfz1isolemsplit  11020  zfz1isolem1  11022  zfz1iso  11023  seq3coll  11024  wrdf  11037  ccatfvalfi  11086  elfzelfzccat  11094  ccatlid  11100  ccatrid  11101  ccatass  11102  ccatws1leng  11126  ccats1val2  11130  swrdval  11139  swrd00g  11140  swrdf  11146  swrdfv2  11154  swrdwrdsymbg  11155  swrdspsleq  11158  swrds1  11159  swrdlsw  11160  ccatswrd  11161  swrdccat2  11162  pfxmpt  11171  pfxfv  11175  pfxeq  11187  pfxsuff1eqwrdeq  11190  ccatpfx  11192  pfxccat1  11193  swrdswrd  11196  pfxswrd  11197  swrdpfx  11198  pfxpfx  11199  pfxlswccat  11204  ccats1pfxeq  11205  ccats1pfxeqrex  11206  ccatopth2  11208  cats1un  11212  wrdind  11213  wrd2ind  11214  swrdccatfn  11215  swrdccatin1  11216  pfxccatin12lem4  11217  swrdccatin2  11220  pfxccatin12lem2c  11221  pfxccatin12lem2  11222  pfxccatin12  11224  swrdccat  11226  swrdccat3blem  11230  swrdccat3b  11231  swrdccatin2d  11235  pfxccatin12d  11236  reuccatpfxs1lem  11237  reuccatpfxs1  11238  shftcan1  11260  shftcan2  11261  cjval  11271  cjth  11272  crre  11283  replim  11285  remim  11286  reim0b  11288  rereb  11289  mulreap  11290  cjreb  11292  recj  11293  reneg  11294  readd  11295  resub  11296  remullem  11297  imcj  11301  imneg  11302  imadd  11303  imsub  11304  cjcj  11309  cjadd  11310  ipcnval  11312  cjmulrcl  11313  cjneg  11316  addcj  11317  cjsub  11318  cnrecnv  11336  caucvgrelemcau  11406  cvg1nlemcau  11410  cvg1nlemres  11411  recvguniqlem  11420  resqrexlemover  11436  resqrexlemlo  11439  resqrexlemcalc1  11440  resqrexlemcalc3  11442  resqrexlemnm  11444  resqrexlemcvg  11445  absneg  11476  abscj  11478  sqabsadd  11481  sqabssub  11482  absmul  11495  absid  11497  absre  11503  absresq  11504  absexpzap  11506  recvalap  11523  abstri  11530  abs2dif2  11533  recan  11535  cau3lem  11540  amgm2  11544  bdtrilem  11665  xrmaxadd  11687  xrbdtri  11702  climaddc1  11755  climsubc1  11758  climcvg1nlem  11775  serf0  11778  summodclem3  11806  summodclem2a  11807  summodc  11809  fsumsplitsn  11836  fsumm1  11842  fsumsplitsnun  11845  fsump1  11846  isummulc2  11852  fsumrev  11869  fisum0diag2  11873  fsummulc2  11874  fsumsub  11878  fsumabs  11891  telfsumo  11892  fsumparts  11896  fsumrelem  11897  fsumiun  11903  binomlem  11909  binom  11910  binom1p  11911  binom11  11912  binom1dif  11913  bcxmas  11915  isumsplit  11917  isum1p  11918  divcnv  11923  arisum2  11925  trireciplem  11926  trirecip  11927  geolim  11937  georeclim  11939  geo2sum  11940  geo2lim  11942  geoisum1c  11946  0.999...  11947  cvgratnnlemnexp  11950  cvgratnnlemmn  11951  cvgratz  11958  mertenslem2  11962  mertensabs  11963  clim2prod  11965  prodfrecap  11972  prodfdivap  11973  prodmodclem3  12001  prodmodclem2a  12002  fprodm1  12024  fprodp1  12026  fprodunsn  12030  fprodfac  12041  fprodeq0  12043  fprodconst  12046  fprodrec  12055  fproddivap  12056  fprodsplitsn  12059  ege2le3  12097  efaddlem  12100  efsub  12107  efexp  12108  eftlub  12116  efsep  12117  effsumlt  12118  ef4p  12120  tanval3ap  12140  resinval  12141  recosval  12142  efi4p  12143  efival  12158  efmival  12159  efeul  12160  sinadd  12162  cosadd  12163  tanaddap  12165  sinsub  12166  cossub  12167  sincossq  12174  sin2t  12175  cos2t  12176  cos2tsin  12177  ef01bndlem  12182  sin01bnd  12183  cos01bnd  12184  cos12dec  12194  absef  12196  absefib  12197  efieq1re  12198  demoivreALT  12200  eirraplem  12203  dvdsexp  12287  oexpneg  12303  opeo  12323  omeo  12324  m1exp1  12327  flodddiv4  12362  flodddiv4t2lthalf  12365  bitsval  12369  bitsp1  12377  bitsinv1lem  12387  bitsinv1  12388  divgcdnnr  12412  gcdaddm  12420  gcdadd  12421  gcdid  12422  modgcd  12427  gcdmultipled  12429  dvdsgcdidd  12430  bezoutlemnewy  12432  bezoutlema  12435  bezoutlemb  12436  bezoutlemex  12437  bezoutlembz  12440  absmulgcd  12453  gcdmultiple  12456  gcdmultiplez  12457  rpmulgcd  12462  rplpwr  12463  eucalginv  12493  eucalg  12496  lcmneg  12511  lcmgcdlem  12514  lcmgcd  12515  lcmid  12517  lcm1  12518  mulgcddvds  12531  qredeq  12533  divgcdcoprmex  12539  prmind2  12557  rpexp1i  12591  pw2dvdslemn  12602  pw2dvdseulemle  12604  pw2dvdseu  12605  oddpwdclemxy  12606  oddpwdclemdvds  12607  oddpwdclemndvds  12608  oddpwdclemdc  12610  2sqpwodd  12613  nn0gcdsq  12637  phiprmpw  12659  eulerthlemrprm  12666  eulerthlema  12667  eulerthlemh  12668  eulerthlemth  12669  fermltl  12671  prmdiv  12672  hashgcdlem  12675  odzdvds  12683  vfermltl  12689  modprm0  12692  nnnn0modprm0  12693  modprmn0modprm0  12694  coprimeprodsq  12695  pythagtriplem1  12703  pythagtriplem4  12706  pythagtriplem12  12713  pythagtriplem14  12715  pythagtriplem16  12717  pythagtriplem18  12719  pythagtrip  12721  pcpremul  12731  pceu  12733  pczpre  12735  pcdiv  12740  pcqmul  12741  pcqdiv  12745  pcexp  12747  pcxqcl  12750  pczdvds  12752  pczndvds  12754  pczndvds2  12756  pcid  12762  pcneg  12763  pcdvdstr  12765  pcgcd1  12766  pcgcd  12767  pc2dvds  12768  pcaddlem  12777  pcadd  12778  pcadd2  12779  pcmpt  12781  pcmpt2  12782  fldivp1  12786  pcfac  12788  pcbc  12789  expnprm  12791  prmpwdvds  12793  pockthlem  12794  pockthi  12796  4sqlem7  12822  4sqlem9  12824  4sqlem10  12825  4sqlem2  12827  4sqlem3  12828  4sqlem4  12830  mul4sqlem  12831  4sqlem11  12839  4sqlem16  12844  4sqlem17  12845  4sqlem19  12847  setscomd  12988  ressvalsets  13011  strressid  13018  ressval3d  13019  ressinbasd  13021  ressressg  13022  ressabsg  13023  grpinvalem  13332  grpinva  13333  grprida  13334  isnsgrp  13353  sgrpass  13355  sgrp1  13358  sgrppropd  13360  prdssgrpd  13362  mnd32g  13374  mnd4g  13376  mndpropd  13387  prdsidlem  13394  prdsmndd  13395  imasmnd2  13399  mhmex  13409  mhmlin  13414  gsumwmhm  13445  grprcan  13484  grpsubval  13493  grpinvid2  13500  grpasscan2  13511  grpsubinv  13520  grpinvadd  13525  grpsubid1  13532  grpsubadd0sub  13534  grpsubadd  13535  grpsubsub  13536  grpaddsubass  13537  grppncan  13538  grpnnncan2  13544  grpsubpropd2  13552  imasgrp2  13561  mhmlem  13565  mhmid  13566  mhmmnd  13567  ghmgrp  13569  mulgnn0gsum  13579  mulgnnp1  13581  mulgaddcomlem  13596  mulgaddcom  13597  mulginvinv  13599  mulgnn0dir  13603  mulgdirlem  13604  mulgp1  13606  mulgneg2  13607  mulgnn0ass  13609  mulgass  13610  mulgmodid  13612  mulgsubdir  13613  nmzsubg  13661  0nsg  13665  eqger  13675  qussub  13688  ghmlin  13699  ghmsub  13702  conjghm  13727  ablsub4  13764  abladdsub4  13765  ablsubsub4  13770  ablsub32  13773  ablnnncan  13774  gsumfzmptfidmadd2  13791  gsumfzconst  13792  gsumfzmhm2  13795  gsumfzsnfd  13796  mgpress  13808  rngass  13816  rngdi  13817  rngdir  13818  rngrz  13823  rngmneg2  13825  rngsubdi  13828  rngsubdir  13829  rngpropd  13832  imasrng  13833  srgass  13848  srgpcomp  13867  srgpcompp  13868  srgpcomppsc  13869  srg1expzeq1  13872  ringpropd  13915  ringrz  13921  ringnegr  13929  ringmneg2  13931  ringsubdi  13933  ringsubdir  13934  ring1  13936  imasring  13941  opprrng  13954  opprring  13956  mulgass3  13962  dvdsrd  13971  unitgrp  13993  invrfvald  13999  dvr1  14015  dvrass  14016  dvrcan1  14017  dvrcan3  14018  rdivmuldivd  14021  subrginv  14114  subrgdv  14115  resrhm2b  14126  islmod  14168  lmodlema  14169  islmodd  14170  lmodvs0  14199  lmodvneg1  14207  lmodvsubval2  14219  lmodsubvs  14220  lmodsubdi  14221  lmodsubdir  14222  lmodprop2d  14225  rmodislmodlem  14227  rmodislmod  14228  lsssn0  14247  sraval  14314  cnfldsub  14452  gsumfzfsumlem0  14463  gsumfzfsumlemm  14464  mulgrhm  14486  mulgrhm2  14487  znval  14513  znval2  14515  znunit  14536  psrval  14543  mplvalcoe  14567  mplval2g  14572  restabs  14762  cnprcl2k  14793  cnrest2r  14824  ispsmet  14910  psmettri2  14915  psmetsym  14916  ismet  14931  isxmet  14932  xmettri2  14948  xmetsym  14955  xmettri3  14961  mettri3  14962  xblss2ps  14991  xblss2  14992  comet  15086  xmetxp  15094  xmetxpbl  15095  txmetcnp  15105  fsumcncntop  15154  cncfi  15165  divcncfap  15201  limccl  15246  ellimc3apf  15247  limccnpcntop  15262  limccnp2lem  15263  reldvg  15266  dvfvalap  15268  eldvap  15269  dvcj  15296  dvfre  15297  dvexp  15298  dvexp2  15299  dvrecap  15300  dvmptaddx  15306  dvmptmulx  15307  dvmptnegcn  15309  dvmptsubcn  15310  dvmptcjx  15311  dvmptfsum  15312  dveflem  15313  dvef  15314  plyconst  15332  plyaddlem1  15334  plymullem1  15335  plyadd  15338  plymul  15339  plycoeid3  15344  plycolemc  15345  plyco  15346  plycjlemc  15347  plycj  15348  plyrecj  15350  dvply1  15352  dvply2g  15353  sin0pilem1  15368  sin0pilem2  15369  efper  15394  sinperlem  15395  efimpi  15406  ptolemy  15411  tangtx  15425  abssinper  15433  cosq34lt1  15437  rpcxpef  15481  rpcxpp1  15493  rpcxpneg  15494  rpcxpsub  15495  rpmulcxp  15496  rpdivcxp  15498  cxpmul  15499  rpcxpmul2  15500  rpcxproot  15501  cxpcom  15525  rpabscxpbnd  15527  rplogbval  15532  rplogbreexp  15540  rplogbzexp  15541  rprelogbmulexp  15543  rprelogbdiv  15544  relogbexpap  15545  rplogbcxp  15550  rpcxplogb  15551  logbgcd1irr  15554  logbgcd1irraplemap  15556  binom4  15566  wilthlem1  15567  sgmval  15570  sgmppw  15579  1sgmprm  15581  mersenne  15584  perfectlem1  15586  perfectlem2  15587  perfect  15588  lgslem1  15592  lgsval  15596  lgsfvalg  15597  lgsval2lem  15602  lgsval4  15612  lgsneg  15616  lgsneg1  15617  lgsmod  15618  lgsdir2  15625  lgsdirprm  15626  lgsdilem2  15628  lgsdi  15629  lgsne0  15630  lgssq2  15633  lgsdirnn0  15639  lgsdinn0  15640  gausslemma2dlem1a  15650  gausslemma2dlem1f1o  15652  gausslemma2dlem2  15654  gausslemma2dlem3  15655  gausslemma2dlem4  15656  gausslemma2dlem5  15658  gausslemma2dlem6  15659  gausslemma2d  15661  lgseisenlem1  15662  lgseisenlem2  15663  lgseisenlem3  15664  lgseisenlem4  15665  lgsquadlem1  15669  lgsquadlem2  15670  lgsquadlem3  15671  lgsquad2lem1  15673  lgsquad2lem2  15674  lgsquad2  15675  lgsquad3  15676  m1lgs  15677  2lgslem3c  15687  2lgslem3d  15688  2lgslem3d1  15692  2sqlem2  15707  2sqlem3  15709  2sqlem4  15710  2sqlem8  15715  2sqlem9  15716  2sqlem10  15717  qdencn  16168  trilpolemclim  16177  trilpolemcl  16178  trilpolemisumle  16179  trilpolemeq1  16181  trilpolemlt1  16182  trilpo  16184  apdifflemf  16187  apdiff  16189  iswomni0  16192  redcwlpolemeq1  16195  redcwlpo  16196  nconstwlpolem0  16204  nconstwlpolemgt0  16205  nconstwlpo  16207  neapmkv  16209