Theorem oveq2 5926

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 3805	. . 3 ⊢ (𝐴 = 𝐵 → ⟨𝐶, 𝐴⟩ = ⟨𝐶, 𝐵⟩)
2	1	fveq2d 5558	. 2 ⊢ (𝐴 = 𝐵 → (𝐹‘⟨𝐶, 𝐴⟩) = (𝐹‘⟨𝐶, 𝐵⟩))
3		df-ov 5921	. 2 ⊢ (𝐶𝐹𝐴) = (𝐹‘⟨𝐶, 𝐴⟩)
4		df-ov 5921	. 2 ⊢ (𝐶𝐹𝐵) = (𝐹‘⟨𝐶, 𝐵⟩)
5	2, 3, 4	3eqtr4g 2251	1 ⊢ (𝐴 = 𝐵 → (𝐶𝐹𝐴) = (𝐶𝐹𝐵))

Syntax hints:   → wi 4   = wceq 1364  ⟨cop 3621  ‘cfv 5254  (class class class)co 5918

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 1458  ax-7 1459  ax-gen 1460  ax-ie1 1504  ax-ie2 1505  ax-8 1515  ax-10 1516  ax-11 1517  ax-i12 1518  ax-bndl 1520  ax-4 1521  ax-17 1537  ax-i9 1541  ax-ial 1545  ax-i5r 1546  ax-ext 2175

This theorem depends on definitions:  df-bi 117  df-3an 982  df-tru 1367  df-nf 1472  df-sb 1774  df-clab 2180  df-cleq 2186  df-clel 2189  df-nfc 2325  df-rex 2478  df-v 2762  df-un 3157  df-sn 3624  df-pr 3625  df-op 3627  df-uni 3836  df-br 4030  df-iota 5215  df-fv 5262  df-ov 5921

This theorem is referenced by:  oveq12  5927  oveq2i  5929  oveq2d  5934  ovanraleqv  5942  ovrspc2v  5944  oveqrspc2v  5945  rspceov  5960  fovcld  6023  ovmpos  6042  ov2gf  6043  ovi3  6055  caovclg  6071  caovcomg  6074  caovassg  6077  caovcang  6080  caovcan  6083  caovordig  6084  caovordg  6086  caovord  6090  caovdig  6093  caovdirg  6096  caovimo  6112  suppssov1  6127  off  6143  caofdig  6159  omv  6508  oeiv  6509  oasuc  6517  oawordriexmid  6523  omsuc  6525  nna0r  6531  nnm0r  6532  nnacl  6533  nnmcl  6534  nnacom  6537  nnaass  6538  nndi  6539  nnmass  6540  nnmsucr  6541  nnmcom  6542  nnaordi  6561  nnaord  6562  nnmordi  6569  nnmord  6570  nnaordex  6581  nnawordex  6582  nnm00  6583  eroveu  6680  ecopovtrn  6686  ecopovtrng  6689  th3qlem2  6692  th3q  6694  ecovcom  6696  ecovicom  6697  ecovass  6698  ecoviass  6699  ecovdi  6700  ecovidi  6701  exmidpw2en  6968  addcanpig  7394  mulcanpig  7395  addcmpblnq  7427  addclnq  7435  mulclnq  7436  recexnq  7450  recmulnqg  7451  ltanqg  7460  ltmnqg  7461  ltexnqq  7468  enq0ref  7493  enq0tr  7494  addcmpblnq0  7503  mulnnnq0  7510  addclnq0  7511  mulclnq0  7512  distrnq0  7519  mulcomnq0  7520  addassnq0  7522  nq02m  7525  prarloclem3  7557  genipv  7569  genpassl  7584  genpassu  7585  addlocpr  7596  distrlem1prl  7642  distrlem1pru  7643  1idprl  7650  1idpru  7651  ltexprlemell  7658  ltexprlemelu  7659  ltexpri  7673  lteupri  7677  ltaprlem  7678  recexprlem1ssl  7693  recexprlem1ssu  7694  recexpr  7698  cauappcvgprlemm  7705  cauappcvgprlemdisj  7711  cauappcvgprlemloc  7712  cauappcvgprlemladdru  7716  cauappcvgprlemladdrl  7717  cauappcvgprlem1  7719  cauappcvgprlemlim  7721  cauappcvgpr  7722  mulcmpblnrlemg  7800  addclsr  7813  mulclsr  7814  ltasrg  7830  negexsr  7832  recexgt0sr  7833  mulgt0sr  7838  mulextsr1  7841  srpospr  7843  caucvgsrlemgt1  7855  map2psrprg  7865  axaddrcl  7925  axmulrcl  7927  axaddcom  7930  axrnegex  7939  axprecex  7940  axcnre  7941  axpre-ltadd  7946  axpre-mulgt0  7947  axpre-mulext  7948  rereceu  7949  recriota  7950  axcaucvglemres  7959  readdcan  8159  cnegexlem1  8194  cnegex  8197  addcan  8199  negeq  8212  subadd  8222  addid0  8392  ine0  8413  rimul  8604  cru  8621  apreim  8622  recexap  8672  mulcanapd  8680  receuap  8688  divmulap  8694  rerecapb  8862  cju  8980  nnaddcl  9002  nnmulcl  9003  nnsub  9021  nnnn0addcl  9270  zaddcllempos  9354  zaddcl  9357  zdiv  9405  deceq1  9452  deceq2  9453  uzaddcl  9651  zq  9691  qreccl  9707  cnref1o  9716  xaddnemnf  9923  xaddnepnf  9924  xaddcom  9927  xnn0xadd0  9933  xnegdi  9934  xaddass  9935  xlt2add  9946  xlesubadd  9949  xleaddadd  9953  fzsuc2  10145  fzrevral  10171  fzshftral  10174  2ffzeq  10207  exfzdc  10307  exbtwnzlemshrink  10317  rebtwn2zlemshrink  10322  modqval  10395  modqmuladd  10437  modqmuladdnn0  10439  frecuzrdgrrn  10479  frec2uzrdg  10480  frecuzrdgrcl  10481  frecuzrdgsuc  10485  frecuzrdgrclt  10486  frecuzrdgg  10487  frecuzrdgsuctlem  10494  frecfzennn  10497  uzsinds  10515  iseqvalcbv  10530  seq3val  10531  seqvalcd  10532  seqovcd  10538  seq3caopr3  10562  seq3caopr2  10564  seqcaopr2g  10565  seq3f1olemp  10586  seqf1og  10592  seq3id  10596  seq3homo  10598  seq3z  10599  seqhomog  10601  seqfeq4g  10602  seq3distr  10603  expp1  10617  expnegap0  10618  expcllem  10621  expcl2lemap  10622  m1expcl2  10632  expap0  10640  mulexp  10649  expadd  10652  expmul  10655  leexp2r  10664  leexp1a  10665  bernneq  10731  expnbnd  10734  modqexp  10737  nn0ltexp2  10780  expcan  10787  apexp1  10789  facdiv  10809  faclbnd3  10814  faclbnd6  10815  bcval  10820  bcpasc  10837  bccl  10838  fz1eqb  10861  omgadd  10873  hashunlem  10875  hashfzo  10893  hashfzp1  10895  iswrdinn0  10919  wrdnval  10944  eqwrd  10954  shftfvalg  10962  shftfval  10965  cjth  10990  remim  11004  reim0b  11006  cjexp  11037  cnrecnv  11054  cvg1nlemcau  11128  cvg1nlemres  11129  recvguniq  11139  resqrexlemp1rp  11150  resqrexlemfp1  11153  resqrexlemlo  11157  resqrexlemgt0  11164  resqrexlemoverl  11165  resqrexlemglsq  11166  resqrexlemsqa  11168  resqrexlemex  11169  resqrex  11170  absexp  11223  recan  11253  climcn2  11452  subcn2  11454  summodc  11526  fsum3  11530  fsum3cvg3  11539  fsumrev  11586  fisum0diag2  11590  telfsumo  11609  fsumrelem  11614  binomlem  11626  binom  11627  binom1dif  11630  bcxmaslem1  11631  bcxmas  11632  isumshft  11633  divcnv  11640  arisum  11641  trireciplem  11643  expcnvap0  11645  expcnvre  11646  expcnv  11647  explecnv  11648  geosergap  11649  geolim  11654  geolim2  11655  geo2sum  11657  geo2lim  11659  geoisum  11660  geoisumr  11661  geoisum1  11662  geoisum1c  11663  cvgratnnlemsumlt  11671  cvgratz  11675  prodmodc  11721  fprodseq  11726  fprodcl2lem  11748  fprodfac  11758  fprodabs  11759  fprodrev  11762  eftvalcn  11800  efcvgfsum  11810  ege2le3  11814  efcj  11816  efaddlem  11817  efexp  11825  eftlub  11833  efgt1p2  11838  eflegeo  11844  sinval  11845  cosval  11846  demoivreALT  11917  divides  11932  dvdscmul  11961  dvds2ln  11967  dvdstr  11971  odd2np1lem  12013  odd2np1  12014  2tp1odd  12025  opeo  12038  omeo  12039  m1expe  12040  m1expo  12041  m1exp1  12042  divalglemnn  12059  divalglemeunn  12062  divalglemeuneg  12064  divalgmod  12068  ndvdssub  12071  gcd0id  12116  bezoutlemnewy  12133  bezoutlema  12136  bezoutlemb  12137  bezoutlemex  12138  bezoutlemaz  12140  bezoutlembz  12141  gcdmultiple  12157  gcdmultiplez  12158  dvdsmulgcd  12162  rplpwr  12164  nn0seqcvgd  12179  dvdslcm  12207  lcmeq0  12209  lcmcl  12210  lcmneg  12212  lcmgcdlem  12215  lcmdvds  12217  lcmid  12218  lcmgcdeq  12221  coprmdvds  12230  mulgcddvds  12232  qredeq  12234  cncongr1  12241  cncongr2  12242  cncongrcoprm  12244  prmind2  12258  isprm6  12285  prmdvdsexp  12286  prmdvdsexpr  12288  sqrt2irr  12300  pw2dvdslemn  12303  pw2dvdseu  12306  oddpwdclemxy  12307  sqpweven  12313  2sqpwodd  12314  sqne2sq  12315  nn0gcdsq  12338  qden1elz  12343  phival  12351  dfphi2  12358  eulerthlemrprm  12367  eulerthlema  12368  prmdiv  12373  prmdiveq  12374  phisum  12378  odzval  12379  odzcllem  12380  odzdvds  12383  reumodprminv  12391  pythagtriplem3  12405  pythagtriplem18  12419  pythagtriplem19  12420  pclem0  12424  pclemub  12425  pclemdc  12426  pcprecl  12427  pcprendvds  12428  pcpremul  12431  pceulem  12432  pceu  12433  pczpre  12435  pcdiv  12440  pcqmul  12441  pcqcl  12444  pcexp  12447  pcxnn0cl  12448  pcxcl  12449  pcge0  12451  pcdvdsb  12458  pcneg  12463  pcabs  12464  pcgcd1  12466  pc2dvds  12468  pc11  12469  pcz  12470  pcprmpw2  12471  pcprmpw  12472  dvdsprmpweq  12473  dvdsprmpweqnn  12474  dvdsprmpweqle  12475  pcaddlem  12477  pcadd  12478  pcfac  12488  oddprmdvds  12492  prmpwdvds  12493  pockthi  12496  infpnlem2  12498  1arithlem1  12501  4sqlemffi  12534  4sqlem12  12540  ennnfonelemnn0  12579  ennnfonelemr  12580  f1ovscpbl  12895  imasaddvallemg  12898  ercpbl  12914  mgm1  12953  mgmidmo  12955  mgmlrid  12962  lidrideqd  12964  lidrididd  12965  grpinvalem  12968  grpinva  12969  gsumfzval  12974  gsumval2  12980  isnsgrp  12989  sgrpass  12991  sgrp1  12994  mndinvmod  13026  mnd1  13027  mnd1id  13028  mhmpropd  13038  mhmlin  13039  insubm  13057  mhmima  13063  gsumwsubmcl  13068  gsumwmhm  13070  grpinvex  13082  grppropd  13089  dfgrp2  13099  grpidd2  13113  grpinvval  13115  grpinvid1  13124  grplrinv  13129  grpidinv2  13130  grpidinv  13131  grplcan  13134  grpidssd  13148  grpinvssd  13149  dfgrp3mlem  13170  dfgrp3m  13171  grplactcnv  13174  grp1  13178  imasgrp2  13180  mhmlem  13184  mulgnn0gsum  13198  mulginvcom  13217  mulgnn0ass  13228  mulgmodid  13231  issubg  13243  issubg2m  13259  issubg4m  13263  isnsg2  13273  nsgbi  13274  isnsg3  13277  elnmz  13278  nmzbi  13279  ghmlin  13318  ghmrn  13327  ghmnsgima  13338  conjghm  13346  conjnmz  13349  gsumfzconst  13411  rngdi  13436  rngdir  13437  srglz  13481  srgisid  13482  srglmhm  13489  ringid  13522  ringinvnz1ne0  13545  ringinvnzdiv  13546  ring1  13555  ringlghm  13557  imasring  13560  dvdsrtr  13597  lringuplu  13692  issubrng  13695  issubrng2  13706  issubrg  13717  issubrg2  13737  rrgeq0i  13760  rrgeq0  13761  unitrrg  13763  domneq0  13768  lmodlema  13788  islmodd  13789  rmodislmodlem  13846  rmodislmod  13847  lssclg  13860  lss1d  13879  rnglidlmcl  13976  quscrng  14029  cnfldexp  14065  gsumfzfsumlemm  14075  cnfldui  14077  expghmap  14095  zrhval  14105  zrhvalg  14106  znunit  14147  txdis1cn  14446  cnmptcom  14466  psmettri2  14496  isxmet2d  14516  xmeteq0  14527  xmettri2  14529  elblps  14558  elbl  14559  blssps  14595  blss  14596  ssblex  14599  blin2  14600  metss2  14666  comet  14667  bdmopn  14672  txmetcnp  14686  blssioo  14713  divcnap  14723  cncfval  14727  cncfi  14733  mulc1cncf  14744  cdivcncfap  14758  mulcncf  14762  expcncf  14763  cnopnap  14765  ellimc3apf  14814  cnlimci  14827  limccnpcntop  14829  limccnp2lem  14830  reldvg  14833  eldvap  14836  dvexp  14860  dvexp2  14861  dvrecap  14862  elplyr  14886  elplyd  14887  ply1termlem  14888  plymullem1  14894  plyadd  14897  plymul  14898  sin0pilem2  14917  relogbcxpbap  15097  logbgcd1irr  15099  2irrexpq  15108  2irrexpqap  15110  lgsneg  15140  lgsdilem  15143  lgsdir  15151  lgsdilem2  15152  lgsdi  15153  lgsne0  15154  lgsdirnn0  15163  lgsdinn0  15164  gausslemma2dlem4  15180  lgseisenlem2  15187  lgseisenlem3  15188  lgseisenlem4  15189  lgsquadlem1  15191  2sqlem6  15207  2sqlem8  15210  2sqlem9  15211  2sqlem10  15212  trilpolemclim  15526  trilpolemcl  15527  trilpolemisumle  15528  trilpolemeq1  15530  trilpolemlt1  15531  trilpo  15533  trirec0  15534  redcwlpo  15545  nconstwlpolemgt0  15554  nconstwlpo  15556  neapmkv  15558