Theorem oveq2d 5959

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

Syntax hints:   → wi 4   = wceq 1372  (class class class)co 5943

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 710  ax-5 1469  ax-7 1470  ax-gen 1471  ax-ie1 1515  ax-ie2 1516  ax-8 1526  ax-10 1527  ax-11 1528  ax-i12 1529  ax-bndl 1531  ax-4 1532  ax-17 1548  ax-i9 1552  ax-ial 1556  ax-i5r 1557  ax-ext 2186

This theorem depends on definitions:  df-bi 117  df-3an 982  df-tru 1375  df-nf 1483  df-sb 1785  df-clab 2191  df-cleq 2197  df-clel 2200  df-nfc 2336  df-rex 2489  df-v 2773  df-un 3169  df-sn 3638  df-pr 3639  df-op 3641  df-uni 3850  df-br 4044  df-iota 5231  df-fv 5278  df-ov 5946

This theorem is referenced by:  csbov1g  5984  caovassg  6104  caovdig  6120  caovdirg  6123  caov32d  6126  caov4d  6130  caov42d  6132  nnaass  6570  nndi  6571  nnmass  6572  nnmsucr  6573  ecovass  6730  ecoviass  6731  ecovdi  6732  ecovidi  6733  addasspig  7442  mulasspig  7444  distrpig  7445  dfplpq2  7466  mulpipq2  7483  addassnqg  7494  prarloclemarch  7530  prarloclemarch2  7531  ltrnqg  7532  enq0sym  7544  addnq0mo  7559  mulnq0mo  7560  addnnnq0  7561  nq0a0  7569  distrnq0  7571  addassnq0  7574  prarloclemlo  7606  prarloclem3  7609  prarloclem5  7612  prarloclemcalc  7614  addnqprl  7641  addnqpru  7642  prmuloclemcalc  7677  mulnqprl  7680  mulnqpru  7681  distrlem4prl  7696  distrlem4pru  7697  1idprl  7702  1idpru  7703  ltexprlemloc  7719  addcanprleml  7726  addcanprlemu  7727  recexprlem1ssu  7746  ltmprr  7754  caucvgprlemcanl  7756  cauappcvgprlemladdru  7768  cauappcvgprlemladdrl  7769  cauappcvgprlem1  7771  cauappcvgprlemlim  7773  caucvgprlemnkj  7778  caucvgprlemnbj  7779  caucvgprlemdisj  7786  caucvgprlemloc  7787  caucvgprlemcl  7788  caucvgprlemladdrl  7790  caucvgprlem1  7791  caucvgpr  7794  caucvgprprlemell  7797  caucvgprprlemcbv  7799  caucvgprprlemval  7800  caucvgprprlemnkeqj  7802  caucvgprprlemopl  7809  caucvgprprlemlol  7810  caucvgprprlemloc  7815  caucvgprprlemclphr  7817  caucvgprprlemexb  7819  caucvgprprlemaddq  7820  caucvgprprlem1  7821  addcmpblnr  7851  mulcmpblnrlemg  7852  addsrmo  7855  mulsrmo  7856  addsrpr  7857  mulsrpr  7858  ltsrprg  7859  recexgt0sr  7885  mulgt0sr  7890  caucvgsrlemgt1  7907  caucvgsrlemoffval  7908  caucvgsr  7914  suplocsrlemb  7918  suplocsrlempr  7919  suplocsrlem  7920  suplocsr  7921  mulcnsr  7947  pitoregt0  7961  recidpirqlemcalc  7969  axmulcom  7983  axmulass  7985  axdistr  7986  ax0id  7990  axcnre  7993  recriota  8002  axcaucvglemcau  8010  axcaucvglemres  8011  mulrid  8068  adddirp1d  8098  mul32  8201  mul31  8202  add32  8230  add4  8232  add42  8233  cnegex  8249  addcan2  8252  addsubass  8281  subsub2  8299  nppcan2  8302  sub32  8305  nnncan  8306  sub4  8316  muladd  8455  subdi  8456  mul2neg  8469  submul2  8470  mulsub  8472  muls1d  8489  mulsubfacd  8490  add20  8546  recexre  8650  rereim  8658  apreap  8659  ltmul1  8664  cru  8674  apreim  8675  mulreim  8676  apadd1  8680  apneg  8683  mulap0  8726  divrecap  8760  divassap  8762  divmulasscomap  8768  divsubdirap  8780  divdivdivap  8785  divmul24ap  8788  divmuleqap  8789  divcanap6  8791  divdivap1  8795  divdivap2  8796  divsubdivap  8800  conjmulap  8801  div2negap  8807  apmul1  8860  cju  9033  nnmulcl  9056  add1p1  9286  sub1m1  9287  cnm2m1cnm3  9288  xp1d2m1eqxm1d2  9289  div4p1lem1div2  9290  un0addcl  9327  un0mulcl  9328  zaddcllemneg  9410  qapne  9759  cnref1o  9771  rexsub  9974  xnegid  9980  xaddcom  9982  xnegdi  9989  xaddass  9990  xaddass2  9991  xpncan  9992  xnpcan  9993  xleadd1a  9994  xsubge0  10002  xposdif  10003  xlesubadd  10004  xadd4d  10006  lincmb01cmp  10124  iccf1o  10125  ige3m2fz  10170  fztp  10199  fzsuc2  10200  fseq1m1p1  10216  fzm1  10221  ige2m1fz1  10230  nn0split  10257  nnsplit  10258  fzo0addelr  10316  elfzoext  10319  fzval3  10331  zpnn0elfzo1  10335  fzosplitsnm1  10336  fzosplitprm1  10361  fzoshftral  10365  rebtwn2zlemstep  10393  flhalf  10443  fldiv4lem1div2uz2  10447  modqval  10467  modqvalr  10468  modqdiffl  10478  modqfrac  10480  flqmod  10481  intqfrac  10482  zmod10  10483  modqmulnn  10485  modqvalp1  10486  modqid  10492  modqcyc  10502  modqcyc2  10503  modqmul1  10520  q2submod  10528  modqdi  10535  modqsubdir  10536  modqeqmodmin  10537  modsumfzodifsn  10539  addmodlteq  10541  frecuzrdgsuctlem  10566  uzsinds  10587  seqeq3  10595  iseqvalcbv  10602  seq3val  10603  seqvalcd  10604  seqf  10607  seq3p1  10608  seqovcd  10610  seqp1cd  10613  seq3m1  10616  seq3fveq2  10618  seqfveq2g  10620  seq3shft2  10624  seqshft2g  10625  monoord2  10629  ser3mono  10630  seq3split  10631  seqsplitg  10632  seq3caopr3  10634  seqcaopr3g  10635  seq3caopr2  10636  seqcaopr2g  10637  seq3caopr  10638  seqcaoprg  10639  seqf1oglem2a  10661  seqf1oglem2  10663  seq3id2  10669  seq3homo  10670  seq3z  10671  seqhomog  10673  exp3vallem  10683  exp3val  10684  expp1  10689  expnegap0  10690  expineg2  10691  expn1ap0  10692  expm1t  10710  1exp  10711  expnegzap  10716  mulexpzap  10722  expadd  10724  expaddzaplem  10725  expaddzap  10726  expmul  10727  expmulzap  10728  m1expeven  10729  expsubap  10730  expp1zap  10731  expm1ap  10732  expdivap  10733  iexpcyc  10787  subsq2  10790  binom2  10794  binom21  10795  binom2sub  10796  binom2sub1  10797  mulbinom2  10799  binom3  10800  zesq  10801  bernneq  10803  sqoddm1div8  10836  mulsubdivbinom2ap  10854  nn0opthlem1d  10863  nn0opthd  10865  facp1  10873  facnn2  10877  faclbnd  10884  faclbnd6  10887  bcval  10892  bccmpl  10897  bcn0  10898  bcnn  10900  bcnp1n  10902  bcm1k  10903  bcp1n  10904  bcp1nk  10905  bcval5  10906  bcp1m1  10908  bcpasc  10909  bcn2m1  10912  bcn2p1  10913  omgadd  10945  hashunlem  10947  hashunsng  10950  hashdifsn  10962  hashxp  10969  zfz1isolemsplit  10981  zfz1isolem1  10983  zfz1iso  10984  seq3coll  10985  wrdf  10998  ccatfvalfi  11046  elfzelfzccat  11054  ccatlid  11060  ccatrid  11061  ccatass  11062  ccatws1leng  11086  ccats1val2  11090  shftcan1  11116  shftcan2  11117  cjval  11127  cjth  11128  crre  11139  replim  11141  remim  11142  reim0b  11144  rereb  11145  mulreap  11146  cjreb  11148  recj  11149  reneg  11150  readd  11151  resub  11152  remullem  11153  imcj  11157  imneg  11158  imadd  11159  imsub  11160  cjcj  11165  cjadd  11166  ipcnval  11168  cjmulrcl  11169  cjneg  11172  addcj  11173  cjsub  11174  cnrecnv  11192  caucvgrelemcau  11262  cvg1nlemcau  11266  cvg1nlemres  11267  recvguniqlem  11276  resqrexlemover  11292  resqrexlemlo  11295  resqrexlemcalc1  11296  resqrexlemcalc3  11298  resqrexlemnm  11300  resqrexlemcvg  11301  absneg  11332  abscj  11334  sqabsadd  11337  sqabssub  11338  absmul  11351  absid  11353  absre  11359  absresq  11360  absexpzap  11362  recvalap  11379  abstri  11386  abs2dif2  11389  recan  11391  cau3lem  11396  amgm2  11400  bdtrilem  11521  xrmaxadd  11543  xrbdtri  11558  climaddc1  11611  climsubc1  11614  climcvg1nlem  11631  serf0  11634  summodclem3  11662  summodclem2a  11663  summodc  11665  fsumsplitsn  11692  fsumm1  11698  fsumsplitsnun  11701  fsump1  11702  isummulc2  11708  fsumrev  11725  fisum0diag2  11729  fsummulc2  11730  fsumsub  11734  fsumabs  11747  telfsumo  11748  fsumparts  11752  fsumrelem  11753  fsumiun  11759  binomlem  11765  binom  11766  binom1p  11767  binom11  11768  binom1dif  11769  bcxmas  11771  isumsplit  11773  isum1p  11774  divcnv  11779  arisum2  11781  trireciplem  11782  trirecip  11783  geolim  11793  georeclim  11795  geo2sum  11796  geo2lim  11798  geoisum1c  11802  0.999...  11803  cvgratnnlemnexp  11806  cvgratnnlemmn  11807  cvgratz  11814  mertenslem2  11818  mertensabs  11819  clim2prod  11821  prodfrecap  11828  prodfdivap  11829  prodmodclem3  11857  prodmodclem2a  11858  fprodm1  11880  fprodp1  11882  fprodunsn  11886  fprodfac  11897  fprodeq0  11899  fprodconst  11902  fprodrec  11911  fproddivap  11912  fprodsplitsn  11915  ege2le3  11953  efaddlem  11956  efsub  11963  efexp  11964  eftlub  11972  efsep  11973  effsumlt  11974  ef4p  11976  tanval3ap  11996  resinval  11997  recosval  11998  efi4p  11999  efival  12014  efmival  12015  efeul  12016  sinadd  12018  cosadd  12019  tanaddap  12021  sinsub  12022  cossub  12023  sincossq  12030  sin2t  12031  cos2t  12032  cos2tsin  12033  ef01bndlem  12038  sin01bnd  12039  cos01bnd  12040  cos12dec  12050  absef  12052  absefib  12053  efieq1re  12054  demoivreALT  12056  eirraplem  12059  dvdsexp  12143  oexpneg  12159  opeo  12179  omeo  12180  m1exp1  12183  flodddiv4  12218  flodddiv4t2lthalf  12221  bitsval  12225  bitsp1  12233  bitsinv1lem  12243  bitsinv1  12244  divgcdnnr  12268  gcdaddm  12276  gcdadd  12277  gcdid  12278  modgcd  12283  gcdmultipled  12285  dvdsgcdidd  12286  bezoutlemnewy  12288  bezoutlema  12291  bezoutlemb  12292  bezoutlemex  12293  bezoutlembz  12296  absmulgcd  12309  gcdmultiple  12312  gcdmultiplez  12313  rpmulgcd  12318  rplpwr  12319  eucalginv  12349  eucalg  12352  lcmneg  12367  lcmgcdlem  12370  lcmgcd  12371  lcmid  12373  lcm1  12374  mulgcddvds  12387  qredeq  12389  divgcdcoprmex  12395  prmind2  12413  rpexp1i  12447  pw2dvdslemn  12458  pw2dvdseulemle  12460  pw2dvdseu  12461  oddpwdclemxy  12462  oddpwdclemdvds  12463  oddpwdclemndvds  12464  oddpwdclemdc  12466  2sqpwodd  12469  nn0gcdsq  12493  phiprmpw  12515  eulerthlemrprm  12522  eulerthlema  12523  eulerthlemh  12524  eulerthlemth  12525  fermltl  12527  prmdiv  12528  hashgcdlem  12531  odzdvds  12539  vfermltl  12545  modprm0  12548  nnnn0modprm0  12549  modprmn0modprm0  12550  coprimeprodsq  12551  pythagtriplem1  12559  pythagtriplem4  12562  pythagtriplem12  12569  pythagtriplem14  12571  pythagtriplem16  12573  pythagtriplem18  12575  pythagtrip  12577  pcpremul  12587  pceu  12589  pczpre  12591  pcdiv  12596  pcqmul  12597  pcqdiv  12601  pcexp  12603  pcxqcl  12606  pczdvds  12608  pczndvds  12610  pczndvds2  12612  pcid  12618  pcneg  12619  pcdvdstr  12621  pcgcd1  12622  pcgcd  12623  pc2dvds  12624  pcaddlem  12633  pcadd  12634  pcadd2  12635  pcmpt  12637  pcmpt2  12638  fldivp1  12642  pcfac  12644  pcbc  12645  expnprm  12647  prmpwdvds  12649  pockthlem  12650  pockthi  12652  4sqlem7  12678  4sqlem9  12680  4sqlem10  12681  4sqlem2  12683  4sqlem3  12684  4sqlem4  12686  mul4sqlem  12687  4sqlem11  12695  4sqlem16  12700  4sqlem17  12701  4sqlem19  12703  setscomd  12844  ressvalsets  12867  strressid  12874  ressval3d  12875  ressinbasd  12877  ressressg  12878  ressabsg  12879  grpinvalem  13188  grpinva  13189  grprida  13190  isnsgrp  13209  sgrpass  13211  sgrp1  13214  sgrppropd  13216  prdssgrpd  13218  mnd32g  13230  mnd4g  13232  mndpropd  13243  prdsidlem  13250  prdsmndd  13251  imasmnd2  13255  mhmex  13265  mhmlin  13270  gsumwmhm  13301  grprcan  13340  grpsubval  13349  grpinvid2  13356  grpasscan2  13367  grpsubinv  13376  grpinvadd  13381  grpsubid1  13388  grpsubadd0sub  13390  grpsubadd  13391  grpsubsub  13392  grpaddsubass  13393  grppncan  13394  grpnnncan2  13400  grpsubpropd2  13408  imasgrp2  13417  mhmlem  13421  mhmid  13422  mhmmnd  13423  ghmgrp  13425  mulgnn0gsum  13435  mulgnnp1  13437  mulgaddcomlem  13452  mulgaddcom  13453  mulginvinv  13455  mulgnn0dir  13459  mulgdirlem  13460  mulgp1  13462  mulgneg2  13463  mulgnn0ass  13465  mulgass  13466  mulgmodid  13468  mulgsubdir  13469  nmzsubg  13517  0nsg  13521  eqger  13531  qussub  13544  ghmlin  13555  ghmsub  13558  conjghm  13583  ablsub4  13620  abladdsub4  13621  ablsubsub4  13626  ablsub32  13629  ablnnncan  13630  gsumfzmptfidmadd2  13647  gsumfzconst  13648  gsumfzmhm2  13651  gsumfzsnfd  13652  mgpress  13664  rngass  13672  rngdi  13673  rngdir  13674  rngrz  13679  rngmneg2  13681  rngsubdi  13684  rngsubdir  13685  rngpropd  13688  imasrng  13689  srgass  13704  srgpcomp  13723  srgpcompp  13724  srgpcomppsc  13725  srg1expzeq1  13728  ringpropd  13771  ringrz  13777  ringnegr  13785  ringmneg2  13787  ringsubdi  13789  ringsubdir  13790  ring1  13792  imasring  13797  opprrng  13810  opprring  13812  mulgass3  13818  dvdsrd  13827  unitgrp  13849  invrfvald  13855  dvr1  13871  dvrass  13872  dvrcan1  13873  dvrcan3  13874  rdivmuldivd  13877  subrginv  13970  subrgdv  13971  resrhm2b  13982  islmod  14024  lmodlema  14025  islmodd  14026  lmodvs0  14055  lmodvneg1  14063  lmodvsubval2  14075  lmodsubvs  14076  lmodsubdi  14077  lmodsubdir  14078  lmodprop2d  14081  rmodislmodlem  14083  rmodislmod  14084  lsssn0  14103  sraval  14170  cnfldsub  14308  gsumfzfsumlem0  14319  gsumfzfsumlemm  14320  mulgrhm  14342  mulgrhm2  14343  znval  14369  znval2  14371  znunit  14392  psrval  14399  mplvalcoe  14423  mplval2g  14428  restabs  14618  cnprcl2k  14649  cnrest2r  14680  ispsmet  14766  psmettri2  14771  psmetsym  14772  ismet  14787  isxmet  14788  xmettri2  14804  xmetsym  14811  xmettri3  14817  mettri3  14818  xblss2ps  14847  xblss2  14848  comet  14942  xmetxp  14950  xmetxpbl  14951  txmetcnp  14961  fsumcncntop  15010  cncfi  15021  divcncfap  15057  limccl  15102  ellimc3apf  15103  limccnpcntop  15118  limccnp2lem  15119  reldvg  15122  dvfvalap  15124  eldvap  15125  dvcj  15152  dvfre  15153  dvexp  15154  dvexp2  15155  dvrecap  15156  dvmptaddx  15162  dvmptmulx  15163  dvmptnegcn  15165  dvmptsubcn  15166  dvmptcjx  15167  dvmptfsum  15168  dveflem  15169  dvef  15170  plyconst  15188  plyaddlem1  15190  plymullem1  15191  plyadd  15194  plymul  15195  plycoeid3  15200  plycolemc  15201  plyco  15202  plycjlemc  15203  plycj  15204  plyrecj  15206  dvply1  15208  dvply2g  15209  sin0pilem1  15224  sin0pilem2  15225  efper  15250  sinperlem  15251  efimpi  15262  ptolemy  15267  tangtx  15281  abssinper  15289  cosq34lt1  15293  rpcxpef  15337  rpcxpp1  15349  rpcxpneg  15350  rpcxpsub  15351  rpmulcxp  15352  rpdivcxp  15354  cxpmul  15355  rpcxpmul2  15356  rpcxproot  15357  cxpcom  15381  rpabscxpbnd  15383  rplogbval  15388  rplogbreexp  15396  rplogbzexp  15397  rprelogbmulexp  15399  rprelogbdiv  15400  relogbexpap  15401  rplogbcxp  15406  rpcxplogb  15407  logbgcd1irr  15410  logbgcd1irraplemap  15412  binom4  15422  wilthlem1  15423  sgmval  15426  sgmppw  15435  1sgmprm  15437  mersenne  15440  perfectlem1  15442  perfectlem2  15443  perfect  15444  lgslem1  15448  lgsval  15452  lgsfvalg  15453  lgsval2lem  15458  lgsval4  15468  lgsneg  15472  lgsneg1  15473  lgsmod  15474  lgsdir2  15481  lgsdirprm  15482  lgsdilem2  15484  lgsdi  15485  lgsne0  15486  lgssq2  15489  lgsdirnn0  15495  lgsdinn0  15496  gausslemma2dlem1a  15506  gausslemma2dlem1f1o  15508  gausslemma2dlem2  15510  gausslemma2dlem3  15511  gausslemma2dlem4  15512  gausslemma2dlem5  15514  gausslemma2dlem6  15515  gausslemma2d  15517  lgseisenlem1  15518  lgseisenlem2  15519  lgseisenlem3  15520  lgseisenlem4  15521  lgsquadlem1  15525  lgsquadlem2  15526  lgsquadlem3  15527  lgsquad2lem1  15529  lgsquad2lem2  15530  lgsquad2  15531  lgsquad3  15532  m1lgs  15533  2lgslem3c  15543  2lgslem3d  15544  2lgslem3d1  15548  2sqlem2  15563  2sqlem3  15565  2sqlem4  15566  2sqlem8  15571  2sqlem9  15572  2sqlem10  15573  qdencn  15928  trilpolemclim  15937  trilpolemcl  15938  trilpolemisumle  15939  trilpolemeq1  15941  trilpolemlt1  15942  trilpo  15944  apdifflemf  15947  apdiff  15949  iswomni0  15952  redcwlpolemeq1  15955  redcwlpo  15956  nconstwlpolem0  15964  nconstwlpolemgt0  15965  nconstwlpo  15967  neapmkv  15969