Theorem oveq2d 6016

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

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

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 3888  df-br 4083  df-iota 5277  df-fv 5325  df-ov 6003

This theorem is referenced by:  csbov1g  6041  caovassg  6163  caovdig  6179  caovdirg  6182  caov32d  6185  caov4d  6189  caov42d  6191  nnaass  6629  nndi  6630  nnmass  6631  nnmsucr  6632  ecovass  6789  ecoviass  6790  ecovdi  6791  ecovidi  6792  addasspig  7513  mulasspig  7515  distrpig  7516  dfplpq2  7537  mulpipq2  7554  addassnqg  7565  prarloclemarch  7601  prarloclemarch2  7602  ltrnqg  7603  enq0sym  7615  addnq0mo  7630  mulnq0mo  7631  addnnnq0  7632  nq0a0  7640  distrnq0  7642  addassnq0  7645  prarloclemlo  7677  prarloclem3  7680  prarloclem5  7683  prarloclemcalc  7685  addnqprl  7712  addnqpru  7713  prmuloclemcalc  7748  mulnqprl  7751  mulnqpru  7752  distrlem4prl  7767  distrlem4pru  7768  1idprl  7773  1idpru  7774  ltexprlemloc  7790  addcanprleml  7797  addcanprlemu  7798  recexprlem1ssu  7817  ltmprr  7825  caucvgprlemcanl  7827  cauappcvgprlemladdru  7839  cauappcvgprlemladdrl  7840  cauappcvgprlem1  7842  cauappcvgprlemlim  7844  caucvgprlemnkj  7849  caucvgprlemnbj  7850  caucvgprlemdisj  7857  caucvgprlemloc  7858  caucvgprlemcl  7859  caucvgprlemladdrl  7861  caucvgprlem1  7862  caucvgpr  7865  caucvgprprlemell  7868  caucvgprprlemcbv  7870  caucvgprprlemval  7871  caucvgprprlemnkeqj  7873  caucvgprprlemopl  7880  caucvgprprlemlol  7881  caucvgprprlemloc  7886  caucvgprprlemclphr  7888  caucvgprprlemexb  7890  caucvgprprlemaddq  7891  caucvgprprlem1  7892  addcmpblnr  7922  mulcmpblnrlemg  7923  addsrmo  7926  mulsrmo  7927  addsrpr  7928  mulsrpr  7929  ltsrprg  7930  recexgt0sr  7956  mulgt0sr  7961  caucvgsrlemgt1  7978  caucvgsrlemoffval  7979  caucvgsr  7985  suplocsrlemb  7989  suplocsrlempr  7990  suplocsrlem  7991  suplocsr  7992  mulcnsr  8018  pitoregt0  8032  recidpirqlemcalc  8040  axmulcom  8054  axmulass  8056  axdistr  8057  ax0id  8061  axcnre  8064  recriota  8073  axcaucvglemcau  8081  axcaucvglemres  8082  mulrid  8139  adddirp1d  8169  mul32  8272  mul31  8273  add32  8301  add4  8303  add42  8304  cnegex  8320  addcan2  8323  addsubass  8352  subsub2  8370  nppcan2  8373  sub32  8376  nnncan  8377  sub4  8387  muladd  8526  subdi  8527  mul2neg  8540  submul2  8541  mulsub  8543  muls1d  8560  mulsubfacd  8561  add20  8617  recexre  8721  rereim  8729  apreap  8730  ltmul1  8735  cru  8745  apreim  8746  mulreim  8747  apadd1  8751  apneg  8754  mulap0  8797  divrecap  8831  divassap  8833  divmulasscomap  8839  divsubdirap  8851  divdivdivap  8856  divmul24ap  8859  divmuleqap  8860  divcanap6  8862  divdivap1  8866  divdivap2  8867  divsubdivap  8871  conjmulap  8872  div2negap  8878  apmul1  8931  cju  9104  nnmulcl  9127  add1p1  9357  sub1m1  9358  cnm2m1cnm3  9359  xp1d2m1eqxm1d2  9360  div4p1lem1div2  9361  un0addcl  9398  un0mulcl  9399  zaddcllemneg  9481  qapne  9830  cnref1o  9842  rexsub  10045  xnegid  10051  xaddcom  10053  xnegdi  10060  xaddass  10061  xaddass2  10062  xpncan  10063  xnpcan  10064  xleadd1a  10065  xsubge0  10073  xposdif  10074  xlesubadd  10075  xadd4d  10077  lincmb01cmp  10195  iccf1o  10196  ige3m2fz  10241  fztp  10270  fzsuc2  10271  fseq1m1p1  10287  fzm1  10292  ige2m1fz1  10301  nn0split  10328  nnsplit  10329  fzo0addelr  10390  elfzoext  10393  fzval3  10405  zpnn0elfzo1  10409  fzosplitsnm1  10410  fzosplitprm1  10435  fzoshftral  10439  rebtwn2zlemstep  10467  flhalf  10517  fldiv4lem1div2uz2  10521  modqval  10541  modqvalr  10542  modqdiffl  10552  modqfrac  10554  flqmod  10555  intqfrac  10556  zmod10  10557  modqmulnn  10559  modqvalp1  10560  modqid  10566  modqcyc  10576  modqcyc2  10577  modqmul1  10594  q2submod  10602  modqdi  10609  modqsubdir  10610  modqeqmodmin  10611  modsumfzodifsn  10613  addmodlteq  10615  frecuzrdgsuctlem  10640  uzsinds  10661  seqeq3  10669  iseqvalcbv  10676  seq3val  10677  seqvalcd  10678  seqf  10681  seq3p1  10682  seqovcd  10684  seqp1cd  10687  seq3m1  10690  seq3fveq2  10692  seqfveq2g  10694  seq3shft2  10698  seqshft2g  10699  monoord2  10703  ser3mono  10704  seq3split  10705  seqsplitg  10706  seq3caopr3  10708  seqcaopr3g  10709  seq3caopr2  10710  seqcaopr2g  10711  seq3caopr  10712  seqcaoprg  10713  seqf1oglem2a  10735  seqf1oglem2  10737  seq3id2  10743  seq3homo  10744  seq3z  10745  seqhomog  10747  exp3vallem  10757  exp3val  10758  expp1  10763  expnegap0  10764  expineg2  10765  expn1ap0  10766  expm1t  10784  1exp  10785  expnegzap  10790  mulexpzap  10796  expadd  10798  expaddzaplem  10799  expaddzap  10800  expmul  10801  expmulzap  10802  m1expeven  10803  expsubap  10804  expp1zap  10805  expm1ap  10806  expdivap  10807  iexpcyc  10861  subsq2  10864  binom2  10868  binom21  10869  binom2sub  10870  binom2sub1  10871  mulbinom2  10873  binom3  10874  zesq  10875  bernneq  10877  sqoddm1div8  10910  mulsubdivbinom2ap  10928  nn0opthlem1d  10937  nn0opthd  10939  facp1  10947  facnn2  10951  faclbnd  10958  faclbnd6  10961  bcval  10966  bccmpl  10971  bcn0  10972  bcnn  10974  bcnp1n  10976  bcm1k  10977  bcp1n  10978  bcp1nk  10979  bcval5  10980  bcp1m1  10982  bcpasc  10983  bcn2m1  10986  bcn2p1  10987  omgadd  11019  hashunlem  11021  hashunsng  11024  hashdifsn  11036  hashxp  11043  zfz1isolemsplit  11055  zfz1isolem1  11057  zfz1iso  11058  seq3coll  11059  wrdf  11072  ccatfvalfi  11122  elfzelfzccat  11130  ccatlid  11136  ccatrid  11137  ccatass  11138  ccatws1leng  11162  ccats1val2  11166  swrdval  11175  swrd00g  11176  swrdf  11182  swrdfv2  11190  swrdwrdsymbg  11191  swrdspsleq  11194  swrds1  11195  swrdlsw  11196  ccatswrd  11197  swrdccat2  11198  pfxmpt  11207  pfxfv  11211  pfxeq  11223  pfxsuff1eqwrdeq  11226  ccatpfx  11228  pfxccat1  11229  swrdswrd  11232  pfxswrd  11233  swrdpfx  11234  pfxpfx  11235  pfxlswccat  11240  ccats1pfxeq  11241  ccats1pfxeqrex  11242  ccatopth2  11244  cats1un  11248  wrdind  11249  wrd2ind  11250  swrdccatfn  11251  swrdccatin1  11252  pfxccatin12lem4  11253  swrdccatin2  11256  pfxccatin12lem2c  11257  pfxccatin12lem2  11258  pfxccatin12  11260  swrdccat  11262  swrdccat3blem  11266  swrdccat3b  11267  swrdccatin2d  11271  pfxccatin12d  11272  reuccatpfxs1lem  11273  reuccatpfxs1  11274  shftcan1  11340  shftcan2  11341  cjval  11351  cjth  11352  crre  11363  replim  11365  remim  11366  reim0b  11368  rereb  11369  mulreap  11370  cjreb  11372  recj  11373  reneg  11374  readd  11375  resub  11376  remullem  11377  imcj  11381  imneg  11382  imadd  11383  imsub  11384  cjcj  11389  cjadd  11390  ipcnval  11392  cjmulrcl  11393  cjneg  11396  addcj  11397  cjsub  11398  cnrecnv  11416  caucvgrelemcau  11486  cvg1nlemcau  11490  cvg1nlemres  11491  recvguniqlem  11500  resqrexlemover  11516  resqrexlemlo  11519  resqrexlemcalc1  11520  resqrexlemcalc3  11522  resqrexlemnm  11524  resqrexlemcvg  11525  absneg  11556  abscj  11558  sqabsadd  11561  sqabssub  11562  absmul  11575  absid  11577  absre  11583  absresq  11584  absexpzap  11586  recvalap  11603  abstri  11610  abs2dif2  11613  recan  11615  cau3lem  11620  amgm2  11624  bdtrilem  11745  xrmaxadd  11767  xrbdtri  11782  climaddc1  11835  climsubc1  11838  climcvg1nlem  11855  serf0  11858  summodclem3  11886  summodclem2a  11887  summodc  11889  fsumsplitsn  11916  fsumm1  11922  fsumsplitsnun  11925  fsump1  11926  isummulc2  11932  fsumrev  11949  fisum0diag2  11953  fsummulc2  11954  fsumsub  11958  fsumabs  11971  telfsumo  11972  fsumparts  11976  fsumrelem  11977  fsumiun  11983  binomlem  11989  binom  11990  binom1p  11991  binom11  11992  binom1dif  11993  bcxmas  11995  isumsplit  11997  isum1p  11998  divcnv  12003  arisum2  12005  trireciplem  12006  trirecip  12007  geolim  12017  georeclim  12019  geo2sum  12020  geo2lim  12022  geoisum1c  12026  0.999...  12027  cvgratnnlemnexp  12030  cvgratnnlemmn  12031  cvgratz  12038  mertenslem2  12042  mertensabs  12043  clim2prod  12045  prodfrecap  12052  prodfdivap  12053  prodmodclem3  12081  prodmodclem2a  12082  fprodm1  12104  fprodp1  12106  fprodunsn  12110  fprodfac  12121  fprodeq0  12123  fprodconst  12126  fprodrec  12135  fproddivap  12136  fprodsplitsn  12139  ege2le3  12177  efaddlem  12180  efsub  12187  efexp  12188  eftlub  12196  efsep  12197  effsumlt  12198  ef4p  12200  tanval3ap  12220  resinval  12221  recosval  12222  efi4p  12223  efival  12238  efmival  12239  efeul  12240  sinadd  12242  cosadd  12243  tanaddap  12245  sinsub  12246  cossub  12247  sincossq  12254  sin2t  12255  cos2t  12256  cos2tsin  12257  ef01bndlem  12262  sin01bnd  12263  cos01bnd  12264  cos12dec  12274  absef  12276  absefib  12277  efieq1re  12278  demoivreALT  12280  eirraplem  12283  dvdsexp  12367  oexpneg  12383  opeo  12403  omeo  12404  m1exp1  12407  flodddiv4  12442  flodddiv4t2lthalf  12445  bitsval  12449  bitsp1  12457  bitsinv1lem  12467  bitsinv1  12468  divgcdnnr  12492  gcdaddm  12500  gcdadd  12501  gcdid  12502  modgcd  12507  gcdmultipled  12509  dvdsgcdidd  12510  bezoutlemnewy  12512  bezoutlema  12515  bezoutlemb  12516  bezoutlemex  12517  bezoutlembz  12520  absmulgcd  12533  gcdmultiple  12536  gcdmultiplez  12537  rpmulgcd  12542  rplpwr  12543  eucalginv  12573  eucalg  12576  lcmneg  12591  lcmgcdlem  12594  lcmgcd  12595  lcmid  12597  lcm1  12598  mulgcddvds  12611  qredeq  12613  divgcdcoprmex  12619  prmind2  12637  rpexp1i  12671  pw2dvdslemn  12682  pw2dvdseulemle  12684  pw2dvdseu  12685  oddpwdclemxy  12686  oddpwdclemdvds  12687  oddpwdclemndvds  12688  oddpwdclemdc  12690  2sqpwodd  12693  nn0gcdsq  12717  phiprmpw  12739  eulerthlemrprm  12746  eulerthlema  12747  eulerthlemh  12748  eulerthlemth  12749  fermltl  12751  prmdiv  12752  hashgcdlem  12755  odzdvds  12763  vfermltl  12769  modprm0  12772  nnnn0modprm0  12773  modprmn0modprm0  12774  coprimeprodsq  12775  pythagtriplem1  12783  pythagtriplem4  12786  pythagtriplem12  12793  pythagtriplem14  12795  pythagtriplem16  12797  pythagtriplem18  12799  pythagtrip  12801  pcpremul  12811  pceu  12813  pczpre  12815  pcdiv  12820  pcqmul  12821  pcqdiv  12825  pcexp  12827  pcxqcl  12830  pczdvds  12832  pczndvds  12834  pczndvds2  12836  pcid  12842  pcneg  12843  pcdvdstr  12845  pcgcd1  12846  pcgcd  12847  pc2dvds  12848  pcaddlem  12857  pcadd  12858  pcadd2  12859  pcmpt  12861  pcmpt2  12862  fldivp1  12866  pcfac  12868  pcbc  12869  expnprm  12871  prmpwdvds  12873  pockthlem  12874  pockthi  12876  4sqlem7  12902  4sqlem9  12904  4sqlem10  12905  4sqlem2  12907  4sqlem3  12908  4sqlem4  12910  mul4sqlem  12911  4sqlem11  12919  4sqlem16  12924  4sqlem17  12925  4sqlem19  12927  setscomd  13068  ressvalsets  13092  strressid  13099  ressval3d  13100  ressinbasd  13102  ressressg  13103  ressabsg  13104  grpinvalem  13413  grpinva  13414  grprida  13415  isnsgrp  13434  sgrpass  13436  sgrp1  13439  sgrppropd  13441  prdssgrpd  13443  mnd32g  13455  mnd4g  13457  mndpropd  13468  prdsidlem  13475  prdsmndd  13476  imasmnd2  13480  mhmex  13490  mhmlin  13495  gsumwmhm  13526  grprcan  13565  grpsubval  13574  grpinvid2  13581  grpasscan2  13592  grpsubinv  13601  grpinvadd  13606  grpsubid1  13613  grpsubadd0sub  13615  grpsubadd  13616  grpsubsub  13617  grpaddsubass  13618  grppncan  13619  grpnnncan2  13625  grpsubpropd2  13633  imasgrp2  13642  mhmlem  13646  mhmid  13647  mhmmnd  13648  ghmgrp  13650  mulgnn0gsum  13660  mulgnnp1  13662  mulgaddcomlem  13677  mulgaddcom  13678  mulginvinv  13680  mulgnn0dir  13684  mulgdirlem  13685  mulgp1  13687  mulgneg2  13688  mulgnn0ass  13690  mulgass  13691  mulgmodid  13693  mulgsubdir  13694  nmzsubg  13742  0nsg  13746  eqger  13756  qussub  13769  ghmlin  13780  ghmsub  13783  conjghm  13808  ablsub4  13845  abladdsub4  13846  ablsubsub4  13851  ablsub32  13854  ablnnncan  13855  gsumfzmptfidmadd2  13872  gsumfzconst  13873  gsumfzmhm2  13876  gsumfzsnfd  13877  mgpress  13889  rngass  13897  rngdi  13898  rngdir  13899  rngrz  13904  rngmneg2  13906  rngsubdi  13909  rngsubdir  13910  rngpropd  13913  imasrng  13914  srgass  13929  srgpcomp  13948  srgpcompp  13949  srgpcomppsc  13950  srg1expzeq1  13953  ringpropd  13996  ringrz  14002  ringnegr  14010  ringmneg2  14012  ringsubdi  14014  ringsubdir  14015  ring1  14017  imasring  14022  opprrng  14035  opprring  14037  mulgass3  14043  dvdsrd  14052  unitgrp  14074  invrfvald  14080  dvr1  14096  dvrass  14097  dvrcan1  14098  dvrcan3  14099  rdivmuldivd  14102  subrginv  14195  subrgdv  14196  resrhm2b  14207  islmod  14249  lmodlema  14250  islmodd  14251  lmodvs0  14280  lmodvneg1  14288  lmodvsubval2  14300  lmodsubvs  14301  lmodsubdi  14302  lmodsubdir  14303  lmodprop2d  14306  rmodislmodlem  14308  rmodislmod  14309  lsssn0  14328  sraval  14395  cnfldsub  14533  gsumfzfsumlem0  14544  gsumfzfsumlemm  14545  mulgrhm  14567  mulgrhm2  14568  znval  14594  znval2  14596  znunit  14617  psrval  14624  mplvalcoe  14648  mplval2g  14653  restabs  14843  cnprcl2k  14874  cnrest2r  14905  ispsmet  14991  psmettri2  14996  psmetsym  14997  ismet  15012  isxmet  15013  xmettri2  15029  xmetsym  15036  xmettri3  15042  mettri3  15043  xblss2ps  15072  xblss2  15073  comet  15167  xmetxp  15175  xmetxpbl  15176  txmetcnp  15186  fsumcncntop  15235  cncfi  15246  divcncfap  15282  limccl  15327  ellimc3apf  15328  limccnpcntop  15343  limccnp2lem  15344  reldvg  15347  dvfvalap  15349  eldvap  15350  dvcj  15377  dvfre  15378  dvexp  15379  dvexp2  15380  dvrecap  15381  dvmptaddx  15387  dvmptmulx  15388  dvmptnegcn  15390  dvmptsubcn  15391  dvmptcjx  15392  dvmptfsum  15393  dveflem  15394  dvef  15395  plyconst  15413  plyaddlem1  15415  plymullem1  15416  plyadd  15419  plymul  15420  plycoeid3  15425  plycolemc  15426  plyco  15427  plycjlemc  15428  plycj  15429  plyrecj  15431  dvply1  15433  dvply2g  15434  sin0pilem1  15449  sin0pilem2  15450  efper  15475  sinperlem  15476  efimpi  15487  ptolemy  15492  tangtx  15506  abssinper  15514  cosq34lt1  15518  rpcxpef  15562  rpcxpp1  15574  rpcxpneg  15575  rpcxpsub  15576  rpmulcxp  15577  rpdivcxp  15579  cxpmul  15580  rpcxpmul2  15581  rpcxproot  15582  cxpcom  15606  rpabscxpbnd  15608  rplogbval  15613  rplogbreexp  15621  rplogbzexp  15622  rprelogbmulexp  15624  rprelogbdiv  15625  relogbexpap  15626  rplogbcxp  15631  rpcxplogb  15632  logbgcd1irr  15635  logbgcd1irraplemap  15637  binom4  15647  wilthlem1  15648  sgmval  15651  sgmppw  15660  1sgmprm  15662  mersenne  15665  perfectlem1  15667  perfectlem2  15668  perfect  15669  lgslem1  15673  lgsval  15677  lgsfvalg  15678  lgsval2lem  15683  lgsval4  15693  lgsneg  15697  lgsneg1  15698  lgsmod  15699  lgsdir2  15706  lgsdirprm  15707  lgsdilem2  15709  lgsdi  15710  lgsne0  15711  lgssq2  15714  lgsdirnn0  15720  lgsdinn0  15721  gausslemma2dlem1a  15731  gausslemma2dlem1f1o  15733  gausslemma2dlem2  15735  gausslemma2dlem3  15736  gausslemma2dlem4  15737  gausslemma2dlem5  15739  gausslemma2dlem6  15740  gausslemma2d  15742  lgseisenlem1  15743  lgseisenlem2  15744  lgseisenlem3  15745  lgseisenlem4  15746  lgsquadlem1  15750  lgsquadlem2  15751  lgsquadlem3  15752  lgsquad2lem1  15754  lgsquad2lem2  15755  lgsquad2  15756  lgsquad3  15757  m1lgs  15758  2lgslem3c  15768  2lgslem3d  15769  2lgslem3d1  15773  2sqlem2  15788  2sqlem3  15790  2sqlem4  15791  2sqlem8  15796  2sqlem9  15797  2sqlem10  15798  iswlk  16029  qdencn  16354  trilpolemclim  16363  trilpolemcl  16364  trilpolemisumle  16365  trilpolemeq1  16367  trilpolemlt1  16368  trilpo  16370  apdifflemf  16373  apdiff  16375  iswomni0  16378  redcwlpolemeq1  16381  redcwlpo  16382  nconstwlpolem0  16390  nconstwlpolemgt0  16391  nconstwlpo  16393  neapmkv  16395