Theorem oveq2 6058

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 3884	. . 3 ⊢ (𝐴 = 𝐵 → ⟨𝐶, 𝐴⟩ = ⟨𝐶, 𝐵⟩)
2	1	fveq2d 5674	. 2 ⊢ (𝐴 = 𝐵 → (𝐹‘⟨𝐶, 𝐴⟩) = (𝐹‘⟨𝐶, 𝐵⟩))
3		df-ov 6053	. 2 ⊢ (𝐶𝐹𝐴) = (𝐹‘⟨𝐶, 𝐴⟩)
4		df-ov 6053	. 2 ⊢ (𝐶𝐹𝐵) = (𝐹‘⟨𝐶, 𝐵⟩)
5	2, 3, 4	3eqtr4g 2290	1 ⊢ (𝐴 = 𝐵 → (𝐶𝐹𝐴) = (𝐶𝐹𝐵))

Syntax hints:   → wi 4   = wceq 1398  ⟨cop 3692  ‘cfv 5352  (class class class)co 6050

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 2214

This theorem depends on definitions:  df-bi 117  df-3an 1007  df-tru 1401  df-nf 1510  df-sb 1812  df-clab 2219  df-cleq 2225  df-clel 2228  df-nfc 2373  df-rex 2526  df-v 2815  df-un 3215  df-sn 3695  df-pr 3696  df-op 3698  df-uni 3915  df-br 4110  df-iota 5312  df-fv 5360  df-ov 6053

This theorem is referenced by:  oveq12  6059  oveq2i  6061  oveq2d  6066  ovanraleqv  6074  ovrspc2v  6076  oveqrspc2v  6077  rspceov  6093  fovcld  6158  ovmpos  6177  ov2gf  6178  ovi3  6191  caovclg  6207  caovcomg  6210  caovassg  6213  caovcang  6216  caovcan  6219  caovordig  6220  caovordg  6222  caovord  6226  caovdig  6229  caovdirg  6232  caovimo  6248  suppssov1  6263  off  6279  caofid0l  6293  caofid2  6296  caofdig  6300  suppofss1dcl  6464  suppofss2dcl  6465  omv  6688  oeiv  6689  oasuc  6697  oawordriexmid  6703  omsuc  6705  nna0r  6711  nnm0r  6712  nnacl  6713  nnmcl  6714  nnacom  6717  nnaass  6718  nndi  6719  nnmass  6720  nnmsucr  6721  nnmcom  6722  nnaordi  6741  nnaord  6742  nnmordi  6749  nnmord  6750  nnaordex  6761  nnawordex  6762  nnm00  6763  eroveu  6860  ecopovtrn  6866  ecopovtrng  6869  th3qlem2  6872  th3q  6874  ecovcom  6876  ecovicom  6877  ecovass  6878  ecoviass  6879  ecovdi  6880  ecovidi  6881  exmidpw2en  7172  mapfi  7214  acneq  7509  addcanpig  7649  mulcanpig  7650  addcmpblnq  7682  addclnq  7690  mulclnq  7691  recexnq  7705  recmulnqg  7706  ltanqg  7715  ltmnqg  7716  ltexnqq  7723  enq0ref  7748  enq0tr  7749  addcmpblnq0  7758  mulnnnq0  7765  addclnq0  7766  mulclnq0  7767  distrnq0  7774  mulcomnq0  7775  addassnq0  7777  nq02m  7780  prarloclem3  7812  genipv  7824  genpassl  7839  genpassu  7840  addlocpr  7851  distrlem1prl  7897  distrlem1pru  7898  1idprl  7905  1idpru  7906  ltexprlemell  7913  ltexprlemelu  7914  ltexpri  7928  lteupri  7932  ltaprlem  7933  recexprlem1ssl  7948  recexprlem1ssu  7949  recexpr  7953  cauappcvgprlemm  7960  cauappcvgprlemdisj  7966  cauappcvgprlemloc  7967  cauappcvgprlemladdru  7971  cauappcvgprlemladdrl  7972  cauappcvgprlem1  7974  cauappcvgprlemlim  7976  cauappcvgpr  7977  mulcmpblnrlemg  8055  addclsr  8068  mulclsr  8069  ltasrg  8085  negexsr  8087  recexgt0sr  8088  mulgt0sr  8093  mulextsr1  8096  srpospr  8098  caucvgsrlemgt1  8110  map2psrprg  8120  axaddrcl  8180  axmulrcl  8182  axaddcom  8185  axrnegex  8194  axprecex  8195  axcnre  8196  axpre-ltadd  8201  axpre-mulgt0  8202  axpre-mulext  8203  rereceu  8204  recriota  8205  axcaucvglemres  8214  readdcan  8413  cnegexlem1  8448  cnegex  8451  addcan  8453  negeq  8466  subadd  8476  addid0  8646  ine0  8667  rimul  8859  cru  8876  apreim  8877  recexap  8927  mulcanapd  8935  receuap  8943  divmulap  8949  rerecapb  9117  cju  9235  nnaddcl  9257  nnmulcl  9258  nnsub  9276  nnnn0addcl  9526  zaddcllempos  9614  zaddcl  9617  zdiv  9666  deceq1  9713  deceq2  9714  uzaddcl  9918  zq  9958  qreccl  9974  cnref1o  9983  xaddnemnf  10190  xaddnepnf  10191  xaddcom  10194  xnn0xadd0  10200  xnegdi  10201  xaddass  10202  xlt2add  10213  xlesubadd  10216  xleaddadd  10220  fzsuc2  10413  fzrevral  10439  fzshftral  10442  2ffzeq  10475  exfzdc  10586  exbtwnzlemshrink  10608  rebtwn2zlemshrink  10613  modqval  10686  modqmuladd  10728  modqmuladdnn0  10730  frecuzrdgrrn  10770  frec2uzrdg  10771  frecuzrdgrcl  10772  frecuzrdgsuc  10776  frecuzrdgrclt  10777  frecuzrdgg  10778  frecuzrdgsuctlem  10785  frecfzennn  10788  uzsinds  10806  iseqvalcbv  10821  seq3val  10822  seqvalcd  10823  seqovcd  10829  seq3caopr3  10853  seq3caopr2  10855  seqcaopr2g  10856  seq3f1olemp  10877  seqf1og  10883  seq3id  10887  seq3homo  10889  seq3z  10890  seqhomog  10892  seqfeq4g  10893  seq3distr  10894  expp1  10908  expnegap0  10909  expcllem  10912  expcl2lemap  10913  m1expcl2  10923  expap0  10931  mulexp  10940  expadd  10943  expmul  10946  leexp2r  10955  leexp1a  10956  bernneq  11022  expnbnd  11025  modqexp  11028  nn0ltexp2  11071  expcan  11078  apexp1  11080  facdiv  11100  faclbnd3  11105  faclbnd6  11106  bcval  11111  bcpasc  11128  bccl  11129  fz1eqb  11153  omgadd  11166  hashunlem  11168  hashfzo  11187  hashfzp1  11189  hashmap  11192  hashfibclem  11206  hashfibc  11207  iswrdinn0  11229  wrdnval  11255  eqwrd  11265  eqs1  11316  pfxeq  11388  ccatopth  11408  wrd2ind  11415  swrdccatin1  11417  swrdccatin2  11421  pfxccatin12lem2  11423  swrdccat3blem  11431  pfxccatid  11433  swrdccatin1d  11435  swrdccatin2d  11436  s2dmg  11482  shftfvalg  11503  shftfval  11506  cjth  11531  remim  11545  reim0b  11547  cjexp  11578  cnrecnv  11595  cvg1nlemcau  11669  cvg1nlemres  11670  recvguniq  11680  resqrexlemp1rp  11691  resqrexlemfp1  11694  resqrexlemlo  11698  resqrexlemgt0  11705  resqrexlemoverl  11706  resqrexlemglsq  11707  resqrexlemsqa  11709  resqrexlemex  11710  resqrex  11711  absexp  11764  recan  11794  climcn2  11994  subcn2  11996  summodc  12069  fsum3  12073  fsum3cvg3  12082  fsumrev  12129  fisum0diag2  12133  telfsumo  12152  fsumrelem  12157  binomlem  12169  binom  12170  binom1dif  12173  bcxmaslem1  12174  bcxmas  12175  isumshft  12176  divcnv  12183  arisum  12184  trireciplem  12186  expcnvap0  12188  expcnvre  12189  expcnv  12190  explecnv  12191  geosergap  12192  geolim  12197  geolim2  12198  geo2sum  12200  geo2lim  12202  geoisum  12203  geoisumr  12204  geoisum1  12205  geoisum1c  12206  cvgratnnlemsumlt  12214  cvgratz  12218  prodmodc  12264  fprodseq  12269  fprodcl2lem  12291  fprodfac  12301  fprodabs  12302  fprodrev  12305  eftvalcn  12343  efcvgfsum  12353  ege2le3  12357  efcj  12359  efaddlem  12360  efexp  12368  eftlub  12376  efgt1p2  12381  eflegeo  12387  sinval  12388  cosval  12389  demoivreALT  12460  divides  12475  dvdscmul  12504  dvds2ln  12510  dvdstr  12514  odd2np1lem  12558  odd2np1  12559  2tp1odd  12570  opeo  12583  omeo  12584  m1expe  12585  m1expo  12586  m1exp1  12587  divalglemnn  12604  divalglemeunn  12607  divalglemeuneg  12609  divalgmod  12613  ndvdssub  12616  bitsval  12629  bitsfzolem  12640  bitsinv1lem  12647  bitsinv1  12648  gcd0id  12675  bezoutlemnewy  12692  bezoutlema  12695  bezoutlemb  12696  bezoutlemex  12697  bezoutlemaz  12699  bezoutlembz  12700  gcdmultiple  12716  gcdmultiplez  12717  dvdsmulgcd  12721  rplpwr  12723  nn0seqcvgd  12738  dvdslcm  12766  lcmeq0  12768  lcmcl  12769  lcmneg  12771  lcmgcdlem  12774  lcmdvds  12776  lcmid  12777  lcmgcdeq  12780  coprmdvds  12789  mulgcddvds  12791  qredeq  12793  cncongr1  12800  cncongr2  12801  cncongrcoprm  12803  prmind2  12817  isprm6  12844  prmdvdsexp  12845  prmdvdsexpr  12847  sqrt2irr  12859  pw2dvdslemn  12862  pw2dvdseu  12865  oddpwdclemxy  12866  sqpweven  12872  2sqpwodd  12873  sqne2sq  12874  nn0gcdsq  12897  qden1elz  12902  phival  12910  dfphi2  12917  eulerthlemrprm  12926  eulerthlema  12927  prmdiv  12932  prmdiveq  12933  phisum  12938  odzval  12939  odzcllem  12940  odzdvds  12943  reumodprminv  12951  pythagtriplem3  12965  pythagtriplem18  12979  pythagtriplem19  12980  pclem0  12984  pclemub  12985  pclemdc  12986  pcprecl  12987  pcprendvds  12988  pcpremul  12991  pceulem  12992  pceu  12993  pczpre  12995  pcdiv  13000  pcqmul  13001  pcqcl  13004  pcexp  13007  pcxnn0cl  13008  pcxcl  13009  pcge0  13011  pcdvdsb  13018  pcneg  13023  pcabs  13024  pcgcd1  13026  pc2dvds  13028  pc11  13029  pcz  13030  pcprmpw2  13031  pcprmpw  13032  dvdsprmpweq  13033  dvdsprmpweqnn  13034  dvdsprmpweqle  13035  pcaddlem  13037  pcadd  13038  pcfac  13048  oddprmdvds  13052  prmpwdvds  13053  pockthi  13056  infpnlem2  13058  1arithlem1  13061  4sqlemffi  13094  4sqlem12  13100  2expltfac  13137  ennnfonelemnn0  13173  ennnfonelemr  13174  f1ovscpbl  13525  imasaddvallemg  13528  ercpbl  13544  mgm1  13583  mgmidmo  13585  mgmlrid  13592  lidrideqd  13594  lidrididd  13595  grpinvalem  13598  grpinva  13599  gsumfzval  13604  gsumval2  13610  isnsgrp  13619  sgrpass  13621  sgrp1  13624  mndinvmod  13658  imasmnd2  13665  mnd1  13668  mnd1id  13669  mhmpropd  13679  mhmlin  13680  insubm  13698  mhmima  13704  gsumwsubmcl  13709  gsumwmhm  13711  grpinvex  13723  grppropd  13730  dfgrp2  13740  grpidd2  13754  grpinvval  13756  grpinvid1  13765  grplrinv  13770  grpidinv2  13771  grpidinv  13772  grplcan  13775  grpidssd  13789  grpinvssd  13790  dfgrp3mlem  13811  dfgrp3m  13812  grplactcnv  13815  grp1  13819  imasgrp2  13827  mhmlem  13831  mulgnn0gsum  13845  mulginvcom  13864  mulgnn0ass  13875  mulgmodid  13878  issubg  13890  issubg2m  13906  issubg4m  13910  isnsg2  13920  nsgbi  13921  isnsg3  13924  elnmz  13925  nmzbi  13926  ghmlin  13965  ghmrn  13974  ghmnsgima  13985  conjghm  13993  conjnmz  13996  gsumfzconst  14058  rngdi  14084  rngdir  14085  srglz  14129  srgisid  14130  srglmhm  14137  ringid  14170  ringinvnz1ne0  14193  ringinvnzdiv  14194  ring1  14203  ringlghm  14205  imasring  14208  dvdsrtr  14246  lringuplu  14341  issubrng  14344  issubrng2  14355  issubrg  14366  issubrg2  14386  rrgeq0i  14409  rrgeq0  14410  unitrrg  14413  domneq0  14418  lmodlema  14440  islmodd  14441  rmodislmodlem  14498  rmodislmod  14499  lssclg  14512  lss1d  14531  rnglidlmcl  14628  quscrng  14681  cnfldexp  14725  gsumfzfsumlemm  14735  cnfldui  14737  expghmap  14755  zrhval  14765  zrhvalg  14766  znunit  14807  txdis1cn  15143  cnmptcom  15163  psmettri2  15193  isxmet2d  15213  xmeteq0  15224  xmettri2  15226  elblps  15255  elbl  15256  blssps  15292  blss  15293  ssblex  15296  blin2  15297  metss2  15363  comet  15364  bdmopn  15369  txmetcnp  15383  blssioo  15418  divcnap  15430  mpomulcn  15431  expcn  15434  cncfval  15437  cncfi  15443  mulc1cncf  15454  cdivcncfap  15469  mulcncf  15473  expcncf  15474  cnopnap  15476  ellimc3apf  15525  cnlimci  15538  limccnpcntop  15540  limccnp2lem  15541  reldvg  15544  eldvap  15547  dvexp  15576  dvexp2  15577  dvrecap  15578  elplyr  15605  elplyd  15606  ply1termlem  15607  plymullem1  15613  plyadd  15616  plymul  15617  plycoeid3  15622  plycolemc  15623  plyco  15624  plycj  15626  dvply1  15630  dvply2g  15631  sin0pilem2  15647  rpcxpmul2  15778  relogbcxpbap  15830  logbgcd1irr  15832  2irrexpq  15841  2irrexpqap  15843  dvdsppwf1o  15857  mpodvdsmulf1o  15858  fsumdvdsmul  15859  sgmppw  15860  1sgmprm  15862  perfect  15869  lgsneg  15897  lgsdilem  15900  lgsdir  15908  lgsdilem2  15909  lgsdi  15910  lgsne0  15911  lgsdirnn0  15920  lgsdinn0  15921  gausslemma2dlem4  15937  lgseisenlem2  15944  lgseisenlem3  15945  lgseisenlem4  15946  lgsquadlem1  15950  lgsquadlem2  15951  lgsquad2lem2  15955  2lgs  15977  2sqlem6  15993  2sqlem8  15996  2sqlem9  15997  2sqlem10  15998  wlkeq  16349  wlkl1loop  16353  uspgr2wlkeq  16360  upgr2wlkdc  16372  clwwlknonmpo  16423  eupth2fi  16474  trilpolemclim  16820  trilpolemcl  16821  trilpolemisumle  16822  trilpolemeq1  16824  trilpolemlt1  16825  trilpo  16827  trirec0  16828  qdiff  16833  redcwlpo  16840  nconstwlpolemgt0  16850  nconstwlpo  16852  neapmkv  16854