Theorem oveq2 6066

Description: Equality theorem for operation value. (Contributed by NM, 28-Feb-1995.)

Assertion

Ref	Expression
oveq2	⊢ (𝐴 = 𝐵 → (𝐶𝐹𝐴) = (𝐶𝐹𝐵))

Proof of Theorem oveq2

Step	Hyp	Ref	Expression
1		opeq2 3889	. . 3 ⊢ (𝐴 = 𝐵 → ⟨𝐶, 𝐴⟩ = ⟨𝐶, 𝐵⟩)
2	1	fveq2d 5679	. 2 ⊢ (𝐴 = 𝐵 → (𝐹‘⟨𝐶, 𝐴⟩) = (𝐹‘⟨𝐶, 𝐵⟩))
3		df-ov 6061	. 2 ⊢ (𝐶𝐹𝐴) = (𝐹‘⟨𝐶, 𝐴⟩)
4		df-ov 6061	. 2 ⊢ (𝐶𝐹𝐵) = (𝐹‘⟨𝐶, 𝐵⟩)
5	2, 3, 4	3eqtr4g 2292	1 ⊢ (𝐴 = 𝐵 → (𝐶𝐹𝐴) = (𝐶𝐹𝐵))

Syntax hints:   → wi 4   = wceq 1398  ⟨cop 3697  ‘cfv 5357  (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:  oveq12  6067  oveq2i  6069  oveq2d  6074  ovanraleqv  6082  ovrspc2v  6084  oveqrspc2v  6085  rspceov  6101  fovcld  6166  ovmpos  6185  ov2gf  6186  ovi3  6199  caovclg  6215  caovcomg  6218  caovassg  6221  caovcang  6224  caovcan  6227  caovordig  6228  caovordg  6230  caovord  6234  caovdig  6237  caovdirg  6240  caovimo  6256  suppssov1  6272  off  6288  caofid0l  6302  caofid2  6305  caofdig  6309  suppofss1dcl  6477  suppofss2dcl  6478  omv  6701  oeiv  6702  oasuc  6710  oawordriexmid  6716  omsuc  6718  nna0r  6724  nnm0r  6725  nnacl  6726  nnmcl  6727  nnacom  6730  nnaass  6731  nndi  6732  nnmass  6733  nnmsucr  6734  nnmcom  6735  nnaordi  6754  nnaord  6755  nnmordi  6762  nnmord  6763  nnaordex  6774  nnawordex  6775  nnm00  6776  eroveu  6873  ecopovtrn  6879  ecopovtrng  6882  th3qlem2  6885  th3q  6887  ecovcom  6889  ecovicom  6890  ecovass  6891  ecoviass  6892  ecovdi  6893  ecovidi  6894  exmidpw2en  7185  mapfi  7227  acneq  7522  addcanpig  7665  mulcanpig  7666  addcmpblnq  7698  addclnq  7706  mulclnq  7707  recexnq  7721  recmulnqg  7722  ltanqg  7731  ltmnqg  7732  ltexnqq  7739  enq0ref  7764  enq0tr  7765  addcmpblnq0  7774  mulnnnq0  7781  addclnq0  7782  mulclnq0  7783  distrnq0  7790  mulcomnq0  7791  addassnq0  7793  nq02m  7796  prarloclem3  7828  genipv  7840  genpassl  7855  genpassu  7856  addlocpr  7867  distrlem1prl  7913  distrlem1pru  7914  1idprl  7921  1idpru  7922  ltexprlemell  7929  ltexprlemelu  7930  ltexpri  7944  lteupri  7948  ltaprlem  7949  recexprlem1ssl  7964  recexprlem1ssu  7965  recexpr  7969  cauappcvgprlemm  7976  cauappcvgprlemdisj  7982  cauappcvgprlemloc  7983  cauappcvgprlemladdru  7987  cauappcvgprlemladdrl  7988  cauappcvgprlem1  7990  cauappcvgprlemlim  7992  cauappcvgpr  7993  mulcmpblnrlemg  8071  addclsr  8084  mulclsr  8085  ltasrg  8101  negexsr  8103  recexgt0sr  8104  mulgt0sr  8109  mulextsr1  8112  srpospr  8114  caucvgsrlemgt1  8126  map2psrprg  8136  axaddrcl  8196  axmulrcl  8198  axaddcom  8201  axrnegex  8210  axprecex  8211  axcnre  8212  axpre-ltadd  8217  axpre-mulgt0  8218  axpre-mulext  8219  rereceu  8220  recriota  8221  axcaucvglemres  8230  readdcan  8429  cnegexlem1  8464  cnegex  8467  addcan  8469  negeq  8482  subadd  8492  addid0  8662  ine0  8684  rimul  8876  cru  8893  apreim  8894  recexap  8944  mulcanapd  8952  receuap  8960  divmulap  8966  rerecapb  9134  cju  9252  nnaddcl  9274  nnmulcl  9275  nnsub  9293  nnnn0addcl  9543  zaddcllempos  9631  zaddcl  9634  zdiv  9684  deceq1  9731  deceq2  9732  uzaddcl  9936  zq  9976  qreccl  9992  cnref1o  10001  xaddnemnf  10209  xaddnepnf  10210  xaddcom  10213  xnn0xadd0  10219  xnegdi  10220  xaddass  10221  xlt2add  10232  xlesubadd  10235  xleaddadd  10239  fzsuc2  10435  fzrevral  10461  fzshftral  10464  2ffzeq  10497  exfzdc  10608  exbtwnzlemshrink  10632  rebtwn2zlemshrink  10637  modqval  10710  modqmuladd  10752  modqmuladdnn0  10754  frecuzrdgrrn  10794  frec2uzrdg  10795  frecuzrdgrcl  10796  frecuzrdgsuc  10800  frecuzrdgrclt  10801  frecuzrdgg  10802  frecuzrdgsuctlem  10809  frecfzennn  10812  uzsinds  10830  iseqvalcbv  10845  seq3val  10846  seqvalcd  10847  seqovcd  10853  seq3caopr3  10877  seq3caopr2  10879  seqcaopr2g  10880  seq3f1olemp  10901  seqf1og  10907  seq3id  10911  seq3homo  10913  seq3z  10914  seqhomog  10916  seqfeq4g  10917  seq3distr  10918  expp1  10932  expnegap0  10933  expcllem  10936  expcl2lemap  10937  m1expcl2  10947  expap0  10955  mulexp  10964  expadd  10967  expmul  10970  leexp2r  10979  leexp1a  10980  bernneq  11047  expnbnd  11050  modqexp  11053  nn0ltexp2  11096  expcan  11103  apexp1  11105  facdiv  11125  faclbnd3  11130  faclbnd6  11131  bcval  11136  bcpasc  11153  bccl  11154  fz1eqb  11178  omgadd  11191  hashunlem  11193  hashfzo  11212  hashfzp1  11214  hashmap  11217  hashfibclem  11231  hashfibc  11232  iswrdinn0  11254  wrdnval  11280  eqwrd  11290  eqs1  11341  pfxeq  11413  ccatopth  11433  wrd2ind  11440  swrdccatin1  11442  swrdccatin2  11446  pfxccatin12lem2  11448  swrdccat3blem  11456  pfxccatid  11458  swrdccatin1d  11460  swrdccatin2d  11461  s2dmg  11507  shftfvalg  11528  shftfval  11531  cjth  11556  remim  11570  reim0b  11572  cjexp  11603  cnrecnv  11620  cvg1nlemcau  11694  cvg1nlemres  11695  recvguniq  11705  resqrexlemp1rp  11716  resqrexlemfp1  11719  resqrexlemlo  11723  resqrexlemgt0  11730  resqrexlemoverl  11731  resqrexlemglsq  11732  resqrexlemsqa  11734  resqrexlemex  11735  resqrex  11736  absexp  11789  recan  11819  climcn2  12019  subcn2  12021  summodc  12094  fsum3  12098  fsum3cvg3  12107  fsumrev  12154  fisum0diag2  12158  telfsumo  12177  fsumrelem  12182  binomlem  12194  binom  12195  binom1dif  12198  bcxmaslem1  12199  bcxmas  12200  isumshft  12201  divcnv  12208  arisum  12209  trireciplem  12211  expcnvap0  12213  expcnvre  12214  expcnv  12215  explecnv  12216  geosergap  12217  geolim  12222  geolim2  12223  geo2sum  12225  geo2lim  12227  geoisum  12228  geoisumr  12229  geoisum1  12230  geoisum1c  12231  cvgratnnlemsumlt  12239  cvgratz  12243  prodmodc  12289  fprodseq  12294  fprodcl2lem  12316  fprodfac  12326  fprodabs  12327  fprodrev  12330  eftvalcn  12368  efcvgfsum  12378  ege2le3  12382  efcj  12384  efaddlem  12385  efexp  12393  eftlub  12401  efgt1p2  12406  eflegeo  12412  sinval  12413  cosval  12414  demoivreALT  12485  divides  12500  dvdscmul  12529  dvds2ln  12535  dvdstr  12539  odd2np1lem  12583  odd2np1  12584  2tp1odd  12595  opeo  12608  omeo  12609  m1expe  12610  m1expo  12611  m1exp1  12612  divalglemnn  12629  divalglemeunn  12632  divalglemeuneg  12634  divalgmod  12638  ndvdssub  12641  bitsval  12654  bitsfzolem  12665  bitsinv1lem  12672  bitsinv1  12673  gcd0id  12700  bezoutlemnewy  12717  bezoutlema  12720  bezoutlemb  12721  bezoutlemex  12722  bezoutlemaz  12724  bezoutlembz  12725  gcdmultiple  12741  gcdmultiplez  12742  dvdsmulgcd  12746  rplpwr  12748  nn0seqcvgd  12763  dvdslcm  12791  lcmeq0  12793  lcmcl  12794  lcmneg  12796  lcmgcdlem  12799  lcmdvds  12801  lcmid  12802  lcmgcdeq  12805  coprmdvds  12814  mulgcddvds  12816  qredeq  12818  cncongr1  12825  cncongr2  12826  cncongrcoprm  12828  prmind2  12842  isprm6  12869  prmdvdsexp  12870  prmdvdsexpr  12872  sqrt2irr  12884  pw2dvdslemn  12887  pw2dvdseu  12890  oddpwdclemxy  12891  sqpweven  12897  2sqpwodd  12898  sqne2sq  12899  nn0gcdsq  12922  qden1elz  12927  phival  12935  dfphi2  12942  eulerthlemrprm  12951  eulerthlema  12952  prmdiv  12957  prmdiveq  12958  phisum  12963  odzval  12964  odzcllem  12965  odzdvds  12968  reumodprminv  12976  pythagtriplem3  12990  pythagtriplem18  13004  pythagtriplem19  13005  pclem0  13009  pclemub  13010  pclemdc  13011  pcprecl  13012  pcprendvds  13013  pcpremul  13016  pceulem  13017  pceu  13018  pczpre  13020  pcdiv  13025  pcqmul  13026  pcqcl  13029  pcexp  13032  pcxnn0cl  13033  pcxcl  13034  pcge0  13036  pcdvdsb  13043  pcneg  13048  pcabs  13049  pcgcd1  13051  pc2dvds  13053  pc11  13054  pcz  13055  pcprmpw2  13056  pcprmpw  13057  dvdsprmpweq  13058  dvdsprmpweqnn  13059  dvdsprmpweqle  13060  pcaddlem  13062  pcadd  13063  pcfac  13073  oddprmdvds  13077  prmpwdvds  13078  pockthi  13081  infpnlem2  13083  1arithlem1  13086  4sqlemffi  13119  4sqlem12  13125  2expltfac  13162  ballotfilemfval  13173  ballotfilemfc0  13176  ballotfilemfcc  13177  ballotfilemsv  13197  ballotfilemsf1o  13201  ballotfi  13226  ennnfonelemnn0  13257  ennnfonelemr  13258  f1ovscpbl  13576  imasaddvallemg  13579  ercpbl  13595  mgm1  13633  mgmidmo  13635  mgmlrid  13642  lidrideqd  13644  lidrididd  13645  grpinvalem  13648  grpinva  13649  gsumfzval  13654  gsumval2  13660  isnsgrp  13669  sgrpass  13671  sgrp1  13674  mndinvmod  13706  imasmnd2  13707  mnd1  13710  mnd1id  13711  mhmpropd  13721  mhmlin  13722  insubm  13740  mhmima  13746  gsumwsubmcl  13751  gsumwmhm  13753  grpinvex  13765  grppropd  13772  dfgrp2  13782  grpidd2  13796  grpinvval  13798  grpinvid1  13807  grplrinv  13812  grpidinv2  13813  grpidinv  13814  grplcan  13817  grpidssd  13831  grpinvssd  13832  dfgrp3mlem  13853  dfgrp3m  13854  grplactcnv  13857  grp1  13861  imasgrp2  13863  mhmlem  13867  mulgnn0gsum  13881  mulginvcom  13900  mulgnn0ass  13911  mulgmodid  13914  issubg  13926  issubg2m  13942  issubg4m  13946  isnsg2  13956  nsgbi  13957  isnsg3  13960  elnmz  13961  nmzbi  13962  ghmlin  14001  ghmrn  14010  ghmnsgima  14021  conjghm  14029  conjnmz  14032  gsumfzconst  14094  rngdi  14179  rngdir  14180  srglz  14228  srgisid  14229  srglmhm  14236  ringid  14269  ringinvnz1ne0  14292  ringinvnzdiv  14293  ring1  14302  ringlghm  14304  imasring  14307  dvdsrtr  14346  lringuplu  14441  issubrng  14445  issubrng2  14456  issubrg  14467  issubrg2  14487  rrgeq0i  14510  rrgeq0  14511  unitrrg  14514  domneq0  14519  lmodlema  14566  islmodd  14567  rmodislmodlem  14624  rmodislmod  14625  lssclg  14638  lss1d  14657  rnglidlmcl  14754  quscrng  14807  cnfldexp  14851  gsumfzfsumlemm  14861  cnfldui  14863  expghmap  14881  zrhval  14891  zrhvalg  14892  znunit  14933  txdis1cn  15269  cnmptcom  15289  psmettri2  15319  isxmet2d  15339  xmeteq0  15350  xmettri2  15352  elblps  15381  elbl  15382  blssps  15418  blss  15419  ssblex  15422  blin2  15423  metss2  15489  comet  15490  bdmopn  15495  txmetcnp  15509  blssioo  15544  divcnap  15556  mpomulcn  15557  expcn  15560  cncfval  15563  cncfi  15569  mulc1cncf  15580  cdivcncfap  15595  mulcncf  15599  expcncf  15600  cnopnap  15602  ellimc3apf  15651  cnlimci  15664  limccnpcntop  15666  limccnp2lem  15667  reldvg  15670  eldvap  15673  dvexp  15702  dvexp2  15703  dvrecap  15704  elplyr  15731  elplyd  15732  ply1termlem  15733  plymullem1  15739  plyadd  15742  plymul  15743  plycoeid3  15748  plycolemc  15749  plyco  15750  plycj  15752  dvply1  15756  dvply2g  15757  sin0pilem2  15773  rpcxpmul2  15904  relogbcxpbap  15956  logbgcd1irr  15958  2irrexpq  15967  2irrexpqap  15969  dvdsppwf1o  15983  mpodvdsmulf1o  15984  fsumdvdsmul  15985  sgmppw  15986  1sgmprm  15988  perfect  15995  lgsneg  16023  lgsdilem  16026  lgsdir  16034  lgsdilem2  16035  lgsdi  16036  lgsne0  16037  lgsdirnn0  16046  lgsdinn0  16047  gausslemma2dlem4  16063  lgseisenlem2  16070  lgseisenlem3  16071  lgseisenlem4  16072  lgsquadlem1  16076  lgsquadlem2  16077  lgsquad2lem2  16081  2lgs  16103  2sqlem6  16119  2sqlem8  16122  2sqlem9  16123  2sqlem10  16124  wlkeq  16475  wlkl1loop  16479  uspgr2wlkeq  16486  upgr2wlkdc  16498  clwwlknonmpo  16549  eupth2fi  16600  trilpolemclim  16946  trilpolemcl  16947  trilpolemisumle  16948  trilpolemeq1  16950  trilpolemlt1  16951  trilpo  16953  trirec0  16954  qdiff  16959  redcwlpo  16966  nconstwlpolemgt0  16976  nconstwlpo  16978  neapmkv  16980