Theorem oveq2d 5893

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

Syntax hints:   → wi 4   = wceq 1353  (class class class)co 5877

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 709  ax-5 1447  ax-7 1448  ax-gen 1449  ax-ie1 1493  ax-ie2 1494  ax-8 1504  ax-10 1505  ax-11 1506  ax-i12 1507  ax-bndl 1509  ax-4 1510  ax-17 1526  ax-i9 1530  ax-ial 1534  ax-i5r 1535  ax-ext 2159

This theorem depends on definitions:  df-bi 117  df-3an 980  df-tru 1356  df-nf 1461  df-sb 1763  df-clab 2164  df-cleq 2170  df-clel 2173  df-nfc 2308  df-rex 2461  df-v 2741  df-un 3135  df-sn 3600  df-pr 3601  df-op 3603  df-uni 3812  df-br 4006  df-iota 5180  df-fv 5226  df-ov 5880

This theorem is referenced by:  csbov1g  5917  caovassg  6035  caovdig  6051  caovdirg  6054  caov32d  6057  caov4d  6061  caov42d  6063  nnaass  6488  nndi  6489  nnmass  6490  nnmsucr  6491  ecovass  6646  ecoviass  6647  ecovdi  6648  ecovidi  6649  addasspig  7331  mulasspig  7333  distrpig  7334  dfplpq2  7355  mulpipq2  7372  addassnqg  7383  prarloclemarch  7419  prarloclemarch2  7420  ltrnqg  7421  enq0sym  7433  addnq0mo  7448  mulnq0mo  7449  addnnnq0  7450  nq0a0  7458  distrnq0  7460  addassnq0  7463  prarloclemlo  7495  prarloclem3  7498  prarloclem5  7501  prarloclemcalc  7503  addnqprl  7530  addnqpru  7531  prmuloclemcalc  7566  mulnqprl  7569  mulnqpru  7570  distrlem4prl  7585  distrlem4pru  7586  1idprl  7591  1idpru  7592  ltexprlemloc  7608  addcanprleml  7615  addcanprlemu  7616  recexprlem1ssu  7635  ltmprr  7643  caucvgprlemcanl  7645  cauappcvgprlemladdru  7657  cauappcvgprlemladdrl  7658  cauappcvgprlem1  7660  cauappcvgprlemlim  7662  caucvgprlemnkj  7667  caucvgprlemnbj  7668  caucvgprlemdisj  7675  caucvgprlemloc  7676  caucvgprlemcl  7677  caucvgprlemladdrl  7679  caucvgprlem1  7680  caucvgpr  7683  caucvgprprlemell  7686  caucvgprprlemcbv  7688  caucvgprprlemval  7689  caucvgprprlemnkeqj  7691  caucvgprprlemopl  7698  caucvgprprlemlol  7699  caucvgprprlemloc  7704  caucvgprprlemclphr  7706  caucvgprprlemexb  7708  caucvgprprlemaddq  7709  caucvgprprlem1  7710  addcmpblnr  7740  mulcmpblnrlemg  7741  addsrmo  7744  mulsrmo  7745  addsrpr  7746  mulsrpr  7747  ltsrprg  7748  recexgt0sr  7774  mulgt0sr  7779  caucvgsrlemgt1  7796  caucvgsrlemoffval  7797  caucvgsr  7803  suplocsrlemb  7807  suplocsrlempr  7808  suplocsrlem  7809  suplocsr  7810  mulcnsr  7836  pitoregt0  7850  recidpirqlemcalc  7858  axmulcom  7872  axmulass  7874  axdistr  7875  ax0id  7879  axcnre  7882  recriota  7891  axcaucvglemcau  7899  axcaucvglemres  7900  mulrid  7956  adddirp1d  7986  mul32  8089  mul31  8090  add32  8118  add4  8120  add42  8121  cnegex  8137  addcan2  8140  addsubass  8169  subsub2  8187  nppcan2  8190  sub32  8193  nnncan  8194  sub4  8204  muladd  8343  subdi  8344  mul2neg  8357  submul2  8358  mulsub  8360  mulsubfacd  8377  add20  8433  recexre  8537  rereim  8545  apreap  8546  ltmul1  8551  cru  8561  apreim  8562  mulreim  8563  apadd1  8567  apneg  8570  mulap0  8613  divrecap  8647  divassap  8649  divmulasscomap  8655  divsubdirap  8667  divdivdivap  8672  divmul24ap  8675  divmuleqap  8676  divcanap6  8678  divdivap1  8682  divdivap2  8683  divsubdivap  8687  conjmulap  8688  div2negap  8694  apmul1  8747  cju  8920  nnmulcl  8942  add1p1  9170  sub1m1  9171  cnm2m1cnm3  9172  xp1d2m1eqxm1d2  9173  div4p1lem1div2  9174  un0addcl  9211  un0mulcl  9212  zaddcllemneg  9294  qapne  9641  cnref1o  9652  rexsub  9855  xnegid  9861  xaddcom  9863  xnegdi  9870  xaddass  9871  xaddass2  9872  xpncan  9873  xnpcan  9874  xleadd1a  9875  xsubge0  9883  xposdif  9884  xlesubadd  9885  xadd4d  9887  lincmb01cmp  10005  iccf1o  10006  ige3m2fz  10051  fztp  10080  fzsuc2  10081  fseq1m1p1  10097  fzm1  10102  ige2m1fz1  10111  nn0split  10138  nnsplit  10139  fzval3  10206  zpnn0elfzo1  10210  fzosplitsnm1  10211  fzosplitprm1  10236  fzoshftral  10240  rebtwn2zlemstep  10255  flhalf  10304  modqval  10326  modqvalr  10327  modqdiffl  10337  modqfrac  10339  flqmod  10340  intqfrac  10341  zmod10  10342  modqmulnn  10344  modqvalp1  10345  modqid  10351  modqcyc  10361  modqcyc2  10362  modqmul1  10379  q2submod  10387  modqdi  10394  modqsubdir  10395  modqeqmodmin  10396  modsumfzodifsn  10398  addmodlteq  10400  frecuzrdgsuctlem  10425  uzsinds  10444  seqeq3  10452  iseqvalcbv  10459  seq3val  10460  seqvalcd  10461  seqf  10463  seq3p1  10464  seqovcd  10465  seqp1cd  10468  seq3m1  10470  seq3fveq2  10471  seq3shft2  10475  monoord2  10479  ser3mono  10480  seq3split  10481  seq3caopr3  10483  seq3caopr2  10484  seq3caopr  10485  seq3id2  10511  seq3homo  10512  seq3z  10513  exp3vallem  10523  exp3val  10524  expp1  10529  expnegap0  10530  expineg2  10531  expn1ap0  10532  expm1t  10550  1exp  10551  expnegzap  10556  mulexpzap  10562  expadd  10564  expaddzaplem  10565  expaddzap  10566  expmul  10567  expmulzap  10568  m1expeven  10569  expsubap  10570  expp1zap  10571  expm1ap  10572  expdivap  10573  iexpcyc  10627  subsq2  10630  binom2  10634  binom21  10635  binom2sub  10636  binom2sub1  10637  mulbinom2  10639  binom3  10640  zesq  10641  bernneq  10643  sqoddm1div8  10676  mulsubdivbinom2ap  10693  nn0opthlem1d  10702  nn0opthd  10704  facp1  10712  facnn2  10716  faclbnd  10723  faclbnd6  10726  bcval  10731  bccmpl  10736  bcn0  10737  bcnn  10739  bcnp1n  10741  bcm1k  10742  bcp1n  10743  bcp1nk  10744  bcval5  10745  bcp1m1  10747  bcpasc  10748  bcn2m1  10751  bcn2p1  10752  omgadd  10784  hashunlem  10786  hashunsng  10789  hashdifsn  10801  hashxp  10808  zfz1isolemsplit  10820  zfz1isolem1  10822  zfz1iso  10823  seq3coll  10824  shftcan1  10845  shftcan2  10846  cjval  10856  cjth  10857  crre  10868  replim  10870  remim  10871  reim0b  10873  rereb  10874  mulreap  10875  cjreb  10877  recj  10878  reneg  10879  readd  10880  resub  10881  remullem  10882  imcj  10886  imneg  10887  imadd  10888  imsub  10889  cjcj  10894  cjadd  10895  ipcnval  10897  cjmulrcl  10898  cjneg  10901  addcj  10902  cjsub  10903  cnrecnv  10921  caucvgrelemcau  10991  cvg1nlemcau  10995  cvg1nlemres  10996  recvguniqlem  11005  resqrexlemover  11021  resqrexlemlo  11024  resqrexlemcalc1  11025  resqrexlemcalc3  11027  resqrexlemnm  11029  resqrexlemcvg  11030  absneg  11061  abscj  11063  sqabsadd  11066  sqabssub  11067  absmul  11080  absid  11082  absre  11088  absresq  11089  absexpzap  11091  recvalap  11108  abstri  11115  abs2dif2  11118  recan  11120  cau3lem  11125  amgm2  11129  bdtrilem  11249  xrmaxadd  11271  xrbdtri  11286  climaddc1  11339  climsubc1  11342  climcvg1nlem  11359  serf0  11362  summodclem3  11390  summodclem2a  11391  summodc  11393  fsumsplitsn  11420  fsumm1  11426  fsumsplitsnun  11429  fsump1  11430  isummulc2  11436  fsumrev  11453  fisum0diag2  11457  fsummulc2  11458  fsumsub  11462  fsumabs  11475  telfsumo  11476  fsumparts  11480  fsumrelem  11481  fsumiun  11487  binomlem  11493  binom  11494  binom1p  11495  binom11  11496  binom1dif  11497  bcxmas  11499  isumsplit  11501  isum1p  11502  divcnv  11507  arisum2  11509  trireciplem  11510  trirecip  11511  geolim  11521  georeclim  11523  geo2sum  11524  geo2lim  11526  geoisum1c  11530  0.999...  11531  cvgratnnlemnexp  11534  cvgratnnlemmn  11535  cvgratz  11542  mertenslem2  11546  mertensabs  11547  clim2prod  11549  prodfrecap  11556  prodfdivap  11557  prodmodclem3  11585  prodmodclem2a  11586  fprodm1  11608  fprodp1  11610  fprodunsn  11614  fprodfac  11625  fprodeq0  11627  fprodconst  11630  fprodrec  11639  fproddivap  11640  fprodsplitsn  11643  ege2le3  11681  efaddlem  11684  efsub  11691  efexp  11692  eftlub  11700  efsep  11701  effsumlt  11702  ef4p  11704  tanval3ap  11724  resinval  11725  recosval  11726  efi4p  11727  efival  11742  efmival  11743  efeul  11744  sinadd  11746  cosadd  11747  tanaddap  11749  sinsub  11750  cossub  11751  sincossq  11758  sin2t  11759  cos2t  11760  cos2tsin  11761  ef01bndlem  11766  sin01bnd  11767  cos01bnd  11768  cos12dec  11777  absef  11779  absefib  11780  efieq1re  11781  demoivreALT  11783  eirraplem  11786  dvdsexp  11869  oexpneg  11884  opeo  11904  omeo  11905  m1exp1  11908  flodddiv4  11941  flodddiv4t2lthalf  11944  divgcdnnr  11979  gcdaddm  11987  gcdadd  11988  gcdid  11989  modgcd  11994  gcdmultipled  11996  dvdsgcdidd  11997  bezoutlemnewy  11999  bezoutlema  12002  bezoutlemb  12003  bezoutlemex  12004  bezoutlembz  12007  absmulgcd  12020  gcdmultiple  12023  gcdmultiplez  12024  rpmulgcd  12029  rplpwr  12030  eucalginv  12058  eucalg  12061  lcmneg  12076  lcmgcdlem  12079  lcmgcd  12080  lcmid  12082  lcm1  12083  mulgcddvds  12096  qredeq  12098  divgcdcoprmex  12104  prmind2  12122  rpexp1i  12156  pw2dvdslemn  12167  pw2dvdseulemle  12169  pw2dvdseu  12170  oddpwdclemxy  12171  oddpwdclemdvds  12172  oddpwdclemndvds  12173  oddpwdclemdc  12175  2sqpwodd  12178  nn0gcdsq  12202  phiprmpw  12224  eulerthlemrprm  12231  eulerthlema  12232  eulerthlemh  12233  eulerthlemth  12234  fermltl  12236  prmdiv  12237  hashgcdlem  12240  odzdvds  12247  vfermltl  12253  modprm0  12256  nnnn0modprm0  12257  modprmn0modprm0  12258  coprimeprodsq  12259  pythagtriplem1  12267  pythagtriplem4  12270  pythagtriplem12  12277  pythagtriplem14  12279  pythagtriplem16  12281  pythagtriplem18  12283  pythagtrip  12285  pcpremul  12295  pceu  12297  pczpre  12299  pcdiv  12304  pcqmul  12305  pcqdiv  12309  pcexp  12311  pczdvds  12315  pczndvds  12317  pczndvds2  12319  pcid  12325  pcneg  12326  pcdvdstr  12328  pcgcd1  12329  pcgcd  12330  pc2dvds  12331  pcaddlem  12340  pcadd  12341  pcmpt  12343  pcmpt2  12344  fldivp1  12348  pcfac  12350  pcbc  12351  expnprm  12353  prmpwdvds  12355  pockthlem  12356  pockthi  12358  4sqlem7  12384  4sqlem9  12386  4sqlem10  12387  4sqlem2  12389  4sqlem3  12390  4sqlem4  12392  mul4sqlem  12393  setscomd  12505  ressvalsets  12526  strressid  12532  ressval3d  12533  ressinbasd  12535  ressressg  12536  ressabsg  12537  grprinvlem  12809  grprinvd  12810  grpridd  12811  isnsgrp  12817  sgrpass  12819  sgrp1  12821  mnd32g  12833  mnd4g  12835  mndpropd  12846  mhmlin  12863  grprcan  12915  grpsubval  12924  grpinvid2  12930  grpasscan2  12939  grpsubinv  12948  grpinvadd  12953  grpsubid1  12960  grpsubadd0sub  12962  grpsubadd  12963  grpsubsub  12964  grpaddsubass  12965  grppncan  12966  grpnnncan2  12972  grpsubpropd2  12980  mhmlem  12983  mhmid  12984  mhmmnd  12985  ghmgrp  12987  mulgnnp1  12996  mulgaddcomlem  13011  mulgaddcom  13012  mulginvinv  13014  mulgnn0dir  13018  mulgdirlem  13019  mulgp1  13021  mulgneg2  13022  mulgnn0ass  13024  mulgass  13025  mulgmodid  13027  mulgsubdir  13028  nmzsubg  13075  0nsg  13079  eqger  13088  ablsub4  13121  abladdsub4  13122  ablsubsub4  13127  ablsub32  13130  ablnnncan  13131  mgpress  13146  srgass  13159  srgpcomp  13178  srgpcompp  13179  srgpcomppsc  13180  srg1expzeq1  13183  ringpropd  13222  ringrz  13228  ringnegr  13234  ringmneg2  13236  ringsubdi  13238  ringsubdir  13239  ring1  13241  opprring  13254  mulgass3  13259  dvdsrd  13268  unitgrp  13290  invrfvald  13296  dvr1  13312  dvrass  13313  dvrcan1  13314  dvrcan3  13315  rdivmuldivd  13318  subrginv  13363  subrgdv  13364  islmod  13386  lmodlema  13387  islmodd  13388  lmodvs0  13417  lmodvneg1  13425  lmodvsubval2  13437  lmodsubvs  13438  lmodsubdi  13439  lmodsubdir  13440  lmodprop2d  13443  rmodislmodlem  13445  rmodislmod  13446  lsssn0  13461  cnfldsub  13508  restabs  13714  cnprcl2k  13745  cnrest2r  13776  ispsmet  13862  psmettri2  13867  psmetsym  13868  ismet  13883  isxmet  13884  xmettri2  13900  xmetsym  13907  xmettri3  13913  mettri3  13914  xblss2ps  13943  xblss2  13944  comet  14038  xmetxp  14046  xmetxpbl  14047  txmetcnp  14057  fsumcncntop  14095  cncfi  14104  limccl  14167  ellimc3apf  14168  limccnpcntop  14183  limccnp2lem  14184  reldvg  14187  dvfvalap  14189  eldvap  14190  dvcj  14212  dvfre  14213  dvexp  14214  dvexp2  14215  dvrecap  14216  dvmptaddx  14220  dvmptmulx  14221  dvmptnegcn  14223  dvmptsubcn  14224  dvmptcjx  14225  dveflem  14226  dvef  14227  sin0pilem1  14241  sin0pilem2  14242  efper  14267  sinperlem  14268  efimpi  14279  ptolemy  14284  tangtx  14298  abssinper  14306  cosq34lt1  14310  rpcxpef  14354  rpcxpp1  14366  rpcxpneg  14367  rpcxpsub  14368  rpmulcxp  14369  rpdivcxp  14371  cxpmul  14372  rpcxproot  14373  cxpcom  14396  rpabscxpbnd  14398  rplogbval  14402  rplogbreexp  14410  rplogbzexp  14411  rprelogbmulexp  14413  rprelogbdiv  14414  relogbexpap  14415  rplogbcxp  14420  rpcxplogb  14421  logbgcd1irr  14424  logbgcd1irraplemap  14426  binom4  14436  lgslem1  14440  lgsval  14444  lgsfvalg  14445  lgsval2lem  14450  lgsval4  14460  lgsneg  14464  lgsneg1  14465  lgsmod  14466  lgsdir2  14473  lgsdirprm  14474  lgsdilem2  14476  lgsdi  14477  lgsne0  14478  lgssq2  14481  lgsdirnn0  14487  lgsdinn0  14488  lgseisenlem1  14489  lgseisenlem2  14490  m1lgs  14491  2sqlem2  14501  2sqlem3  14503  2sqlem4  14504  2sqlem8  14509  2sqlem9  14510  2sqlem10  14511  qdencn  14814  trilpolemclim  14823  trilpolemcl  14824  trilpolemisumle  14825  trilpolemeq1  14827  trilpolemlt1  14828  trilpo  14830  apdifflemf  14833  apdiff  14835  iswomni0  14838  redcwlpolemeq1  14841  redcwlpo  14842  nconstwlpolem0  14850  nconstwlpolemgt0  14851  nconstwlpo  14853  neapmkv  14855