Theorem oveq2d 6023

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 6015	. 2 ⊢ (𝐴 = 𝐵 → (𝐶𝐹𝐴) = (𝐶𝐹𝐵))
3	1, 2	syl 14	1 ⊢ (𝜑 → (𝐶𝐹𝐴) = (𝐶𝐹𝐵))

Syntax hints:   → wi 4   = wceq 1395  (class class class)co 6007

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 714  ax-5 1493  ax-7 1494  ax-gen 1495  ax-ie1 1539  ax-ie2 1540  ax-8 1550  ax-10 1551  ax-11 1552  ax-i12 1553  ax-bndl 1555  ax-4 1556  ax-17 1572  ax-i9 1576  ax-ial 1580  ax-i5r 1581  ax-ext 2211

This theorem depends on definitions:  df-bi 117  df-3an 1004  df-tru 1398  df-nf 1507  df-sb 1809  df-clab 2216  df-cleq 2222  df-clel 2225  df-nfc 2361  df-rex 2514  df-v 2801  df-un 3201  df-sn 3672  df-pr 3673  df-op 3675  df-uni 3889  df-br 4084  df-iota 5278  df-fv 5326  df-ov 6010

This theorem is referenced by:  csbov1g  6048  caovassg  6170  caovdig  6186  caovdirg  6189  caov32d  6192  caov4d  6196  caov42d  6198  nnaass  6639  nndi  6640  nnmass  6641  nnmsucr  6642  ecovass  6799  ecoviass  6800  ecovdi  6801  ecovidi  6802  addasspig  7528  mulasspig  7530  distrpig  7531  dfplpq2  7552  mulpipq2  7569  addassnqg  7580  prarloclemarch  7616  prarloclemarch2  7617  ltrnqg  7618  enq0sym  7630  addnq0mo  7645  mulnq0mo  7646  addnnnq0  7647  nq0a0  7655  distrnq0  7657  addassnq0  7660  prarloclemlo  7692  prarloclem3  7695  prarloclem5  7698  prarloclemcalc  7700  addnqprl  7727  addnqpru  7728  prmuloclemcalc  7763  mulnqprl  7766  mulnqpru  7767  distrlem4prl  7782  distrlem4pru  7783  1idprl  7788  1idpru  7789  ltexprlemloc  7805  addcanprleml  7812  addcanprlemu  7813  recexprlem1ssu  7832  ltmprr  7840  caucvgprlemcanl  7842  cauappcvgprlemladdru  7854  cauappcvgprlemladdrl  7855  cauappcvgprlem1  7857  cauappcvgprlemlim  7859  caucvgprlemnkj  7864  caucvgprlemnbj  7865  caucvgprlemdisj  7872  caucvgprlemloc  7873  caucvgprlemcl  7874  caucvgprlemladdrl  7876  caucvgprlem1  7877  caucvgpr  7880  caucvgprprlemell  7883  caucvgprprlemcbv  7885  caucvgprprlemval  7886  caucvgprprlemnkeqj  7888  caucvgprprlemopl  7895  caucvgprprlemlol  7896  caucvgprprlemloc  7901  caucvgprprlemclphr  7903  caucvgprprlemexb  7905  caucvgprprlemaddq  7906  caucvgprprlem1  7907  addcmpblnr  7937  mulcmpblnrlemg  7938  addsrmo  7941  mulsrmo  7942  addsrpr  7943  mulsrpr  7944  ltsrprg  7945  recexgt0sr  7971  mulgt0sr  7976  caucvgsrlemgt1  7993  caucvgsrlemoffval  7994  caucvgsr  8000  suplocsrlemb  8004  suplocsrlempr  8005  suplocsrlem  8006  suplocsr  8007  mulcnsr  8033  pitoregt0  8047  recidpirqlemcalc  8055  axmulcom  8069  axmulass  8071  axdistr  8072  ax0id  8076  axcnre  8079  recriota  8088  axcaucvglemcau  8096  axcaucvglemres  8097  mulrid  8154  adddirp1d  8184  mul32  8287  mul31  8288  add32  8316  add4  8318  add42  8319  cnegex  8335  addcan2  8338  addsubass  8367  subsub2  8385  nppcan2  8388  sub32  8391  nnncan  8392  sub4  8402  muladd  8541  subdi  8542  mul2neg  8555  submul2  8556  mulsub  8558  muls1d  8575  mulsubfacd  8576  add20  8632  recexre  8736  rereim  8744  apreap  8745  ltmul1  8750  cru  8760  apreim  8761  mulreim  8762  apadd1  8766  apneg  8769  mulap0  8812  divrecap  8846  divassap  8848  divmulasscomap  8854  divsubdirap  8866  divdivdivap  8871  divmul24ap  8874  divmuleqap  8875  divcanap6  8877  divdivap1  8881  divdivap2  8882  divsubdivap  8886  conjmulap  8887  div2negap  8893  apmul1  8946  cju  9119  nnmulcl  9142  add1p1  9372  sub1m1  9373  cnm2m1cnm3  9374  xp1d2m1eqxm1d2  9375  div4p1lem1div2  9376  un0addcl  9413  un0mulcl  9414  zaddcllemneg  9496  qapne  9846  cnref1o  9858  rexsub  10061  xnegid  10067  xaddcom  10069  xnegdi  10076  xaddass  10077  xaddass2  10078  xpncan  10079  xnpcan  10080  xleadd1a  10081  xsubge0  10089  xposdif  10090  xlesubadd  10091  xadd4d  10093  lincmb01cmp  10211  iccf1o  10212  ige3m2fz  10257  fztp  10286  fzsuc2  10287  fseq1m1p1  10303  fzm1  10308  ige2m1fz1  10317  nn0split  10344  nnsplit  10345  fzo0addelr  10407  elfzoext  10410  fzval3  10422  zpnn0elfzo1  10426  fzosplitsnm1  10427  fzosplitprm1  10452  fzoshftral  10456  rebtwn2zlemstep  10484  flhalf  10534  fldiv4lem1div2uz2  10538  modqval  10558  modqvalr  10559  modqdiffl  10569  modqfrac  10571  flqmod  10572  intqfrac  10573  zmod10  10574  modqmulnn  10576  modqvalp1  10577  modqid  10583  modqcyc  10593  modqcyc2  10594  modqmul1  10611  q2submod  10619  modqdi  10626  modqsubdir  10627  modqeqmodmin  10628  modsumfzodifsn  10630  addmodlteq  10632  frecuzrdgsuctlem  10657  uzsinds  10678  seqeq3  10686  iseqvalcbv  10693  seq3val  10694  seqvalcd  10695  seqf  10698  seq3p1  10699  seqovcd  10701  seqp1cd  10704  seq3m1  10707  seq3fveq2  10709  seqfveq2g  10711  seq3shft2  10715  seqshft2g  10716  monoord2  10720  ser3mono  10721  seq3split  10722  seqsplitg  10723  seq3caopr3  10725  seqcaopr3g  10726  seq3caopr2  10727  seqcaopr2g  10728  seq3caopr  10729  seqcaoprg  10730  seqf1oglem2a  10752  seqf1oglem2  10754  seq3id2  10760  seq3homo  10761  seq3z  10762  seqhomog  10764  exp3vallem  10774  exp3val  10775  expp1  10780  expnegap0  10781  expineg2  10782  expn1ap0  10783  expm1t  10801  1exp  10802  expnegzap  10807  mulexpzap  10813  expadd  10815  expaddzaplem  10816  expaddzap  10817  expmul  10818  expmulzap  10819  m1expeven  10820  expsubap  10821  expp1zap  10822  expm1ap  10823  expdivap  10824  iexpcyc  10878  subsq2  10881  binom2  10885  binom21  10886  binom2sub  10887  binom2sub1  10888  mulbinom2  10890  binom3  10891  zesq  10892  bernneq  10894  sqoddm1div8  10927  mulsubdivbinom2ap  10945  nn0opthlem1d  10954  nn0opthd  10956  facp1  10964  facnn2  10968  faclbnd  10975  faclbnd6  10978  bcval  10983  bccmpl  10988  bcn0  10989  bcnn  10991  bcnp1n  10993  bcm1k  10994  bcp1n  10995  bcp1nk  10996  bcval5  10997  bcp1m1  10999  bcpasc  11000  bcn2m1  11003  bcn2p1  11004  omgadd  11036  hashunlem  11038  hashunsng  11042  hashdifsn  11054  hashxp  11061  zfz1isolemsplit  11073  zfz1isolem1  11075  zfz1iso  11076  seq3coll  11077  wrdf  11090  ccatfvalfi  11140  elfzelfzccat  11148  ccatlid  11154  ccatrid  11155  ccatass  11156  ccatalpha  11161  ccatws1leng  11182  ccats1val2  11186  swrdval  11195  swrd00g  11196  swrdf  11202  swrdfv2  11210  swrdwrdsymbg  11211  swrdspsleq  11214  swrds1  11215  swrdlsw  11216  ccatswrd  11217  swrdccat2  11218  pfxmpt  11227  pfxfv  11231  pfxeq  11243  pfxsuff1eqwrdeq  11246  ccatpfx  11248  pfxccat1  11249  swrdswrd  11252  pfxswrd  11253  swrdpfx  11254  pfxpfx  11255  pfxlswccat  11260  ccats1pfxeq  11261  ccats1pfxeqrex  11262  ccatopth2  11264  cats1un  11268  wrdind  11269  wrd2ind  11270  swrdccatfn  11271  swrdccatin1  11272  pfxccatin12lem4  11273  swrdccatin2  11276  pfxccatin12lem2c  11277  pfxccatin12lem2  11278  pfxccatin12  11280  swrdccat  11282  swrdccat3blem  11286  swrdccat3b  11287  swrdccatin2d  11291  pfxccatin12d  11292  reuccatpfxs1lem  11293  reuccatpfxs1  11294  shftcan1  11360  shftcan2  11361  cjval  11371  cjth  11372  crre  11383  replim  11385  remim  11386  reim0b  11388  rereb  11389  mulreap  11390  cjreb  11392  recj  11393  reneg  11394  readd  11395  resub  11396  remullem  11397  imcj  11401  imneg  11402  imadd  11403  imsub  11404  cjcj  11409  cjadd  11410  ipcnval  11412  cjmulrcl  11413  cjneg  11416  addcj  11417  cjsub  11418  cnrecnv  11436  caucvgrelemcau  11506  cvg1nlemcau  11510  cvg1nlemres  11511  recvguniqlem  11520  resqrexlemover  11536  resqrexlemlo  11539  resqrexlemcalc1  11540  resqrexlemcalc3  11542  resqrexlemnm  11544  resqrexlemcvg  11545  absneg  11576  abscj  11578  sqabsadd  11581  sqabssub  11582  absmul  11595  absid  11597  absre  11603  absresq  11604  absexpzap  11606  recvalap  11623  abstri  11630  abs2dif2  11633  recan  11635  cau3lem  11640  amgm2  11644  bdtrilem  11765  xrmaxadd  11787  xrbdtri  11802  climaddc1  11855  climsubc1  11858  climcvg1nlem  11875  serf0  11878  summodclem3  11906  summodclem2a  11907  summodc  11909  fsumsplitsn  11936  fsumm1  11942  fsumsplitsnun  11945  fsump1  11946  isummulc2  11952  fsumrev  11969  fisum0diag2  11973  fsummulc2  11974  fsumsub  11978  fsumabs  11991  telfsumo  11992  fsumparts  11996  fsumrelem  11997  fsumiun  12003  binomlem  12009  binom  12010  binom1p  12011  binom11  12012  binom1dif  12013  bcxmas  12015  isumsplit  12017  isum1p  12018  divcnv  12023  arisum2  12025  trireciplem  12026  trirecip  12027  geolim  12037  georeclim  12039  geo2sum  12040  geo2lim  12042  geoisum1c  12046  0.999...  12047  cvgratnnlemnexp  12050  cvgratnnlemmn  12051  cvgratz  12058  mertenslem2  12062  mertensabs  12063  clim2prod  12065  prodfrecap  12072  prodfdivap  12073  prodmodclem3  12101  prodmodclem2a  12102  fprodm1  12124  fprodp1  12126  fprodunsn  12130  fprodfac  12141  fprodeq0  12143  fprodconst  12146  fprodrec  12155  fproddivap  12156  fprodsplitsn  12159  ege2le3  12197  efaddlem  12200  efsub  12207  efexp  12208  eftlub  12216  efsep  12217  effsumlt  12218  ef4p  12220  tanval3ap  12240  resinval  12241  recosval  12242  efi4p  12243  efival  12258  efmival  12259  efeul  12260  sinadd  12262  cosadd  12263  tanaddap  12265  sinsub  12266  cossub  12267  sincossq  12274  sin2t  12275  cos2t  12276  cos2tsin  12277  ef01bndlem  12282  sin01bnd  12283  cos01bnd  12284  cos12dec  12294  absef  12296  absefib  12297  efieq1re  12298  demoivreALT  12300  eirraplem  12303  dvdsexp  12387  oexpneg  12403  opeo  12423  omeo  12424  m1exp1  12427  flodddiv4  12462  flodddiv4t2lthalf  12465  bitsval  12469  bitsp1  12477  bitsinv1lem  12487  bitsinv1  12488  divgcdnnr  12512  gcdaddm  12520  gcdadd  12521  gcdid  12522  modgcd  12527  gcdmultipled  12529  dvdsgcdidd  12530  bezoutlemnewy  12532  bezoutlema  12535  bezoutlemb  12536  bezoutlemex  12537  bezoutlembz  12540  absmulgcd  12553  gcdmultiple  12556  gcdmultiplez  12557  rpmulgcd  12562  rplpwr  12563  eucalginv  12593  eucalg  12596  lcmneg  12611  lcmgcdlem  12614  lcmgcd  12615  lcmid  12617  lcm1  12618  mulgcddvds  12631  qredeq  12633  divgcdcoprmex  12639  prmind2  12657  rpexp1i  12691  pw2dvdslemn  12702  pw2dvdseulemle  12704  pw2dvdseu  12705  oddpwdclemxy  12706  oddpwdclemdvds  12707  oddpwdclemndvds  12708  oddpwdclemdc  12710  2sqpwodd  12713  nn0gcdsq  12737  phiprmpw  12759  eulerthlemrprm  12766  eulerthlema  12767  eulerthlemh  12768  eulerthlemth  12769  fermltl  12771  prmdiv  12772  hashgcdlem  12775  odzdvds  12783  vfermltl  12789  modprm0  12792  nnnn0modprm0  12793  modprmn0modprm0  12794  coprimeprodsq  12795  pythagtriplem1  12803  pythagtriplem4  12806  pythagtriplem12  12813  pythagtriplem14  12815  pythagtriplem16  12817  pythagtriplem18  12819  pythagtrip  12821  pcpremul  12831  pceu  12833  pczpre  12835  pcdiv  12840  pcqmul  12841  pcqdiv  12845  pcexp  12847  pcxqcl  12850  pczdvds  12852  pczndvds  12854  pczndvds2  12856  pcid  12862  pcneg  12863  pcdvdstr  12865  pcgcd1  12866  pcgcd  12867  pc2dvds  12868  pcaddlem  12877  pcadd  12878  pcadd2  12879  pcmpt  12881  pcmpt2  12882  fldivp1  12886  pcfac  12888  pcbc  12889  expnprm  12891  prmpwdvds  12893  pockthlem  12894  pockthi  12896  4sqlem7  12922  4sqlem9  12924  4sqlem10  12925  4sqlem2  12927  4sqlem3  12928  4sqlem4  12930  mul4sqlem  12931  4sqlem11  12939  4sqlem16  12944  4sqlem17  12945  4sqlem19  12947  setscomd  13088  ressvalsets  13112  strressid  13119  ressval3d  13120  ressinbasd  13122  ressressg  13123  ressabsg  13124  grpinvalem  13433  grpinva  13434  grprida  13435  isnsgrp  13454  sgrpass  13456  sgrp1  13459  sgrppropd  13461  prdssgrpd  13463  mnd32g  13475  mnd4g  13477  mndpropd  13488  prdsidlem  13495  prdsmndd  13496  imasmnd2  13500  mhmex  13510  mhmlin  13515  gsumwmhm  13546  grprcan  13585  grpsubval  13594  grpinvid2  13601  grpasscan2  13612  grpsubinv  13621  grpinvadd  13626  grpsubid1  13633  grpsubadd0sub  13635  grpsubadd  13636  grpsubsub  13637  grpaddsubass  13638  grppncan  13639  grpnnncan2  13645  grpsubpropd2  13653  imasgrp2  13662  mhmlem  13666  mhmid  13667  mhmmnd  13668  ghmgrp  13670  mulgnn0gsum  13680  mulgnnp1  13682  mulgaddcomlem  13697  mulgaddcom  13698  mulginvinv  13700  mulgnn0dir  13704  mulgdirlem  13705  mulgp1  13707  mulgneg2  13708  mulgnn0ass  13710  mulgass  13711  mulgmodid  13713  mulgsubdir  13714  nmzsubg  13762  0nsg  13766  eqger  13776  qussub  13789  ghmlin  13800  ghmsub  13803  conjghm  13828  ablsub4  13865  abladdsub4  13866  ablsubsub4  13871  ablsub32  13874  ablnnncan  13875  gsumfzmptfidmadd2  13892  gsumfzconst  13893  gsumfzmhm2  13896  gsumfzsnfd  13897  mgpress  13909  rngass  13917  rngdi  13918  rngdir  13919  rngrz  13924  rngmneg2  13926  rngsubdi  13929  rngsubdir  13930  rngpropd  13933  imasrng  13934  srgass  13949  srgpcomp  13968  srgpcompp  13969  srgpcomppsc  13970  srg1expzeq1  13973  ringpropd  14016  ringrz  14022  ringnegr  14030  ringmneg2  14032  ringsubdi  14034  ringsubdir  14035  ring1  14037  imasring  14042  opprrng  14055  opprring  14057  mulgass3  14063  dvdsrd  14073  unitgrp  14095  invrfvald  14101  dvr1  14117  dvrass  14118  dvrcan1  14119  dvrcan3  14120  rdivmuldivd  14123  subrginv  14216  subrgdv  14217  resrhm2b  14228  islmod  14270  lmodlema  14271  islmodd  14272  lmodvs0  14301  lmodvneg1  14309  lmodvsubval2  14321  lmodsubvs  14322  lmodsubdi  14323  lmodsubdir  14324  lmodprop2d  14327  rmodislmodlem  14329  rmodislmod  14330  lsssn0  14349  sraval  14416  cnfldsub  14554  gsumfzfsumlem0  14565  gsumfzfsumlemm  14566  mulgrhm  14588  mulgrhm2  14589  znval  14615  znval2  14617  znunit  14638  psrval  14645  mplvalcoe  14669  mplval2g  14674  restabs  14864  cnprcl2k  14895  cnrest2r  14926  ispsmet  15012  psmettri2  15017  psmetsym  15018  ismet  15033  isxmet  15034  xmettri2  15050  xmetsym  15057  xmettri3  15063  mettri3  15064  xblss2ps  15093  xblss2  15094  comet  15188  xmetxp  15196  xmetxpbl  15197  txmetcnp  15207  fsumcncntop  15256  cncfi  15267  divcncfap  15303  limccl  15348  ellimc3apf  15349  limccnpcntop  15364  limccnp2lem  15365  reldvg  15368  dvfvalap  15370  eldvap  15371  dvcj  15398  dvfre  15399  dvexp  15400  dvexp2  15401  dvrecap  15402  dvmptaddx  15408  dvmptmulx  15409  dvmptnegcn  15411  dvmptsubcn  15412  dvmptcjx  15413  dvmptfsum  15414  dveflem  15415  dvef  15416  plyconst  15434  plyaddlem1  15436  plymullem1  15437  plyadd  15440  plymul  15441  plycoeid3  15446  plycolemc  15447  plyco  15448  plycjlemc  15449  plycj  15450  plyrecj  15452  dvply1  15454  dvply2g  15455  sin0pilem1  15470  sin0pilem2  15471  efper  15496  sinperlem  15497  efimpi  15508  ptolemy  15513  tangtx  15527  abssinper  15535  cosq34lt1  15539  rpcxpef  15583  rpcxpp1  15595  rpcxpneg  15596  rpcxpsub  15597  rpmulcxp  15598  rpdivcxp  15600  cxpmul  15601  rpcxpmul2  15602  rpcxproot  15603  cxpcom  15627  rpabscxpbnd  15629  rplogbval  15634  rplogbreexp  15642  rplogbzexp  15643  rprelogbmulexp  15645  rprelogbdiv  15646  relogbexpap  15647  rplogbcxp  15652  rpcxplogb  15653  logbgcd1irr  15656  logbgcd1irraplemap  15658  binom4  15668  wilthlem1  15669  sgmval  15672  sgmppw  15681  1sgmprm  15683  mersenne  15686  perfectlem1  15688  perfectlem2  15689  perfect  15690  lgslem1  15694  lgsval  15698  lgsfvalg  15699  lgsval2lem  15704  lgsval4  15714  lgsneg  15718  lgsneg1  15719  lgsmod  15720  lgsdir2  15727  lgsdirprm  15728  lgsdilem2  15730  lgsdi  15731  lgsne0  15732  lgssq2  15735  lgsdirnn0  15741  lgsdinn0  15742  gausslemma2dlem1a  15752  gausslemma2dlem1f1o  15754  gausslemma2dlem2  15756  gausslemma2dlem3  15757  gausslemma2dlem4  15758  gausslemma2dlem5  15760  gausslemma2dlem6  15761  gausslemma2d  15763  lgseisenlem1  15764  lgseisenlem2  15765  lgseisenlem3  15766  lgseisenlem4  15767  lgsquadlem1  15771  lgsquadlem2  15772  lgsquadlem3  15773  lgsquad2lem1  15775  lgsquad2lem2  15776  lgsquad2  15777  lgsquad3  15778  m1lgs  15779  2lgslem3c  15789  2lgslem3d  15790  2lgslem3d1  15794  2sqlem2  15809  2sqlem3  15811  2sqlem4  15812  2sqlem8  15817  2sqlem9  15818  2sqlem10  15819  vtxdumgrfival  16057  iswlk  16064  upgr2wlkdc  16116  wlkres  16118  trlreslem  16127  isclwwlk  16132  clwwlkccatlem  16137  qdencn  16455  trilpolemclim  16464  trilpolemcl  16465  trilpolemisumle  16466  trilpolemeq1  16468  trilpolemlt1  16469  trilpo  16471  apdifflemf  16474  apdiff  16476  iswomni0  16479  redcwlpolemeq1  16482  redcwlpo  16483  nconstwlpolem0  16491  nconstwlpolemgt0  16492  nconstwlpo  16494  neapmkv  16496