Theorem oveq2 5933

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 3810	. . 3 ⊢ (𝐴 = 𝐵 → ⟨𝐶, 𝐴⟩ = ⟨𝐶, 𝐵⟩)
2	1	fveq2d 5565	. 2 ⊢ (𝐴 = 𝐵 → (𝐹‘⟨𝐶, 𝐴⟩) = (𝐹‘⟨𝐶, 𝐵⟩))
3		df-ov 5928	. 2 ⊢ (𝐶𝐹𝐴) = (𝐹‘⟨𝐶, 𝐴⟩)
4		df-ov 5928	. 2 ⊢ (𝐶𝐹𝐵) = (𝐹‘⟨𝐶, 𝐵⟩)
5	2, 3, 4	3eqtr4g 2254	1 ⊢ (𝐴 = 𝐵 → (𝐶𝐹𝐴) = (𝐶𝐹𝐵))

Syntax hints:   → wi 4   = wceq 1364  ⟨cop 3626  ‘cfv 5259  (class class class)co 5925

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 1461  ax-7 1462  ax-gen 1463  ax-ie1 1507  ax-ie2 1508  ax-8 1518  ax-10 1519  ax-11 1520  ax-i12 1521  ax-bndl 1523  ax-4 1524  ax-17 1540  ax-i9 1544  ax-ial 1548  ax-i5r 1549  ax-ext 2178

This theorem depends on definitions:  df-bi 117  df-3an 982  df-tru 1367  df-nf 1475  df-sb 1777  df-clab 2183  df-cleq 2189  df-clel 2192  df-nfc 2328  df-rex 2481  df-v 2765  df-un 3161  df-sn 3629  df-pr 3630  df-op 3632  df-uni 3841  df-br 4035  df-iota 5220  df-fv 5267  df-ov 5928

This theorem is referenced by:  oveq12  5934  oveq2i  5936  oveq2d  5941  ovanraleqv  5949  ovrspc2v  5951  oveqrspc2v  5952  rspceov  5968  fovcld  6031  ovmpos  6050  ov2gf  6051  ovi3  6064  caovclg  6080  caovcomg  6083  caovassg  6086  caovcang  6089  caovcan  6092  caovordig  6093  caovordg  6095  caovord  6099  caovdig  6102  caovdirg  6105  caovimo  6121  suppssov1  6136  off  6152  caofid0l  6166  caofid2  6169  caofdig  6173  omv  6522  oeiv  6523  oasuc  6531  oawordriexmid  6537  omsuc  6539  nna0r  6545  nnm0r  6546  nnacl  6547  nnmcl  6548  nnacom  6551  nnaass  6552  nndi  6553  nnmass  6554  nnmsucr  6555  nnmcom  6556  nnaordi  6575  nnaord  6576  nnmordi  6583  nnmord  6584  nnaordex  6595  nnawordex  6596  nnm00  6597  eroveu  6694  ecopovtrn  6700  ecopovtrng  6703  th3qlem2  6706  th3q  6708  ecovcom  6710  ecovicom  6711  ecovass  6712  ecoviass  6713  ecovdi  6714  ecovidi  6715  exmidpw2en  6982  acneq  7285  addcanpig  7418  mulcanpig  7419  addcmpblnq  7451  addclnq  7459  mulclnq  7460  recexnq  7474  recmulnqg  7475  ltanqg  7484  ltmnqg  7485  ltexnqq  7492  enq0ref  7517  enq0tr  7518  addcmpblnq0  7527  mulnnnq0  7534  addclnq0  7535  mulclnq0  7536  distrnq0  7543  mulcomnq0  7544  addassnq0  7546  nq02m  7549  prarloclem3  7581  genipv  7593  genpassl  7608  genpassu  7609  addlocpr  7620  distrlem1prl  7666  distrlem1pru  7667  1idprl  7674  1idpru  7675  ltexprlemell  7682  ltexprlemelu  7683  ltexpri  7697  lteupri  7701  ltaprlem  7702  recexprlem1ssl  7717  recexprlem1ssu  7718  recexpr  7722  cauappcvgprlemm  7729  cauappcvgprlemdisj  7735  cauappcvgprlemloc  7736  cauappcvgprlemladdru  7740  cauappcvgprlemladdrl  7741  cauappcvgprlem1  7743  cauappcvgprlemlim  7745  cauappcvgpr  7746  mulcmpblnrlemg  7824  addclsr  7837  mulclsr  7838  ltasrg  7854  negexsr  7856  recexgt0sr  7857  mulgt0sr  7862  mulextsr1  7865  srpospr  7867  caucvgsrlemgt1  7879  map2psrprg  7889  axaddrcl  7949  axmulrcl  7951  axaddcom  7954  axrnegex  7963  axprecex  7964  axcnre  7965  axpre-ltadd  7970  axpre-mulgt0  7971  axpre-mulext  7972  rereceu  7973  recriota  7974  axcaucvglemres  7983  readdcan  8183  cnegexlem1  8218  cnegex  8221  addcan  8223  negeq  8236  subadd  8246  addid0  8416  ine0  8437  rimul  8629  cru  8646  apreim  8647  recexap  8697  mulcanapd  8705  receuap  8713  divmulap  8719  rerecapb  8887  cju  9005  nnaddcl  9027  nnmulcl  9028  nnsub  9046  nnnn0addcl  9296  zaddcllempos  9380  zaddcl  9383  zdiv  9431  deceq1  9478  deceq2  9479  uzaddcl  9677  zq  9717  qreccl  9733  cnref1o  9742  xaddnemnf  9949  xaddnepnf  9950  xaddcom  9953  xnn0xadd0  9959  xnegdi  9960  xaddass  9961  xlt2add  9972  xlesubadd  9975  xleaddadd  9979  fzsuc2  10171  fzrevral  10197  fzshftral  10200  2ffzeq  10233  exfzdc  10333  exbtwnzlemshrink  10355  rebtwn2zlemshrink  10360  modqval  10433  modqmuladd  10475  modqmuladdnn0  10477  frecuzrdgrrn  10517  frec2uzrdg  10518  frecuzrdgrcl  10519  frecuzrdgsuc  10523  frecuzrdgrclt  10524  frecuzrdgg  10525  frecuzrdgsuctlem  10532  frecfzennn  10535  uzsinds  10553  iseqvalcbv  10568  seq3val  10569  seqvalcd  10570  seqovcd  10576  seq3caopr3  10600  seq3caopr2  10602  seqcaopr2g  10603  seq3f1olemp  10624  seqf1og  10630  seq3id  10634  seq3homo  10636  seq3z  10637  seqhomog  10639  seqfeq4g  10640  seq3distr  10641  expp1  10655  expnegap0  10656  expcllem  10659  expcl2lemap  10660  m1expcl2  10670  expap0  10678  mulexp  10687  expadd  10690  expmul  10693  leexp2r  10702  leexp1a  10703  bernneq  10769  expnbnd  10772  modqexp  10775  nn0ltexp2  10818  expcan  10825  apexp1  10827  facdiv  10847  faclbnd3  10852  faclbnd6  10853  bcval  10858  bcpasc  10875  bccl  10876  fz1eqb  10899  omgadd  10911  hashunlem  10913  hashfzo  10931  hashfzp1  10933  iswrdinn0  10957  wrdnval  10982  eqwrd  10992  shftfvalg  11000  shftfval  11003  cjth  11028  remim  11042  reim0b  11044  cjexp  11075  cnrecnv  11092  cvg1nlemcau  11166  cvg1nlemres  11167  recvguniq  11177  resqrexlemp1rp  11188  resqrexlemfp1  11191  resqrexlemlo  11195  resqrexlemgt0  11202  resqrexlemoverl  11203  resqrexlemglsq  11204  resqrexlemsqa  11206  resqrexlemex  11207  resqrex  11208  absexp  11261  recan  11291  climcn2  11491  subcn2  11493  summodc  11565  fsum3  11569  fsum3cvg3  11578  fsumrev  11625  fisum0diag2  11629  telfsumo  11648  fsumrelem  11653  binomlem  11665  binom  11666  binom1dif  11669  bcxmaslem1  11670  bcxmas  11671  isumshft  11672  divcnv  11679  arisum  11680  trireciplem  11682  expcnvap0  11684  expcnvre  11685  expcnv  11686  explecnv  11687  geosergap  11688  geolim  11693  geolim2  11694  geo2sum  11696  geo2lim  11698  geoisum  11699  geoisumr  11700  geoisum1  11701  geoisum1c  11702  cvgratnnlemsumlt  11710  cvgratz  11714  prodmodc  11760  fprodseq  11765  fprodcl2lem  11787  fprodfac  11797  fprodabs  11798  fprodrev  11801  eftvalcn  11839  efcvgfsum  11849  ege2le3  11853  efcj  11855  efaddlem  11856  efexp  11864  eftlub  11872  efgt1p2  11877  eflegeo  11883  sinval  11884  cosval  11885  demoivreALT  11956  divides  11971  dvdscmul  12000  dvds2ln  12006  dvdstr  12010  odd2np1lem  12054  odd2np1  12055  2tp1odd  12066  opeo  12079  omeo  12080  m1expe  12081  m1expo  12082  m1exp1  12083  divalglemnn  12100  divalglemeunn  12103  divalglemeuneg  12105  divalgmod  12109  ndvdssub  12112  bitsval  12125  bitsfzolem  12136  bitsinv1lem  12143  bitsinv1  12144  gcd0id  12171  bezoutlemnewy  12188  bezoutlema  12191  bezoutlemb  12192  bezoutlemex  12193  bezoutlemaz  12195  bezoutlembz  12196  gcdmultiple  12212  gcdmultiplez  12213  dvdsmulgcd  12217  rplpwr  12219  nn0seqcvgd  12234  dvdslcm  12262  lcmeq0  12264  lcmcl  12265  lcmneg  12267  lcmgcdlem  12270  lcmdvds  12272  lcmid  12273  lcmgcdeq  12276  coprmdvds  12285  mulgcddvds  12287  qredeq  12289  cncongr1  12296  cncongr2  12297  cncongrcoprm  12299  prmind2  12313  isprm6  12340  prmdvdsexp  12341  prmdvdsexpr  12343  sqrt2irr  12355  pw2dvdslemn  12358  pw2dvdseu  12361  oddpwdclemxy  12362  sqpweven  12368  2sqpwodd  12369  sqne2sq  12370  nn0gcdsq  12393  qden1elz  12398  phival  12406  dfphi2  12413  eulerthlemrprm  12422  eulerthlema  12423  prmdiv  12428  prmdiveq  12429  phisum  12434  odzval  12435  odzcllem  12436  odzdvds  12439  reumodprminv  12447  pythagtriplem3  12461  pythagtriplem18  12475  pythagtriplem19  12476  pclem0  12480  pclemub  12481  pclemdc  12482  pcprecl  12483  pcprendvds  12484  pcpremul  12487  pceulem  12488  pceu  12489  pczpre  12491  pcdiv  12496  pcqmul  12497  pcqcl  12500  pcexp  12503  pcxnn0cl  12504  pcxcl  12505  pcge0  12507  pcdvdsb  12514  pcneg  12519  pcabs  12520  pcgcd1  12522  pc2dvds  12524  pc11  12525  pcz  12526  pcprmpw2  12527  pcprmpw  12528  dvdsprmpweq  12529  dvdsprmpweqnn  12530  dvdsprmpweqle  12531  pcaddlem  12533  pcadd  12534  pcfac  12544  oddprmdvds  12548  prmpwdvds  12549  pockthi  12552  infpnlem2  12554  1arithlem1  12557  4sqlemffi  12590  4sqlem12  12596  2expltfac  12633  ennnfonelemnn0  12664  ennnfonelemr  12665  f1ovscpbl  13014  imasaddvallemg  13017  ercpbl  13033  mgm1  13072  mgmidmo  13074  mgmlrid  13081  lidrideqd  13083  lidrididd  13084  grpinvalem  13087  grpinva  13088  gsumfzval  13093  gsumval2  13099  isnsgrp  13108  sgrpass  13110  sgrp1  13113  mndinvmod  13147  imasmnd2  13154  mnd1  13157  mnd1id  13158  mhmpropd  13168  mhmlin  13169  insubm  13187  mhmima  13193  gsumwsubmcl  13198  gsumwmhm  13200  grpinvex  13212  grppropd  13219  dfgrp2  13229  grpidd2  13243  grpinvval  13245  grpinvid1  13254  grplrinv  13259  grpidinv2  13260  grpidinv  13261  grplcan  13264  grpidssd  13278  grpinvssd  13279  dfgrp3mlem  13300  dfgrp3m  13301  grplactcnv  13304  grp1  13308  imasgrp2  13316  mhmlem  13320  mulgnn0gsum  13334  mulginvcom  13353  mulgnn0ass  13364  mulgmodid  13367  issubg  13379  issubg2m  13395  issubg4m  13399  isnsg2  13409  nsgbi  13410  isnsg3  13413  elnmz  13414  nmzbi  13415  ghmlin  13454  ghmrn  13463  ghmnsgima  13474  conjghm  13482  conjnmz  13485  gsumfzconst  13547  rngdi  13572  rngdir  13573  srglz  13617  srgisid  13618  srglmhm  13625  ringid  13658  ringinvnz1ne0  13681  ringinvnzdiv  13682  ring1  13691  ringlghm  13693  imasring  13696  dvdsrtr  13733  lringuplu  13828  issubrng  13831  issubrng2  13842  issubrg  13853  issubrg2  13873  rrgeq0i  13896  rrgeq0  13897  unitrrg  13899  domneq0  13904  lmodlema  13924  islmodd  13925  rmodislmodlem  13982  rmodislmod  13983  lssclg  13996  lss1d  14015  rnglidlmcl  14112  quscrng  14165  cnfldexp  14209  gsumfzfsumlemm  14219  cnfldui  14221  expghmap  14239  zrhval  14249  zrhvalg  14250  znunit  14291  txdis1cn  14598  cnmptcom  14618  psmettri2  14648  isxmet2d  14668  xmeteq0  14679  xmettri2  14681  elblps  14710  elbl  14711  blssps  14747  blss  14748  ssblex  14751  blin2  14752  metss2  14818  comet  14819  bdmopn  14824  txmetcnp  14838  blssioo  14873  divcnap  14885  mpomulcn  14886  expcn  14889  cncfval  14892  cncfi  14898  mulc1cncf  14909  cdivcncfap  14924  mulcncf  14928  expcncf  14929  cnopnap  14931  ellimc3apf  14980  cnlimci  14993  limccnpcntop  14995  limccnp2lem  14996  reldvg  14999  eldvap  15002  dvexp  15031  dvexp2  15032  dvrecap  15033  elplyr  15060  elplyd  15061  ply1termlem  15062  plymullem1  15068  plyadd  15071  plymul  15072  plycoeid3  15077  plycolemc  15078  plyco  15079  plycj  15081  dvply1  15085  dvply2g  15086  sin0pilem2  15102  rpcxpmul2  15233  relogbcxpbap  15285  logbgcd1irr  15287  2irrexpq  15296  2irrexpqap  15298  dvdsppwf1o  15309  mpodvdsmulf1o  15310  fsumdvdsmul  15311  sgmppw  15312  1sgmprm  15314  perfect  15321  lgsneg  15349  lgsdilem  15352  lgsdir  15360  lgsdilem2  15361  lgsdi  15362  lgsne0  15363  lgsdirnn0  15372  lgsdinn0  15373  gausslemma2dlem4  15389  lgseisenlem2  15396  lgseisenlem3  15397  lgseisenlem4  15398  lgsquadlem1  15402  lgsquadlem2  15403  lgsquad2lem2  15407  2lgs  15429  2sqlem6  15445  2sqlem8  15448  2sqlem9  15449  2sqlem10  15450  trilpolemclim  15767  trilpolemcl  15768  trilpolemisumle  15769  trilpolemeq1  15771  trilpolemlt1  15772  trilpo  15774  trirec0  15775  redcwlpo  15786  nconstwlpolemgt0  15795  nconstwlpo  15797  neapmkv  15799