Theorem oveq2d 6066

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

Syntax hints:   → wi 4   = wceq 1398  (class class class)co 6050

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 717  ax-5 1496  ax-7 1497  ax-gen 1498  ax-ie1 1542  ax-ie2 1543  ax-8 1553  ax-10 1554  ax-11 1555  ax-i12 1556  ax-bndl 1558  ax-4 1559  ax-17 1575  ax-i9 1579  ax-ial 1583  ax-i5r 1584  ax-ext 2214

This theorem depends on definitions:  df-bi 117  df-3an 1007  df-tru 1401  df-nf 1510  df-sb 1812  df-clab 2219  df-cleq 2225  df-clel 2228  df-nfc 2373  df-rex 2526  df-v 2815  df-un 3215  df-sn 3695  df-pr 3696  df-op 3698  df-uni 3915  df-br 4110  df-iota 5312  df-fv 5360  df-ov 6053

This theorem is referenced by:  csbov1g  6091  caovassg  6213  caovdig  6229  caovdirg  6232  caov32d  6235  caov4d  6239  caov42d  6241  suppofss1dcl  6464  suppofss2dcl  6465  nnaass  6718  nndi  6719  nnmass  6720  nnmsucr  6721  ecovass  6878  ecoviass  6879  ecovdi  6880  ecovidi  6881  addasspig  7645  mulasspig  7647  distrpig  7648  dfplpq2  7669  mulpipq2  7686  addassnqg  7697  prarloclemarch  7733  prarloclemarch2  7734  ltrnqg  7735  enq0sym  7747  addnq0mo  7762  mulnq0mo  7763  addnnnq0  7764  nq0a0  7772  distrnq0  7774  addassnq0  7777  prarloclemlo  7809  prarloclem3  7812  prarloclem5  7815  prarloclemcalc  7817  addnqprl  7844  addnqpru  7845  prmuloclemcalc  7880  mulnqprl  7883  mulnqpru  7884  distrlem4prl  7899  distrlem4pru  7900  1idprl  7905  1idpru  7906  ltexprlemloc  7922  addcanprleml  7929  addcanprlemu  7930  recexprlem1ssu  7949  ltmprr  7957  caucvgprlemcanl  7959  cauappcvgprlemladdru  7971  cauappcvgprlemladdrl  7972  cauappcvgprlem1  7974  cauappcvgprlemlim  7976  caucvgprlemnkj  7981  caucvgprlemnbj  7982  caucvgprlemdisj  7989  caucvgprlemloc  7990  caucvgprlemcl  7991  caucvgprlemladdrl  7993  caucvgprlem1  7994  caucvgpr  7997  caucvgprprlemell  8000  caucvgprprlemcbv  8002  caucvgprprlemval  8003  caucvgprprlemnkeqj  8005  caucvgprprlemopl  8012  caucvgprprlemlol  8013  caucvgprprlemloc  8018  caucvgprprlemclphr  8020  caucvgprprlemexb  8022  caucvgprprlemaddq  8023  caucvgprprlem1  8024  addcmpblnr  8054  mulcmpblnrlemg  8055  addsrmo  8058  mulsrmo  8059  addsrpr  8060  mulsrpr  8061  ltsrprg  8062  recexgt0sr  8088  mulgt0sr  8093  caucvgsrlemgt1  8110  caucvgsrlemoffval  8111  caucvgsr  8117  suplocsrlemb  8121  suplocsrlempr  8122  suplocsrlem  8123  suplocsr  8124  mulcnsr  8150  pitoregt0  8164  recidpirqlemcalc  8172  axmulcom  8186  axmulass  8188  axdistr  8189  ax0id  8193  axcnre  8196  recriota  8205  axcaucvglemcau  8213  axcaucvglemres  8214  mulrid  8271  adddirp1d  8300  mul32  8403  mul31  8404  add32  8432  add4  8434  add42  8435  cnegex  8451  addcan2  8454  addsubass  8483  subsub2  8501  nppcan2  8504  sub32  8507  nnncan  8508  sub4  8518  muladd  8657  subdi  8658  mul2neg  8671  submul2  8672  mulsub  8674  muls1d  8691  mulsubfacd  8692  add20  8748  recexre  8852  rereim  8860  apreap  8861  ltmul1  8866  cru  8876  apreim  8877  mulreim  8878  apadd1  8882  apneg  8885  mulap0  8928  divrecap  8962  divassap  8964  divmulasscomap  8970  divsubdirap  8982  divdivdivap  8987  divmul24ap  8990  divmuleqap  8991  divcanap6  8993  divdivap1  8997  divdivap2  8998  divsubdivap  9002  conjmulap  9003  div2negap  9009  apmul1  9062  cju  9235  nnmulcl  9258  add1p1  9488  sub1m1  9489  cnm2m1cnm3  9490  xp1d2m1eqxm1d2  9491  div4p1lem1div2  9492  un0addcl  9529  un0mulcl  9530  zaddcllemneg  9616  qapne  9971  cnref1o  9983  rexsub  10186  xnegid  10192  xaddcom  10194  xnegdi  10201  xaddass  10202  xaddass2  10203  xpncan  10204  xnpcan  10205  xleadd1a  10206  xsubge0  10214  xposdif  10215  xlesubadd  10216  xadd4d  10218  lincmb01cmp  10336  iccf1o  10338  ige3m2fz  10383  fztp  10412  fzsuc2  10413  fseq1m1p1  10429  fzm1  10434  ige2m1fz1  10443  nn0split  10470  nnsplit  10471  fzo0addelr  10534  elfzoext  10537  fzval3  10549  zpnn0elfzo1  10553  fzosplitsnm1  10554  fzosplitpr  10579  fzosplitprm1  10580  fzoshftral  10584  rebtwn2zlemstep  10612  flhalf  10662  fldiv4lem1div2uz2  10666  modqval  10686  modqvalr  10687  modqdiffl  10697  modqfrac  10699  flqmod  10700  intqfrac  10701  zmod10  10702  modqmulnn  10704  modqvalp1  10705  modqid  10711  modqcyc  10721  modqcyc2  10722  modqmul1  10739  q2submod  10747  modqdi  10754  modqsubdir  10755  modqeqmodmin  10756  modsumfzodifsn  10758  addmodlteq  10760  frecuzrdgsuctlem  10785  uzsinds  10806  seqeq3  10814  iseqvalcbv  10821  seq3val  10822  seqvalcd  10823  seqf  10826  seq3p1  10827  seqovcd  10829  seqp1cd  10832  seq3m1  10835  seq3fveq2  10837  seqfveq2g  10839  seq3shft2  10843  seqshft2g  10844  monoord2  10848  ser3mono  10849  seq3split  10850  seqsplitg  10851  seq3caopr3  10853  seqcaopr3g  10854  seq3caopr2  10855  seqcaopr2g  10856  seq3caopr  10857  seqcaoprg  10858  seqf1oglem2a  10880  seqf1oglem2  10882  seq3id2  10888  seq3homo  10889  seq3z  10890  seqhomog  10892  exp3vallem  10902  exp3val  10903  expp1  10908  expnegap0  10909  expineg2  10910  expn1ap0  10911  expm1t  10929  1exp  10930  expnegzap  10935  mulexpzap  10941  expadd  10943  expaddzaplem  10944  expaddzap  10945  expmul  10946  expmulzap  10947  m1expeven  10948  expsubap  10949  expp1zap  10950  expm1ap  10951  expdivap  10952  iexpcyc  11006  subsq2  11009  binom2  11013  binom21  11014  binom2sub  11015  binom2sub1  11016  mulbinom2  11018  binom3  11019  zesq  11020  bernneq  11022  sqoddm1div8  11055  mulsubdivbinom2ap  11073  nn0opthlem1d  11082  nn0opthd  11084  facp1  11092  facnn2  11096  faclbnd  11103  faclbnd6  11106  bcval  11111  bccmpl  11116  bcn0  11117  bcnn  11119  bcnp1n  11121  bcm1k  11122  bcp1n  11123  bcp1nk  11124  bcval5  11125  bcp1m1  11127  bcpasc  11128  bcm1n  11131  bcn2m1  11132  bcn2p1  11133  omgadd  11166  hashunlem  11168  hashunsng  11172  hashdifsn  11184  hashxp  11191  hashmap  11192  sseqn  11203  zfz1isolemsplit  11210  zfz1isolem1  11212  zfz1iso  11213  seq3coll  11214  wrdf  11230  ccatfvalfi  11280  elfzelfzccat  11288  ccatlid  11294  ccatrid  11295  ccatass  11296  ccatalpha  11301  ccatws1leng  11322  ccats1val2  11328  ccatw2s1p1g  11333  swrdval  11340  swrd00g  11341  swrdf  11347  swrdfv2  11355  swrdwrdsymbg  11356  swrdspsleq  11359  swrds1  11360  swrdlsw  11361  ccatswrd  11362  swrdccat2  11363  pfxmpt  11372  pfxfv  11376  pfxeq  11388  pfxsuff1eqwrdeq  11391  ccatpfx  11393  pfxccat1  11394  swrdswrd  11397  pfxswrd  11398  swrdpfx  11399  pfxpfx  11400  pfxlswccat  11405  ccats1pfxeq  11406  ccats1pfxeqrex  11407  ccatopth2  11409  cats1un  11413  wrdind  11414  wrd2ind  11415  swrdccatfn  11416  swrdccatin1  11417  pfxccatin12lem4  11418  swrdccatin2  11421  pfxccatin12lem2c  11422  pfxccatin12lem2  11423  pfxccatin12  11425  swrdccat  11427  swrdccat3blem  11431  swrdccat3b  11432  swrdccatin2d  11436  pfxccatin12d  11437  reuccatpfxs1lem  11438  reuccatpfxs1  11439  shftcan1  11519  shftcan2  11520  cjval  11530  cjth  11531  crre  11542  replim  11544  remim  11545  reim0b  11547  rereb  11548  mulreap  11549  cjreb  11551  recj  11552  reneg  11553  readd  11554  resub  11555  remullem  11556  imcj  11560  imneg  11561  imadd  11562  imsub  11563  cjcj  11568  cjadd  11569  ipcnval  11571  cjmulrcl  11572  cjneg  11575  addcj  11576  cjsub  11577  cnrecnv  11595  caucvgrelemcau  11665  cvg1nlemcau  11669  cvg1nlemres  11670  recvguniqlem  11679  resqrexlemover  11695  resqrexlemlo  11698  resqrexlemcalc1  11699  resqrexlemcalc3  11701  resqrexlemnm  11703  resqrexlemcvg  11704  absneg  11735  abscj  11737  sqabsadd  11740  sqabssub  11741  absmul  11754  absid  11756  absre  11762  absresq  11763  absexpzap  11765  recvalap  11782  abstri  11789  abs2dif2  11792  recan  11794  cau3lem  11799  amgm2  11803  bdtrilem  11924  xrmaxadd  11946  xrbdtri  11961  climaddc1  12014  climsubc1  12017  climcvg1nlem  12034  serf0  12037  fzf1o  12061  summodclem3  12066  summodclem2a  12067  summodc  12069  fsumsplitsn  12096  fsumm1  12102  fsumsplitsnun  12105  fsump1  12106  isummulc2  12112  fsumrev  12129  fisum0diag2  12133  fsummulc2  12134  fsumsub  12138  fsumabs  12151  telfsumo  12152  fsumparts  12156  fsumrelem  12157  fsumiun  12163  binomlem  12169  binom  12170  binom1p  12171  binom11  12172  binom1dif  12173  bcxmas  12175  isumsplit  12177  isum1p  12178  divcnv  12183  arisum2  12185  trireciplem  12186  trirecip  12187  geolim  12197  georeclim  12199  geo2sum  12200  geo2lim  12202  geoisum1c  12206  0.999...  12207  cvgratnnlemnexp  12210  cvgratnnlemmn  12211  cvgratz  12218  mertenslem2  12222  mertensabs  12223  clim2prod  12225  prodfrecap  12232  prodfdivap  12233  prodmodclem3  12261  prodmodclem2a  12262  fprodm1  12284  fprodp1  12286  fprodunsn  12290  fprodfac  12301  fprodeq0  12303  fprodconst  12306  fprodrec  12315  fproddivap  12316  fprodsplitsn  12319  ege2le3  12357  efaddlem  12360  efsub  12367  efexp  12368  eftlub  12376  efsep  12377  effsumlt  12378  ef4p  12380  tanval3ap  12400  resinval  12401  recosval  12402  efi4p  12403  efival  12418  efmival  12419  efeul  12420  sinadd  12422  cosadd  12423  tanaddap  12425  sinsub  12426  cossub  12427  sincossq  12434  sin2t  12435  cos2t  12436  cos2tsin  12437  ef01bndlem  12442  sin01bnd  12443  cos01bnd  12444  cos12dec  12454  absef  12456  absefib  12457  efieq1re  12458  demoivreALT  12460  eirraplem  12463  dvdsexp  12547  oexpneg  12563  opeo  12583  omeo  12584  m1exp1  12587  flodddiv4  12622  flodddiv4t2lthalf  12625  bitsval  12629  bitsp1  12637  bitsinv1lem  12647  bitsinv1  12648  divgcdnnr  12672  gcdaddm  12680  gcdadd  12681  gcdid  12682  modgcd  12687  gcdmultipled  12689  dvdsgcdidd  12690  bezoutlemnewy  12692  bezoutlema  12695  bezoutlemb  12696  bezoutlemex  12697  bezoutlembz  12700  absmulgcd  12713  gcdmultiple  12716  gcdmultiplez  12717  rpmulgcd  12722  rplpwr  12723  eucalginv  12753  eucalg  12756  lcmneg  12771  lcmgcdlem  12774  lcmgcd  12775  lcmid  12777  lcm1  12778  mulgcddvds  12791  qredeq  12793  divgcdcoprmex  12799  prmind2  12817  rpexp1i  12851  pw2dvdslemn  12862  pw2dvdseulemle  12864  pw2dvdseu  12865  oddpwdclemxy  12866  oddpwdclemdvds  12867  oddpwdclemndvds  12868  oddpwdclemdc  12870  2sqpwodd  12873  nn0gcdsq  12897  phiprmpw  12919  eulerthlemrprm  12926  eulerthlema  12927  eulerthlemh  12928  eulerthlemth  12929  fermltl  12931  prmdiv  12932  hashgcdlem  12935  odzdvds  12943  vfermltl  12949  modprm0  12952  nnnn0modprm0  12953  modprmn0modprm0  12954  coprimeprodsq  12955  pythagtriplem1  12963  pythagtriplem4  12966  pythagtriplem12  12973  pythagtriplem14  12975  pythagtriplem16  12977  pythagtriplem18  12979  pythagtrip  12981  pcpremul  12991  pceu  12993  pczpre  12995  pcdiv  13000  pcqmul  13001  pcqdiv  13005  pcexp  13007  pcxqcl  13010  pczdvds  13012  pczndvds  13014  pczndvds2  13016  pcid  13022  pcneg  13023  pcdvdstr  13025  pcgcd1  13026  pcgcd  13027  pc2dvds  13028  pcaddlem  13037  pcadd  13038  pcadd2  13039  pcmpt  13041  pcmpt2  13042  fldivp1  13046  pcfac  13048  pcbc  13049  expnprm  13051  prmpwdvds  13053  pockthlem  13054  pockthi  13056  4sqlem7  13082  4sqlem9  13084  4sqlem10  13085  4sqlem2  13087  4sqlem3  13088  4sqlem4  13090  mul4sqlem  13091  4sqlem11  13099  4sqlem16  13104  4sqlem17  13105  4sqlem19  13107  setscomd  13253  ressvalsets  13277  strressid  13284  ressval3d  13285  ressinbasd  13287  ressressg  13288  ressabsg  13289  grpinvalem  13598  grpinva  13599  grprida  13600  isnsgrp  13619  sgrpass  13621  sgrp1  13624  sgrppropd  13626  prdssgrpd  13628  mnd32g  13640  mnd4g  13642  mndpropd  13653  prdsidlem  13660  prdsmndd  13661  imasmnd2  13665  mhmex  13675  mhmlin  13680  gsumwmhm  13711  grprcan  13750  grpsubval  13759  grpinvid2  13766  grpasscan2  13777  grpsubinv  13786  grpinvadd  13791  grpsubid1  13798  grpsubadd0sub  13800  grpsubadd  13801  grpsubsub  13802  grpaddsubass  13803  grppncan  13804  grpnnncan2  13810  grpsubpropd2  13818  imasgrp2  13827  mhmlem  13831  mhmid  13832  mhmmnd  13833  ghmgrp  13835  mulgnn0gsum  13845  mulgnnp1  13847  mulgaddcomlem  13862  mulgaddcom  13863  mulginvinv  13865  mulgnn0dir  13869  mulgdirlem  13870  mulgp1  13872  mulgneg2  13873  mulgnn0ass  13875  mulgass  13876  mulgmodid  13878  mulgsubdir  13879  nmzsubg  13927  0nsg  13931  eqger  13941  qussub  13954  ghmlin  13965  ghmsub  13968  conjghm  13993  ablsub4  14030  abladdsub4  14031  ablsubsub4  14036  ablsub32  14039  ablnnncan  14040  gsumfzmptfidmadd2  14057  gsumfzconst  14058  gsumfzmhm2  14061  gsumfzsnfd  14062  gsumsplit0  14063  mgpress  14075  rngass  14083  rngdi  14084  rngdir  14085  rngrz  14090  rngmneg2  14092  rngsubdi  14095  rngsubdir  14096  rngpropd  14099  imasrng  14100  srgass  14115  srgpcomp  14134  srgpcompp  14135  srgpcomppsc  14136  srg1expzeq1  14139  ringpropd  14182  ringrz  14188  ringnegr  14196  ringmneg2  14198  ringsubdi  14200  ringsubdir  14201  ring1  14203  imasring  14208  opprrng  14221  opprring  14223  mulgass3  14229  dvdsrd  14239  unitgrp  14261  invrfvald  14267  dvr1  14283  dvrass  14284  dvrcan1  14285  dvrcan3  14286  rdivmuldivd  14289  subrginv  14382  subrgdv  14383  resrhm2b  14394  rrgsupp  14411  islmod  14439  lmodlema  14440  islmodd  14441  lmodvs0  14470  lmodvneg1  14478  lmodvsubval2  14490  lmodsubvs  14491  lmodsubdi  14492  lmodsubdir  14493  lmodprop2d  14496  rmodislmodlem  14498  rmodislmod  14499  lsssn0  14518  sraval  14585  cnfldsub  14723  gsumfzfsumlem0  14734  gsumfzfsumlemm  14735  mulgrhm  14757  mulgrhm2  14758  znval  14784  znval2  14786  znunit  14807  psrval  14814  mplvalcoe  14845  mplval2g  14850  restabs  15040  cnprcl2k  15071  cnrest2r  15102  ispsmet  15188  psmettri2  15193  psmetsym  15194  ismet  15209  isxmet  15210  xmettri2  15226  xmetsym  15233  xmettri3  15239  mettri3  15240  xblss2ps  15269  xblss2  15270  comet  15364  xmetxp  15372  xmetxpbl  15373  txmetcnp  15383  fsumcncntop  15432  cncfi  15443  divcncfap  15479  limccl  15524  ellimc3apf  15525  limccnpcntop  15540  limccnp2lem  15541  reldvg  15544  dvfvalap  15546  eldvap  15547  dvcj  15574  dvfre  15575  dvexp  15576  dvexp2  15577  dvrecap  15578  dvmptaddx  15584  dvmptmulx  15585  dvmptnegcn  15587  dvmptsubcn  15588  dvmptcjx  15589  dvmptfsum  15590  dveflem  15591  dvef  15592  plyconst  15610  plyaddlem1  15612  plymullem1  15613  plyadd  15616  plymul  15617  plycoeid3  15622  plycolemc  15623  plyco  15624  plycjlemc  15625  plycj  15626  plyrecj  15628  dvply1  15630  dvply2g  15631  sin0pilem1  15646  sin0pilem2  15647  efper  15672  sinperlem  15673  efimpi  15684  ptolemy  15689  tangtx  15703  abssinper  15711  cosq34lt1  15715  rpcxpef  15759  rpcxpp1  15771  rpcxpneg  15772  rpcxpsub  15773  rpmulcxp  15774  rpdivcxp  15776  cxpmul  15777  rpcxpmul2  15778  rpcxproot  15779  cxpcom  15803  rpabscxpbnd  15805  rplogbval  15810  rplogbreexp  15818  rplogbzexp  15819  rprelogbmulexp  15821  rprelogbdiv  15822  relogbexpap  15823  rplogbcxp  15828  rpcxplogb  15829  logbgcd1irr  15832  logbgcd1irraplemap  15834  binom4  15844  pellexlem2  15846  pellexlem3  15847  wilthlem1  15848  sgmval  15851  sgmppw  15860  1sgmprm  15862  mersenne  15865  perfectlem1  15867  perfectlem2  15868  perfect  15869  lgslem1  15873  lgsval  15877  lgsfvalg  15878  lgsval2lem  15883  lgsval4  15893  lgsneg  15897  lgsneg1  15898  lgsmod  15899  lgsdir2  15906  lgsdirprm  15907  lgsdilem2  15909  lgsdi  15910  lgsne0  15911  lgssq2  15914  lgsdirnn0  15920  lgsdinn0  15921  gausslemma2dlem1a  15931  gausslemma2dlem1f1o  15933  gausslemma2dlem2  15935  gausslemma2dlem3  15936  gausslemma2dlem4  15937  gausslemma2dlem5  15939  gausslemma2dlem6  15940  gausslemma2d  15942  lgseisenlem1  15943  lgseisenlem2  15944  lgseisenlem3  15945  lgseisenlem4  15946  lgsquadlem1  15950  lgsquadlem2  15951  lgsquadlem3  15952  lgsquad2lem1  15954  lgsquad2lem2  15955  lgsquad2  15956  lgsquad3  15957  m1lgs  15958  2lgslem3c  15968  2lgslem3d  15969  2lgslem3d1  15973  2sqlem2  15988  2sqlem3  15990  2sqlem4  15991  2sqlem8  15996  2sqlem9  15997  2sqlem10  15998  vtxdumgrfival  16293  p1evtxdeqfi  16307  p1evtxdp1fi  16308  iswlk  16318  upgr2wlkdc  16372  wlkres  16374  trlreslem  16384  isclwwlk  16389  clwwlkccatlem  16395  clwwlknp  16412  clwwlkn1  16413  clwwlkn2  16416  clwwlkext2edg  16417  clwwlknonex2lem1  16432  clwwlknonex2lem2  16433  clwwlknonex2  16434  iseupth  16442  eupth2lem3lem6fi  16466  eupth2lem3lem4fi  16468  depindlem1  16501  qdencn  16807  trilpolemclim  16820  trilpolemcl  16821  trilpolemisumle  16822  trilpolemeq1  16824  trilpolemlt1  16825  trilpo  16827  apdifflemf  16830  apdiff  16832  iswomni0  16836  redcwlpolemeq1  16839  redcwlpo  16840  nconstwlpolem0  16849  nconstwlpolemgt0  16850  nconstwlpo  16852  neapmkv  16854  gfsumval  16862  gsumgfsum1  16863  gsumgfsum  16866  gfsumsn  16867  gfsump1  16868  gfsumz  16869  gfsumcl  16870