Theorem oveq2d 6074

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

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

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 2216

This theorem depends on definitions:  df-bi 117  df-3an 1007  df-tru 1401  df-nf 1510  df-sb 1812  df-clab 2221  df-cleq 2227  df-clel 2230  df-nfc 2375  df-rex 2528  df-v 2817  df-un 3218  df-sn 3700  df-pr 3701  df-op 3703  df-uni 3920  df-br 4115  df-iota 5317  df-fv 5365  df-ov 6061

This theorem is referenced by:  csbov1g  6099  caovassg  6221  caovdig  6237  caovdirg  6240  caov32d  6243  caov4d  6247  caov42d  6249  suppofss1dcl  6477  suppofss2dcl  6478  nnaass  6731  nndi  6732  nnmass  6733  nnmsucr  6734  ecovass  6891  ecoviass  6892  ecovdi  6893  ecovidi  6894  addasspig  7661  mulasspig  7663  distrpig  7664  dfplpq2  7685  mulpipq2  7702  addassnqg  7713  prarloclemarch  7749  prarloclemarch2  7750  ltrnqg  7751  enq0sym  7763  addnq0mo  7778  mulnq0mo  7779  addnnnq0  7780  nq0a0  7788  distrnq0  7790  addassnq0  7793  prarloclemlo  7825  prarloclem3  7828  prarloclem5  7831  prarloclemcalc  7833  addnqprl  7860  addnqpru  7861  prmuloclemcalc  7896  mulnqprl  7899  mulnqpru  7900  distrlem4prl  7915  distrlem4pru  7916  1idprl  7921  1idpru  7922  ltexprlemloc  7938  addcanprleml  7945  addcanprlemu  7946  recexprlem1ssu  7965  ltmprr  7973  caucvgprlemcanl  7975  cauappcvgprlemladdru  7987  cauappcvgprlemladdrl  7988  cauappcvgprlem1  7990  cauappcvgprlemlim  7992  caucvgprlemnkj  7997  caucvgprlemnbj  7998  caucvgprlemdisj  8005  caucvgprlemloc  8006  caucvgprlemcl  8007  caucvgprlemladdrl  8009  caucvgprlem1  8010  caucvgpr  8013  caucvgprprlemell  8016  caucvgprprlemcbv  8018  caucvgprprlemval  8019  caucvgprprlemnkeqj  8021  caucvgprprlemopl  8028  caucvgprprlemlol  8029  caucvgprprlemloc  8034  caucvgprprlemclphr  8036  caucvgprprlemexb  8038  caucvgprprlemaddq  8039  caucvgprprlem1  8040  addcmpblnr  8070  mulcmpblnrlemg  8071  addsrmo  8074  mulsrmo  8075  addsrpr  8076  mulsrpr  8077  ltsrprg  8078  recexgt0sr  8104  mulgt0sr  8109  caucvgsrlemgt1  8126  caucvgsrlemoffval  8127  caucvgsr  8133  suplocsrlemb  8137  suplocsrlempr  8138  suplocsrlem  8139  suplocsr  8140  mulcnsr  8166  pitoregt0  8180  recidpirqlemcalc  8188  axmulcom  8202  axmulass  8204  axdistr  8205  ax0id  8209  axcnre  8212  recriota  8221  axcaucvglemcau  8229  axcaucvglemres  8230  mulrid  8287  adddirp1d  8316  mul32  8419  mul31  8420  add32  8448  add4  8450  add42  8451  cnegex  8467  addcan2  8470  addsubass  8499  subsub2  8517  nppcan2  8520  sub32  8523  nnncan  8524  sub4  8534  muladd  8674  subdi  8675  mul2neg  8688  submul2  8689  mulsub  8691  muls1d  8708  mulsubfacd  8709  add20  8765  recexre  8869  rereim  8877  apreap  8878  ltmul1  8883  cru  8893  apreim  8894  mulreim  8895  apadd1  8899  apneg  8902  mulap0  8945  divrecap  8979  divassap  8981  divmulasscomap  8987  divsubdirap  8999  divdivdivap  9004  divmul24ap  9007  divmuleqap  9008  divcanap6  9010  divdivap1  9014  divdivap2  9015  divsubdivap  9019  conjmulap  9020  div2negap  9026  apmul1  9079  cju  9252  nnmulcl  9275  add1p1  9505  sub1m1  9506  cnm2m1cnm3  9507  xp1d2m1eqxm1d2  9508  div4p1lem1div2  9509  un0addcl  9546  un0mulcl  9547  zaddcllemneg  9633  qapne  9989  cnref1o  10001  rexsub  10205  xnegid  10211  xaddcom  10213  xnegdi  10220  xaddass  10221  xaddass2  10222  xpncan  10223  xnpcan  10224  xleadd1a  10225  xsubge0  10233  xposdif  10234  xlesubadd  10235  xadd4d  10237  lincmb01cmp  10355  iccf1o  10357  ige3m2fz  10403  fztp  10434  fzsuc2  10435  fseq1m1p1  10451  fzm1  10456  ige2m1fz1  10465  nn0split  10492  nnsplit  10493  fzo0addelr  10556  elfzoext  10559  fzval3  10571  zpnn0elfzo1  10575  fzosplitsnm1  10576  fzosplitpr  10601  fzosplitprm1  10602  fzoshftral  10606  rebtwn2zlemstep  10636  flhalf  10686  fldiv4lem1div2uz2  10690  modqval  10710  modqvalr  10711  modqdiffl  10721  modqfrac  10723  flqmod  10724  intqfrac  10725  zmod10  10726  modqmulnn  10728  modqvalp1  10729  modqid  10735  modqcyc  10745  modqcyc2  10746  modqmul1  10763  q2submod  10771  modqdi  10778  modqsubdir  10779  modqeqmodmin  10780  modsumfzodifsn  10782  addmodlteq  10784  frecuzrdgsuctlem  10809  uzsinds  10830  seqeq3  10838  iseqvalcbv  10845  seq3val  10846  seqvalcd  10847  seqf  10850  seq3p1  10851  seqovcd  10853  seqp1cd  10856  seq3m1  10859  seq3fveq2  10861  seqfveq2g  10863  seq3shft2  10867  seqshft2g  10868  monoord2  10872  ser3mono  10873  seq3split  10874  seqsplitg  10875  seq3caopr3  10877  seqcaopr3g  10878  seq3caopr2  10879  seqcaopr2g  10880  seq3caopr  10881  seqcaoprg  10882  seqf1oglem2a  10904  seqf1oglem2  10906  seq3id2  10912  seq3homo  10913  seq3z  10914  seqhomog  10916  exp3vallem  10926  exp3val  10927  expp1  10932  expnegap0  10933  expineg2  10934  expn1ap0  10935  expm1t  10953  1exp  10954  expnegzap  10959  mulexpzap  10965  expadd  10967  expaddzaplem  10968  expaddzap  10969  expmul  10970  expmulzap  10971  m1expeven  10972  expsubap  10973  expp1zap  10974  expm1ap  10975  expdivap  10976  iexpcyc  11030  subsq2  11033  binom2  11037  binom21  11038  binom2sub  11039  binom2sub1  11040  mulbinom2  11042  binom3  11043  zesq  11045  bernneq  11047  sqoddm1div8  11080  mulsubdivbinom2ap  11098  nn0opthlem1d  11107  nn0opthd  11109  facp1  11117  facnn2  11121  faclbnd  11128  faclbnd6  11131  bcval  11136  bccmpl  11141  bcn0  11142  bcnn  11144  bcnp1n  11146  bcm1k  11147  bcp1n  11148  bcp1nk  11149  bcval5  11150  bcp1m1  11152  bcpasc  11153  bcm1n  11156  bcn2m1  11157  bcn2p1  11158  omgadd  11191  hashunlem  11193  hashunsng  11197  hashdifsn  11209  hashxp  11216  hashmap  11217  sseqn  11228  zfz1isolemsplit  11235  zfz1isolem1  11237  zfz1iso  11238  seq3coll  11239  wrdf  11255  ccatfvalfi  11305  elfzelfzccat  11313  ccatlid  11319  ccatrid  11320  ccatass  11321  ccatalpha  11326  ccatws1leng  11347  ccats1val2  11353  ccatw2s1p1g  11358  swrdval  11365  swrd00g  11366  swrdf  11372  swrdfv2  11380  swrdwrdsymbg  11381  swrdspsleq  11384  swrds1  11385  swrdlsw  11386  ccatswrd  11387  swrdccat2  11388  pfxmpt  11397  pfxfv  11401  pfxeq  11413  pfxsuff1eqwrdeq  11416  ccatpfx  11418  pfxccat1  11419  swrdswrd  11422  pfxswrd  11423  swrdpfx  11424  pfxpfx  11425  pfxlswccat  11430  ccats1pfxeq  11431  ccats1pfxeqrex  11432  ccatopth2  11434  cats1un  11438  wrdind  11439  wrd2ind  11440  swrdccatfn  11441  swrdccatin1  11442  pfxccatin12lem4  11443  swrdccatin2  11446  pfxccatin12lem2c  11447  pfxccatin12lem2  11448  pfxccatin12  11450  swrdccat  11452  swrdccat3blem  11456  swrdccat3b  11457  swrdccatin2d  11461  pfxccatin12d  11462  reuccatpfxs1lem  11463  reuccatpfxs1  11464  shftcan1  11544  shftcan2  11545  cjval  11555  cjth  11556  crre  11567  replim  11569  remim  11570  reim0b  11572  rereb  11573  mulreap  11574  cjreb  11576  recj  11577  reneg  11578  readd  11579  resub  11580  remullem  11581  imcj  11585  imneg  11586  imadd  11587  imsub  11588  cjcj  11593  cjadd  11594  ipcnval  11596  cjmulrcl  11597  cjneg  11600  addcj  11601  cjsub  11602  cnrecnv  11620  caucvgrelemcau  11690  cvg1nlemcau  11694  cvg1nlemres  11695  recvguniqlem  11704  resqrexlemover  11720  resqrexlemlo  11723  resqrexlemcalc1  11724  resqrexlemcalc3  11726  resqrexlemnm  11728  resqrexlemcvg  11729  absneg  11760  abscj  11762  sqabsadd  11765  sqabssub  11766  absmul  11779  absid  11781  absre  11787  absresq  11788  absexpzap  11790  recvalap  11807  abstri  11814  abs2dif2  11817  recan  11819  cau3lem  11824  amgm2  11828  bdtrilem  11949  xrmaxadd  11971  xrbdtri  11986  climaddc1  12039  climsubc1  12042  climcvg1nlem  12059  serf0  12062  fzf1o  12086  summodclem3  12091  summodclem2a  12092  summodc  12094  fsumsplitsn  12121  fsumm1  12127  fsumsplitsnun  12130  fsump1  12131  isummulc2  12137  fsumrev  12154  fisum0diag2  12158  fsummulc2  12159  fsumsub  12163  fsumabs  12176  telfsumo  12177  fsumparts  12181  fsumrelem  12182  fsumiun  12188  binomlem  12194  binom  12195  binom1p  12196  binom11  12197  binom1dif  12198  bcxmas  12200  isumsplit  12202  isum1p  12203  divcnv  12208  arisum2  12210  trireciplem  12211  trirecip  12212  geolim  12222  georeclim  12224  geo2sum  12225  geo2lim  12227  geoisum1c  12231  0.999...  12232  cvgratnnlemnexp  12235  cvgratnnlemmn  12236  cvgratz  12243  mertenslem2  12247  mertensabs  12248  clim2prod  12250  prodfrecap  12257  prodfdivap  12258  prodmodclem3  12286  prodmodclem2a  12287  fprodm1  12309  fprodp1  12311  fprodunsn  12315  fprodfac  12326  fprodeq0  12328  fprodconst  12331  fprodrec  12340  fproddivap  12341  fprodsplitsn  12344  ege2le3  12382  efaddlem  12385  efsub  12392  efexp  12393  eftlub  12401  efsep  12402  effsumlt  12403  ef4p  12405  tanval3ap  12425  resinval  12426  recosval  12427  efi4p  12428  efival  12443  efmival  12444  efeul  12445  sinadd  12447  cosadd  12448  tanaddap  12450  sinsub  12451  cossub  12452  sincossq  12459  sin2t  12460  cos2t  12461  cos2tsin  12462  ef01bndlem  12467  sin01bnd  12468  cos01bnd  12469  cos12dec  12479  absef  12481  absefib  12482  efieq1re  12483  demoivreALT  12485  eirraplem  12488  dvdsexp  12572  oexpneg  12588  opeo  12608  omeo  12609  m1exp1  12612  flodddiv4  12647  flodddiv4t2lthalf  12650  bitsval  12654  bitsp1  12662  bitsinv1lem  12672  bitsinv1  12673  divgcdnnr  12697  gcdaddm  12705  gcdadd  12706  gcdid  12707  modgcd  12712  gcdmultipled  12714  dvdsgcdidd  12715  bezoutlemnewy  12717  bezoutlema  12720  bezoutlemb  12721  bezoutlemex  12722  bezoutlembz  12725  absmulgcd  12738  gcdmultiple  12741  gcdmultiplez  12742  rpmulgcd  12747  rplpwr  12748  eucalginv  12778  eucalg  12781  lcmneg  12796  lcmgcdlem  12799  lcmgcd  12800  lcmid  12802  lcm1  12803  mulgcddvds  12816  qredeq  12818  divgcdcoprmex  12824  prmind2  12842  rpexp1i  12876  pw2dvdslemn  12887  pw2dvdseulemle  12889  pw2dvdseu  12890  oddpwdclemxy  12891  oddpwdclemdvds  12892  oddpwdclemndvds  12893  oddpwdclemdc  12895  2sqpwodd  12898  nn0gcdsq  12922  phiprmpw  12944  eulerthlemrprm  12951  eulerthlema  12952  eulerthlemh  12953  eulerthlemth  12954  fermltl  12956  prmdiv  12957  hashgcdlem  12960  odzdvds  12968  vfermltl  12974  modprm0  12977  nnnn0modprm0  12978  modprmn0modprm0  12979  coprimeprodsq  12980  pythagtriplem1  12988  pythagtriplem4  12991  pythagtriplem12  12998  pythagtriplem14  13000  pythagtriplem16  13002  pythagtriplem18  13004  pythagtrip  13006  pcpremul  13016  pceu  13018  pczpre  13020  pcdiv  13025  pcqmul  13026  pcqdiv  13030  pcexp  13032  pcxqcl  13035  pczdvds  13037  pczndvds  13039  pczndvds2  13041  pcid  13047  pcneg  13048  pcdvdstr  13050  pcgcd1  13051  pcgcd  13052  pc2dvds  13053  pcaddlem  13062  pcadd  13063  pcadd2  13064  pcmpt  13066  pcmpt2  13067  fldivp1  13071  pcfac  13073  pcbc  13074  expnprm  13076  prmpwdvds  13078  pockthlem  13079  pockthi  13081  4sqlem7  13107  4sqlem9  13109  4sqlem10  13110  4sqlem2  13112  4sqlem3  13113  4sqlem4  13115  mul4sqlem  13116  4sqlem11  13124  4sqlem16  13129  4sqlem17  13130  4sqlem19  13132  ballotfilemfc0  13176  ballotfilemfcc  13177  ballotfilemsv  13197  ballotfilemsima  13203  ballotfilemfrci  13215  setscomd  13337  ressvalsets  13361  strressid  13368  ressval3d  13369  ressinbasd  13371  ressressg  13372  ressabsg  13373  grpinvalem  13648  grpinva  13649  grprida  13650  isnsgrp  13669  sgrpass  13671  sgrp1  13674  sgrppropd  13676  mnd32g  13688  mnd4g  13690  mndpropd  13701  imasmnd2  13707  mhmex  13717  mhmlin  13722  gsumwmhm  13753  grprcan  13792  grpsubval  13801  grpinvid2  13808  grpasscan2  13819  grpsubinv  13828  grpinvadd  13833  grpsubid1  13840  grpsubadd0sub  13842  grpsubadd  13843  grpsubsub  13844  grpaddsubass  13845  grppncan  13846  grpnnncan2  13852  grpsubpropd2  13860  imasgrp2  13863  mhmlem  13867  mhmid  13868  mhmmnd  13869  ghmgrp  13871  mulgnn0gsum  13881  mulgnnp1  13883  mulgaddcomlem  13898  mulgaddcom  13899  mulginvinv  13901  mulgnn0dir  13905  mulgdirlem  13906  mulgp1  13908  mulgneg2  13909  mulgnn0ass  13911  mulgass  13912  mulgmodid  13914  mulgsubdir  13915  nmzsubg  13963  0nsg  13967  eqger  13977  qussub  13990  ghmlin  14001  ghmsub  14004  conjghm  14029  ablsub4  14066  abladdsub4  14067  ablsubsub4  14072  ablsub32  14075  ablnnncan  14076  gsumfzmptfidmadd2  14093  gsumfzconst  14094  gsumfzmhm2  14097  gsumfzsnfd  14098  gsumsplit0  14099  gfsumval  14102  gsumgfsum1  14103  gsumgfsum  14106  gfsumsn  14107  gfsump1  14108  gfsumz  14109  gfsumcl  14110  prdssgrpd  14133  prdsidlem  14135  prdsmndd  14136  mgpress  14170  rngass  14178  rngdi  14179  rngdir  14180  rngrz  14185  rngmneg2  14187  rngsubdi  14190  rngsubdir  14191  rngpropd  14194  imasrng  14195  srgass  14214  srgpcomp  14233  srgpcompp  14234  srgpcomppsc  14235  srg1expzeq1  14238  ringpropd  14281  ringrz  14287  ringnegr  14295  ringmneg2  14297  ringsubdi  14299  ringsubdir  14300  ring1  14302  imasring  14307  opprrng  14320  opprring  14322  mulgass3  14329  dvdsrd  14339  unitgrp  14361  invrfvald  14367  dvr1  14383  dvrass  14384  dvrcan1  14385  dvrcan3  14386  rdivmuldivd  14389  subrginv  14483  subrgdv  14484  resrhm2b  14495  rrgsupp  14512  islmod  14565  lmodlema  14566  islmodd  14567  lmodvs0  14596  lmodvneg1  14604  lmodvsubval2  14616  lmodsubvs  14617  lmodsubdi  14618  lmodsubdir  14619  lmodprop2d  14622  rmodislmodlem  14624  rmodislmod  14625  lsssn0  14644  sraval  14711  cnfldsub  14849  gsumfzfsumlem0  14860  gsumfzfsumlemm  14861  mulgrhm  14883  mulgrhm2  14884  znval  14910  znval2  14912  znunit  14933  psrval  14940  mplvalcoe  14971  mplval2g  14976  restabs  15166  cnprcl2k  15197  cnrest2r  15228  ispsmet  15314  psmettri2  15319  psmetsym  15320  ismet  15335  isxmet  15336  xmettri2  15352  xmetsym  15359  xmettri3  15365  mettri3  15366  xblss2ps  15395  xblss2  15396  comet  15490  xmetxp  15498  xmetxpbl  15499  txmetcnp  15509  fsumcncntop  15558  cncfi  15569  divcncfap  15605  limccl  15650  ellimc3apf  15651  limccnpcntop  15666  limccnp2lem  15667  reldvg  15670  dvfvalap  15672  eldvap  15673  dvcj  15700  dvfre  15701  dvexp  15702  dvexp2  15703  dvrecap  15704  dvmptaddx  15710  dvmptmulx  15711  dvmptnegcn  15713  dvmptsubcn  15714  dvmptcjx  15715  dvmptfsum  15716  dveflem  15717  dvef  15718  plyconst  15736  plyaddlem1  15738  plymullem1  15739  plyadd  15742  plymul  15743  plycoeid3  15748  plycolemc  15749  plyco  15750  plycjlemc  15751  plycj  15752  plyrecj  15754  dvply1  15756  dvply2g  15757  sin0pilem1  15772  sin0pilem2  15773  efper  15798  sinperlem  15799  efimpi  15810  ptolemy  15815  tangtx  15829  abssinper  15837  cosq34lt1  15841  rpcxpef  15885  rpcxpp1  15897  rpcxpneg  15898  rpcxpsub  15899  rpmulcxp  15900  rpdivcxp  15902  cxpmul  15903  rpcxpmul2  15904  rpcxproot  15905  cxpcom  15929  rpabscxpbnd  15931  rplogbval  15936  rplogbreexp  15944  rplogbzexp  15945  rprelogbmulexp  15947  rprelogbdiv  15948  relogbexpap  15949  rplogbcxp  15954  rpcxplogb  15955  logbgcd1irr  15958  logbgcd1irraplemap  15960  binom4  15970  pellexlem2  15972  pellexlem3  15973  wilthlem1  15974  sgmval  15977  sgmppw  15986  1sgmprm  15988  mersenne  15991  perfectlem1  15993  perfectlem2  15994  perfect  15995  lgslem1  15999  lgsval  16003  lgsfvalg  16004  lgsval2lem  16009  lgsval4  16019  lgsneg  16023  lgsneg1  16024  lgsmod  16025  lgsdir2  16032  lgsdirprm  16033  lgsdilem2  16035  lgsdi  16036  lgsne0  16037  lgssq2  16040  lgsdirnn0  16046  lgsdinn0  16047  gausslemma2dlem1a  16057  gausslemma2dlem1f1o  16059  gausslemma2dlem2  16061  gausslemma2dlem3  16062  gausslemma2dlem4  16063  gausslemma2dlem5  16065  gausslemma2dlem6  16066  gausslemma2d  16068  lgseisenlem1  16069  lgseisenlem2  16070  lgseisenlem3  16071  lgseisenlem4  16072  lgsquadlem1  16076  lgsquadlem2  16077  lgsquadlem3  16078  lgsquad2lem1  16080  lgsquad2lem2  16081  lgsquad2  16082  lgsquad3  16083  m1lgs  16084  2lgslem3c  16094  2lgslem3d  16095  2lgslem3d1  16099  2sqlem2  16114  2sqlem3  16116  2sqlem4  16117  2sqlem8  16122  2sqlem9  16123  2sqlem10  16124  vtxdumgrfival  16419  p1evtxdeqfi  16433  p1evtxdp1fi  16434  iswlk  16444  upgr2wlkdc  16498  wlkres  16500  trlreslem  16510  isclwwlk  16515  clwwlkccatlem  16521  clwwlknp  16538  clwwlkn1  16539  clwwlkn2  16542  clwwlkext2edg  16543  clwwlknonex2lem1  16558  clwwlknonex2lem2  16559  clwwlknonex2  16560  iseupth  16568  eupth2lem3lem6fi  16592  eupth2lem3lem4fi  16594  depindlem1  16627  qdencn  16933  trilpolemclim  16946  trilpolemcl  16947  trilpolemisumle  16948  trilpolemeq1  16950  trilpolemlt1  16951  trilpo  16953  apdifflemf  16956  apdiff  16958  iswomni0  16962  redcwlpolemeq1  16965  redcwlpo  16966  nconstwlpolem0  16975  nconstwlpolemgt0  16976  nconstwlpo  16978  neapmkv  16980