Theorem oveq2d 6101

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

This proof depends on syntax axioms:   → wi 4   = wceq 1402  (class class class)co 6085

This proof depends on axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-ia1 106  ax-ia2 107  ax-ia3 108  ax-io 721  ax-5 1500  ax-7 1501  ax-gen 1502  ax-ie1 1546  ax-ie2 1547  ax-8 1557  ax-10 1558  ax-11 1559  ax-i12 1560  ax-bndl 1562  ax-4 1563  ax-17 1579  ax-i9 1583  ax-ial 1587  ax-i5r 1588  ax-ext 2220

This proof depends on definitions:  df-bi 117  df-3an 1011  df-tru 1405  df-nf 1514  df-sb 1816  df-clab 2225  df-cleq 2231  df-clel 2234  df-nfc 2381  df-rex 2534  df-v 2823  df-un 3224  df-sn 3715  df-pr 3716  df-op 3718  df-uni 3936  df-br 4131  df-iota 5337  df-fv 5385  df-ov 6088

This theorem is used by:  csbov1g  6126  caovassg  6248  caovdig  6264  caovdirg  6267  caov32d  6270  caov4d  6274  caov42d  6276  suppofss1dcl  6504  suppofss2dcl  6505  nnaass  6758  nndi  6759  nnmass  6760  nnmsucr  6761  ecovass  6918  ecoviass  6919  ecovdi  6920  ecovidi  6921  addasspig  7697  mulasspig  7699  distrpig  7700  dfplpq2  7721  mulpipq2  7738  addassnqg  7749  prarloclemarch  7785  prarloclemarch2  7786  ltrnqg  7787  enq0sym  7799  addnq0mo  7814  mulnq0mo  7815  addnnnq0  7816  nq0a0  7824  distrnq0  7826  addassnq0  7829  prarloclemlo  7861  prarloclem3  7864  prarloclem5  7867  prarloclemcalc  7869  addnqprl  7896  addnqpru  7897  prmuloclemcalc  7932  mulnqprl  7935  mulnqpru  7936  distrlem4prl  7951  distrlem4pru  7952  1idprl  7957  1idpru  7958  ltexprlemloc  7974  addcanprleml  7981  addcanprlemu  7982  recexprlem1ssu  8001  ltmprr  8009  caucvgprlemcanl  8011  cauappcvgprlemladdru  8023  cauappcvgprlemladdrl  8024  cauappcvgprlem1  8026  cauappcvgprlemlim  8028  caucvgprlemnkj  8033  caucvgprlemnbj  8034  caucvgprlemdisj  8041  caucvgprlemloc  8042  caucvgprlemcl  8043  caucvgprlemladdrl  8045  caucvgprlem1  8046  caucvgpr  8049  caucvgprprlemell  8052  caucvgprprlemcbv  8054  caucvgprprlemval  8055  caucvgprprlemnkeqj  8057  caucvgprprlemopl  8064  caucvgprprlemlol  8065  caucvgprprlemloc  8070  caucvgprprlemclphr  8072  caucvgprprlemexb  8074  caucvgprprlemaddq  8075  caucvgprprlem1  8076  addcmpblnr  8106  mulcmpblnrlemg  8107  addsrmo  8110  mulsrmo  8111  addsrpr  8112  mulsrpr  8113  ltsrprg  8114  recexgt0sr  8140  mulgt0sr  8145  caucvgsrlemgt1  8162  caucvgsrlemoffval  8163  caucvgsr  8169  suplocsrlemb  8173  suplocsrlempr  8174  suplocsrlem  8175  suplocsr  8176  mulcnsr  8202  pitoregt0  8216  recidpirqlemcalc  8224  axmulcom  8238  axmulass  8240  axdistr  8241  ax0id  8245  axcnre  8248  recriota  8257  axcaucvglemcau  8265  axcaucvglemres  8266  mulrid  8323  adddirp1d  8352  mul32  8456  mul31  8457  add32  8485  add4  8487  add42  8488  cnegex  8504  addcan2  8507  addsubass  8536  subsub2  8554  nppcan2  8557  sub32  8560  nnncan  8561  sub4  8571  muladd  8711  subdi  8712  mul2neg  8725  submul2  8726  mulsub  8728  muls1d  8745  mulsubfacd  8746  add20  8802  recexre  8906  rereim  8914  apreap  8915  ltmul1  8920  cru  8930  apreim  8931  mulreim  8932  apadd1  8936  apneg  8939  mulap0  8982  divrecap  9018  divassap  9020  divmulasscomap  9026  divsubdirap  9038  divdivdivap  9043  divmul24ap  9046  divmuleqap  9047  divcanap6  9049  divdivap1  9053  divdivap2  9054  divsubdivap  9058  conjmulap  9059  div2negap  9065  apmul1  9118  cju  9291  nnmulcl  9325  add1p1  9555  sub1m1  9556  cnm2m1cnm3  9557  xp1d2m1eqxm1d2  9558  div4p1lem1div2  9559  un0addcl  9596  un0mulcl  9597  zaddcllemneg  9683  qapne  10039  cnref1o  10051  rexsub  10255  xnegid  10261  xaddcom  10263  xnegdi  10270  xaddass  10271  xaddass2  10272  xpncan  10273  xnpcan  10274  xleadd1a  10275  xsubge0  10283  xposdif  10284  xlesubadd  10285  xadd4d  10287  lincmb01cmp  10405  iccf1o  10407  ige3m2fz  10454  fztp  10485  fzsuc2  10486  fseq1m1p1  10502  fzm1  10507  ige2m1fz1  10516  nn0split  10543  nnsplit  10544  fzo0addelr  10607  elfzoext  10610  fzval3  10622  zpnn0elfzo1  10626  fzosplitsnm1  10627  fzosplitpr  10652  fzosplitprm1  10653  fzoshftral  10657  rebtwn2zlemstep  10687  flhalf  10737  fldiv4lem1div2uz2  10741  modqval  10761  modqvalr  10762  modqdiffl  10772  modqfrac  10774  flqmod  10775  intqfrac  10776  zmod10  10777  modqmulnn  10779  modqvalp1  10780  modqid  10786  modqcyc  10796  modqcyc2  10797  modqmul1  10814  q2submod  10822  modqdi  10829  modqsubdir  10830  modqeqmodmin  10831  modsumfzodifsn  10833  addmodlteq  10835  frecuzrdgsuctlem  10860  uzsinds  10881  seqeq3  10889  iseqvalcbv  10896  seq3val  10897  seqvalcd  10898  seqf  10901  seq3p1  10902  seqovcd  10904  seqp1cd  10907  seq3m1  10910  seq3fveq2  10912  seqfveq2g  10914  seq3shft2  10918  seqshft2g  10919  monoord2  10923  ser3mono  10924  seq3split  10925  seqsplitg  10926  seq3caopr3  10928  seqcaopr3g  10929  seq3caopr2  10930  seqcaopr2g  10931  seq3caopr  10932  seqcaoprg  10933  seqf1oglem2a  10955  seqf1oglem2  10957  seq3id2  10963  seq3homo  10964  seq3z  10965  seqhomog  10967  exp3vallem  10977  exp3val  10978  expp1  10983  expnegap0  10984  expineg2  10985  expn1ap0  10986  expm1t  11004  1exp  11005  expnegzap  11010  mulexpzap  11016  expadd  11018  expaddzaplem  11019  expaddzap  11020  expmul  11021  expmulzap  11022  m1expeven  11023  expsubap  11024  expp1zap  11025  expm1ap  11026  expdivap  11027  iexpcyc  11081  subsq2  11084  binom2  11088  binom21  11089  binom2sub  11090  binom2sub1  11091  mulbinom2  11093  binom3  11094  zesq  11096  bernneq  11098  sqoddm1div8  11131  mulsubdivbinom2ap  11149  nn0opthlem1d  11158  nn0opthd  11160  facp1  11168  facnn2  11172  faclbnd  11179  faclbnd6  11182  bcval  11187  bccmpl  11192  bcn0  11193  bcnn  11195  bcnp1n  11197  bcm1k  11198  bcp1n  11199  bcp1nk  11200  bcval5  11201  bcp1m1  11203  bcpasc  11204  bcm1n  11207  bcn2m1  11208  bcn2p1  11209  omgadd  11242  hashunlem  11244  hashunsng  11248  hashdifsn  11260  hashxp  11267  hashmap  11268  sseqn  11279  hashf1lem2  11286  hashf1  11287  hashfac  11288  zfz1isolemsplit  11290  zfz1isolem1  11292  zfz1iso  11293  seq3coll  11294  wrdf  11310  ccatfvalfi  11360  elfzelfzccat  11368  ccatlid  11374  ccatrid  11375  ccatass  11376  ccatalpha  11381  ccatws1leng  11402  ccats1val2  11408  ccatw2s1p1g  11413  swrdval  11420  swrd00g  11421  swrdf  11427  swrdfv2  11435  swrdwrdsymbg  11436  swrdspsleq  11439  swrds1  11440  swrdlsw  11441  ccatswrd  11442  swrdccat2  11443  pfxmpt  11452  pfxfv  11456  pfxeq  11468  pfxsuff1eqwrdeq  11471  ccatpfx  11473  pfxccat1  11474  swrdswrd  11477  pfxswrd  11478  swrdpfx  11479  pfxpfx  11480  pfxlswccat  11485  ccats1pfxeq  11486  ccats1pfxeqrex  11487  ccatopth2  11489  cats1un  11493  wrdind  11494  wrd2ind  11495  swrdccatfn  11496  swrdccatin1  11497  pfxccatin12lem4  11498  swrdccatin2  11501  pfxccatin12lem2c  11502  pfxccatin12lem2  11503  pfxccatin12  11505  swrdccat  11507  swrdccat3blem  11511  swrdccat3b  11512  swrdccatin2d  11516  pfxccatin12d  11517  reuccatpfxs1lem  11518  reuccatpfxs1  11519  shftcan1  11599  shftcan2  11600  cjval  11610  cjth  11611  crre  11622  replim  11624  remim  11625  reim0b  11627  rereb  11628  mulreap  11629  cjreb  11631  recj  11632  reneg  11633  readd  11634  resub  11635  remullem  11636  imcj  11640  imneg  11641  imadd  11642  imsub  11643  cjcj  11648  cjadd  11649  ipcnval  11651  cjmulrcl  11652  cjneg  11655  addcj  11656  cjsub  11657  sq01  11660  cnrecnv  11676  caucvgrelemcau  11746  cvg1nlemcau  11750  cvg1nlemres  11751  recvguniqlem  11760  resqrexlemover  11776  resqrexlemlo  11779  resqrexlemcalc1  11780  resqrexlemcalc3  11782  resqrexlemnm  11784  resqrexlemcvg  11785  absneg  11816  abscj  11818  sqabsadd  11821  sqabssub  11822  absmul  11835  absid  11837  absre  11843  absresq  11844  absexpzap  11846  recvalap  11863  abstri  11870  abs2dif2  11873  recan  11875  cau3lem  11880  amgm2  11884  bdtrilem  12005  xrmaxadd  12027  xrbdtri  12042  climaddc1  12095  climsubc1  12098  climcvg1nlem  12115  serf0  12118  fzf1o  12142  summodclem3  12147  summodclem2a  12148  summodc  12150  fsumsplitsn  12177  fsumm1  12183  fsumsplitsnun  12186  fsump1  12187  isummulc2  12193  fsumrev  12210  fisum0diag2  12214  fsummulc2  12215  fsumsub  12219  fsumabs  12232  telfsumo  12233  fsumparts  12237  fsumrelem  12238  fsumiun  12244  binomlem  12250  binom  12251  binom1p  12252  binom11  12253  binom1dif  12254  bcxmas  12256  isumsplit  12258  isum1p  12259  divcnv  12264  arisum2  12266  trireciplem  12267  trirecip  12268  geolim  12278  georeclim  12280  geo2sum  12281  geo2lim  12283  geoisum1c  12287  0.999...  12288  cvgratnnlemnexp  12291  cvgratnnlemmn  12292  cvgratz  12299  mertenslem2  12303  mertensabs  12304  clim2prod  12306  prodfrecap  12313  prodfdivap  12314  prodmodclem3  12342  prodmodclem2a  12343  fprodm1  12365  fprodp1  12367  fprodunsn  12371  fprodfac  12382  fprodeq0  12384  fprodconst  12387  fprodrec  12396  fproddivap  12397  fprodsplitsn  12400  ege2le3  12438  efaddlem  12441  efsub  12448  efexp  12449  eftlub  12457  efsep  12458  effsumlt  12459  ef4p  12461  tanval3ap  12481  resinval  12482  recosval  12483  efi4p  12484  efival  12499  efmival  12500  efeul  12501  sinadd  12503  cosadd  12504  tanaddap  12506  sinsub  12507  cossub  12508  sincossq  12515  sin2t  12516  cos2t  12517  cos2tsin  12518  ef01bndlem  12523  sin01bnd  12524  cos01bnd  12525  cos12dec  12535  absef  12537  absefib  12538  efieq1re  12539  demoivreALT  12541  eirraplem  12544  dvdsexp  12628  oexpneg  12644  opeo  12664  omeo  12665  m1exp1  12668  flodddiv4  12703  flodddiv4t2lthalf  12706  bitsval  12710  bitsp1  12718  bitsinv1lem  12728  bitsinv1  12729  divgcdnnr  12753  gcdaddm  12761  gcdadd  12762  gcdid  12763  modgcd  12768  gcdmultipled  12770  dvdsgcdidd  12771  bezoutlemnewy  12773  bezoutlema  12776  bezoutlemb  12777  bezoutlemex  12778  bezoutlembz  12781  absmulgcd  12794  gcdmultiple  12797  gcdmultiplez  12798  rpmulgcd  12803  rplpwr  12804  eucalginv  12834  eucalg  12837  lcmneg  12852  lcmgcdlem  12855  lcmgcd  12856  lcmid  12858  lcm1  12859  mulgcddvds  12872  qredeq  12874  divgcdcoprmex  12880  prmind2  12898  rpexp1i  12932  pw2dvdslemn  12943  pw2dvdseulemle  12945  pw2dvdseu  12946  oddpwdclemxy  12947  oddpwdclemdvds  12948  oddpwdclemndvds  12949  oddpwdclemdc  12951  2sqpwodd  12954  nn0gcdsq  12978  phiprmpw  13000  eulerthlemrprm  13007  eulerthlema  13008  eulerthlemh  13009  eulerthlemth  13010  fermltl  13012  prmdiv  13013  hashgcdlem  13016  odzdvds  13024  vfermltl  13030  modprm0  13033  nnnn0modprm0  13034  modprmn0modprm0  13035  coprimeprodsq  13036  pythagtriplem1  13044  pythagtriplem4  13047  pythagtriplem12  13054  pythagtriplem14  13056  pythagtriplem16  13058  pythagtriplem18  13060  pythagtrip  13062  pcpremul  13072  pceu  13074  pczpre  13076  pcdiv  13081  pcqmul  13082  pcqdiv  13086  pcexp  13088  pcxqcl  13091  pczdvds  13093  pczndvds  13095  pczndvds2  13097  pcid  13103  pcneg  13104  pcdvdstr  13106  pcgcd1  13107  pcgcd  13108  pc2dvds  13109  pcaddlem  13118  pcadd  13119  pcadd2  13120  pcmpt  13122  pcmpt2  13123  fldivp1  13127  pcfac  13129  pcbc  13130  expnprm  13132  prmpwdvds  13134  pockthlem  13135  pockthi  13137  4sqlem7  13163  4sqlem9  13165  4sqlem10  13166  4sqlem2  13168  4sqlem3  13169  4sqlem4  13171  mul4sqlem  13172  4sqlem11  13180  4sqlem16  13185  4sqlem17  13186  4sqlem19  13188  ballotfilemfc0  13232  ballotfilemfcc  13233  ballotfilemsv  13253  ballotfilemsima  13259  ballotfilemfrci  13271  setscomd  13393  ressvalsets  13418  strressid  13425  ressval3d  13426  ressinbasd  13428  ressressg  13429  ressabsg  13430  grpinvalem  13705  grpinva  13706  grprida  13707  isnsgrp  13721  sgrpass  13723  sgrp1  13726  sgrppropd  13728  mnd32g  13740  mnd4g  13742  mndpropd  13753  imasmnd2  13759  mhmex  13769  mhmlin  13774  gzsumwmhm  13803  grprcan  13842  grpsubval  13851  grpinvid2  13858  grpasscan2  13869  grpsubinv  13878  grpinvadd  13883  grpsubid1  13890  grpsubadd0sub  13892  grpsubadd  13893  grpsubsub  13894  grpaddsubass  13895  grppncan  13896  grpnnncan2  13902  grpsubpropd2  13910  imasgrp2  13913  mhmlem  13917  mhmid  13918  mhmmnd  13919  ghmgrp  13921  mulgnn0gzsum  13931  mulgnnp1  13933  mulgaddcomlem  13948  mulgaddcom  13949  mulginvinv  13951  mulgnn0dir  13955  mulgdirlem  13956  mulgp1  13958  mulgneg2  13959  mulgnn0ass  13961  mulgass  13962  mulgmodid  13964  mulgsubdir  13965  nmzsubg  14013  0nsg  14017  eqger  14027  qussub  14040  ghmlin  14051  ghmsub  14054  conjghm  14079  ablsub4  14117  abladdsub4  14118  ablsubsub4  14123  ablsub32  14126  ablnnncan  14127  gzsumconst  14143  gzsummhm2  14146  gzsumsnfd  14147  gzsumsplit0  14148  gsumvalfi  14152  gzsumgsum1  14153  gzsumgsum  14155  gsumsncmn  14156  gsump1  14157  gsumzfi  14158  gsumclfi  14159  gsumf1ofi  14160  gsummptfidmadd  14161  gsummptfidmadd2  14162  gsumsubmclfi  14163  gsummhm2fi  14165  gsumconstcmn  14166  prdssgrpd  14191  prdsidlem  14193  prdsmndd  14194  mgpress  14230  rngass  14238  rngdi  14239  rngdir  14240  rngrz  14245  rngmneg2  14247  rngsubdi  14250  rngsubdir  14251  rngpropd  14254  imasrng  14255  srgass  14275  srgpcomp  14294  srgpcompp  14295  srgpcomppsc  14296  srg1expzeq1  14299  ringpropd  14343  ringrz  14349  ringnegr  14357  ringmneg2  14359  ringsubdi  14361  ringsubdir  14362  ring1  14364  imasring  14369  opprrng  14382  opprring  14384  mulgass3  14391  dvdsrd  14401  unitgrp  14423  invrfvald  14429  dvr1  14445  dvrass  14446  dvrcan1  14447  dvrcan3  14448  rdivmuldivd  14451  subrginv  14545  subrgdv  14546  resrhm2b  14557  rrgsupp  14574  islmod  14627  lmodlema  14628  islmodd  14629  lmodvs0  14659  lmodvneg1  14667  lmodvsubval2  14679  lmodsubvs  14680  lmodsubdi  14681  lmodsubdir  14682  lmodprop2d  14685  rmodislmodlem  14687  rmodislmod  14688  lsssn0  14707  sraval  14774  cnfldsub  14912  gsumfsum  14923  mulgrhm  14944  mulgrhm2  14945  znval  14971  znval2  14973  znunit  14994  isassa  15002  assalem  15003  assa2ass2  15010  assapropd  15014  asclmul1  15029  asclmul2  15030  ascldimul  15031  asclpropd  15040  assamulgscmlem2  15042  asclmulg  15044  psrval  15050  mplvalcoe  15081  mplval2g  15086  restabs  15276  cnprcl2k  15307  cnrest2r  15338  ispsmet  15424  psmettri2  15429  psmetsym  15430  ismet  15445  isxmet  15446  xmettri2  15462  xmetsym  15469  xmettri3  15475  mettri3  15476  xblss2ps  15505  xblss2  15506  comet  15600  xmetxp  15608  xmetxpbl  15609  txmetcnp  15619  fsumcncntop  15668  cncfi  15679  divcncfap  15715  limccl  15760  ellimc3apf  15761  limccnpcntop  15776  limccnp2lem  15777  reldvg  15780  dvfvalap  15782  eldvap  15783  dvcj  15810  dvfre  15811  dvexp  15812  dvexp2  15813  dvrecap  15814  dvmptaddx  15820  dvmptmulx  15821  dvmptnegcn  15823  dvmptsubcn  15824  dvmptcjx  15825  dvmptfsum  15826  dveflem  15827  dvef  15828  plyconst  15846  plyaddlem1  15848  plymullem1  15849  plyadd  15852  plymul  15853  plycoeid3  15858  plycolemc  15859  plyco  15860  plycjlemc  15861  plycj  15862  plyrecj  15864  dvply1  15866  dvply2g  15867  sin0pilem1  15882  sin0pilem2  15883  efper  15908  sinperlem  15909  efimpi  15920  ptolemy  15925  tangtx  15939  abssinper  15947  cosq34lt1  15951  rpcxpef  15996  rpcxpp1  16008  rpcxpneg  16009  rpcxpsub  16010  rpmulcxp  16011  rpdivcxp  16013  cxpmul  16014  rpcxpmul2  16015  rpcxproot  16016  cxpcom  16040  rpabscxpbnd  16042  rplogbval  16047  rplogbreexp  16055  rplogbzexp  16056  rprelogbmulexp  16058  rprelogbdiv  16059  relogbexpap  16060  rplogbcxp  16065  rpcxplogb  16066  logbgcd1irr  16069  logbgcd1irraplemap  16071  binom4  16081  log2tlbndlog2  16082  log2ublem2  16084  birthdaylem2  16088  pellexlem2  16092  pellexlem3  16093  wilthlem1  16094  sgmval  16097  sgmppw  16106  1sgmprm  16108  mersenne  16111  perfectlem1  16113  perfectlem2  16114  perfect  16115  lgslem1  16119  lgsval  16123  lgsfvalg  16124  lgsval2lem  16129  lgsval4  16139  lgsneg  16143  lgsneg1  16144  lgsmod  16145  lgsdir2  16152  lgsdirprm  16153  lgsdilem2  16155  lgsdi  16156  lgsne0  16157  lgssq2  16160  lgsdirnn0  16166  lgsdinn0  16167  gausslemma2dlem1a  16177  gausslemma2dlem1f1o  16179  gausslemma2dlem2  16181  gausslemma2dlem3  16182  gausslemma2dlem4  16183  gausslemma2dlem5  16185  gausslemma2dlem6  16186  gausslemma2d  16188  lgseisenlem1  16189  lgseisenlem2  16190  lgseisenlem3  16191  lgseisenlem4  16192  lgsquadlem1  16196  lgsquadlem2  16197  lgsquadlem3  16198  lgsquad2lem1  16200  lgsquad2lem2  16201  lgsquad2  16202  lgsquad3  16203  m1lgs  16204  2lgslem3c  16214  2lgslem3d  16215  2lgslem3d1  16219  2sqlem2  16234  2sqlem3  16236  2sqlem4  16237  2sqlem8  16242  2sqlem9  16243  2sqlem10  16244  vtxdumgrfival  16539  p1evtxdeqfi  16553  p1evtxdp1fi  16554  iswlk  16564  upgr2wlkdc  16618  wlkres  16620  trlreslem  16630  isclwwlk  16635  clwwlkccatlem  16641  clwwlknp  16658  clwwlkn1  16659  clwwlkn2  16662  clwwlkext2edg  16663  clwwlknonex2lem1  16678  clwwlknonex2lem2  16679  clwwlknonex2  16680  iseupth  16688  eupth2lem3lem6fi  16712  eupth2lem3lem4fi  16714  depindlem1  16747  qdencn  17072  trilpolemclim  17085  trilpolemcl  17086  trilpolemisumle  17087  trilpolemeq1  17089  trilpolemlt1  17090  trilpo  17092  apdifflemf  17095  apdiff  17097  iswomni0  17101  redcwlpolemeq1  17104  redcwlpo  17105  nconstwlpolem0  17113  nconstwlpolemgt0  17114  nconstwlpo  17116  neapmkv  17118