Theorem oveq2 6015

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 3858	. . 3 ⊢ (𝐴 = 𝐵 → ⟨𝐶, 𝐴⟩ = ⟨𝐶, 𝐵⟩)
2	1	fveq2d 5633	. 2 ⊢ (𝐴 = 𝐵 → (𝐹‘⟨𝐶, 𝐴⟩) = (𝐹‘⟨𝐶, 𝐵⟩))
3		df-ov 6010	. 2 ⊢ (𝐶𝐹𝐴) = (𝐹‘⟨𝐶, 𝐴⟩)
4		df-ov 6010	. 2 ⊢ (𝐶𝐹𝐵) = (𝐹‘⟨𝐶, 𝐵⟩)
5	2, 3, 4	3eqtr4g 2287	1 ⊢ (𝐴 = 𝐵 → (𝐶𝐹𝐴) = (𝐶𝐹𝐵))

Syntax hints:   → wi 4   = wceq 1395  ⟨cop 3669  ‘cfv 5318  (class class class)co 6007

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 714  ax-5 1493  ax-7 1494  ax-gen 1495  ax-ie1 1539  ax-ie2 1540  ax-8 1550  ax-10 1551  ax-11 1552  ax-i12 1553  ax-bndl 1555  ax-4 1556  ax-17 1572  ax-i9 1576  ax-ial 1580  ax-i5r 1581  ax-ext 2211

This theorem depends on definitions:  df-bi 117  df-3an 1004  df-tru 1398  df-nf 1507  df-sb 1809  df-clab 2216  df-cleq 2222  df-clel 2225  df-nfc 2361  df-rex 2514  df-v 2801  df-un 3201  df-sn 3672  df-pr 3673  df-op 3675  df-uni 3889  df-br 4084  df-iota 5278  df-fv 5326  df-ov 6010

This theorem is referenced by:  oveq12  6016  oveq2i  6018  oveq2d  6023  ovanraleqv  6031  ovrspc2v  6033  oveqrspc2v  6034  rspceov  6050  fovcld  6115  ovmpos  6134  ov2gf  6135  ovi3  6148  caovclg  6164  caovcomg  6167  caovassg  6170  caovcang  6173  caovcan  6176  caovordig  6177  caovordg  6179  caovord  6183  caovdig  6186  caovdirg  6189  caovimo  6205  suppssov1  6221  off  6237  caofid0l  6251  caofid2  6254  caofdig  6258  omv  6609  oeiv  6610  oasuc  6618  oawordriexmid  6624  omsuc  6626  nna0r  6632  nnm0r  6633  nnacl  6634  nnmcl  6635  nnacom  6638  nnaass  6639  nndi  6640  nnmass  6641  nnmsucr  6642  nnmcom  6643  nnaordi  6662  nnaord  6663  nnmordi  6670  nnmord  6671  nnaordex  6682  nnawordex  6683  nnm00  6684  eroveu  6781  ecopovtrn  6787  ecopovtrng  6790  th3qlem2  6793  th3q  6795  ecovcom  6797  ecovicom  6798  ecovass  6799  ecoviass  6800  ecovdi  6801  ecovidi  6802  exmidpw2en  7085  acneq  7395  addcanpig  7532  mulcanpig  7533  addcmpblnq  7565  addclnq  7573  mulclnq  7574  recexnq  7588  recmulnqg  7589  ltanqg  7598  ltmnqg  7599  ltexnqq  7606  enq0ref  7631  enq0tr  7632  addcmpblnq0  7641  mulnnnq0  7648  addclnq0  7649  mulclnq0  7650  distrnq0  7657  mulcomnq0  7658  addassnq0  7660  nq02m  7663  prarloclem3  7695  genipv  7707  genpassl  7722  genpassu  7723  addlocpr  7734  distrlem1prl  7780  distrlem1pru  7781  1idprl  7788  1idpru  7789  ltexprlemell  7796  ltexprlemelu  7797  ltexpri  7811  lteupri  7815  ltaprlem  7816  recexprlem1ssl  7831  recexprlem1ssu  7832  recexpr  7836  cauappcvgprlemm  7843  cauappcvgprlemdisj  7849  cauappcvgprlemloc  7850  cauappcvgprlemladdru  7854  cauappcvgprlemladdrl  7855  cauappcvgprlem1  7857  cauappcvgprlemlim  7859  cauappcvgpr  7860  mulcmpblnrlemg  7938  addclsr  7951  mulclsr  7952  ltasrg  7968  negexsr  7970  recexgt0sr  7971  mulgt0sr  7976  mulextsr1  7979  srpospr  7981  caucvgsrlemgt1  7993  map2psrprg  8003  axaddrcl  8063  axmulrcl  8065  axaddcom  8068  axrnegex  8077  axprecex  8078  axcnre  8079  axpre-ltadd  8084  axpre-mulgt0  8085  axpre-mulext  8086  rereceu  8087  recriota  8088  axcaucvglemres  8097  readdcan  8297  cnegexlem1  8332  cnegex  8335  addcan  8337  negeq  8350  subadd  8360  addid0  8530  ine0  8551  rimul  8743  cru  8760  apreim  8761  recexap  8811  mulcanapd  8819  receuap  8827  divmulap  8833  rerecapb  9001  cju  9119  nnaddcl  9141  nnmulcl  9142  nnsub  9160  nnnn0addcl  9410  zaddcllempos  9494  zaddcl  9497  zdiv  9546  deceq1  9593  deceq2  9594  uzaddcl  9793  zq  9833  qreccl  9849  cnref1o  9858  xaddnemnf  10065  xaddnepnf  10066  xaddcom  10069  xnn0xadd0  10075  xnegdi  10076  xaddass  10077  xlt2add  10088  xlesubadd  10091  xleaddadd  10095  fzsuc2  10287  fzrevral  10313  fzshftral  10316  2ffzeq  10349  exfzdc  10458  exbtwnzlemshrink  10480  rebtwn2zlemshrink  10485  modqval  10558  modqmuladd  10600  modqmuladdnn0  10602  frecuzrdgrrn  10642  frec2uzrdg  10643  frecuzrdgrcl  10644  frecuzrdgsuc  10648  frecuzrdgrclt  10649  frecuzrdgg  10650  frecuzrdgsuctlem  10657  frecfzennn  10660  uzsinds  10678  iseqvalcbv  10693  seq3val  10694  seqvalcd  10695  seqovcd  10701  seq3caopr3  10725  seq3caopr2  10727  seqcaopr2g  10728  seq3f1olemp  10749  seqf1og  10755  seq3id  10759  seq3homo  10761  seq3z  10762  seqhomog  10764  seqfeq4g  10765  seq3distr  10766  expp1  10780  expnegap0  10781  expcllem  10784  expcl2lemap  10785  m1expcl2  10795  expap0  10803  mulexp  10812  expadd  10815  expmul  10818  leexp2r  10827  leexp1a  10828  bernneq  10894  expnbnd  10897  modqexp  10900  nn0ltexp2  10943  expcan  10950  apexp1  10952  facdiv  10972  faclbnd3  10977  faclbnd6  10978  bcval  10983  bcpasc  11000  bccl  11001  fz1eqb  11024  omgadd  11036  hashunlem  11038  hashfzo  11057  hashfzp1  11059  iswrdinn0  11089  wrdnval  11115  eqwrd  11125  eqs1  11176  pfxeq  11244  ccatopth  11264  wrd2ind  11271  swrdccatin1  11273  swrdccatin2  11277  pfxccatin12lem2  11279  swrdccat3blem  11287  pfxccatid  11289  swrdccatin1d  11291  swrdccatin2d  11292  s2dmg  11338  shftfvalg  11345  shftfval  11348  cjth  11373  remim  11387  reim0b  11389  cjexp  11420  cnrecnv  11437  cvg1nlemcau  11511  cvg1nlemres  11512  recvguniq  11522  resqrexlemp1rp  11533  resqrexlemfp1  11536  resqrexlemlo  11540  resqrexlemgt0  11547  resqrexlemoverl  11548  resqrexlemglsq  11549  resqrexlemsqa  11551  resqrexlemex  11552  resqrex  11553  absexp  11606  recan  11636  climcn2  11836  subcn2  11838  summodc  11910  fsum3  11914  fsum3cvg3  11923  fsumrev  11970  fisum0diag2  11974  telfsumo  11993  fsumrelem  11998  binomlem  12010  binom  12011  binom1dif  12014  bcxmaslem1  12015  bcxmas  12016  isumshft  12017  divcnv  12024  arisum  12025  trireciplem  12027  expcnvap0  12029  expcnvre  12030  expcnv  12031  explecnv  12032  geosergap  12033  geolim  12038  geolim2  12039  geo2sum  12041  geo2lim  12043  geoisum  12044  geoisumr  12045  geoisum1  12046  geoisum1c  12047  cvgratnnlemsumlt  12055  cvgratz  12059  prodmodc  12105  fprodseq  12110  fprodcl2lem  12132  fprodfac  12142  fprodabs  12143  fprodrev  12146  eftvalcn  12184  efcvgfsum  12194  ege2le3  12198  efcj  12200  efaddlem  12201  efexp  12209  eftlub  12217  efgt1p2  12222  eflegeo  12228  sinval  12229  cosval  12230  demoivreALT  12301  divides  12316  dvdscmul  12345  dvds2ln  12351  dvdstr  12355  odd2np1lem  12399  odd2np1  12400  2tp1odd  12411  opeo  12424  omeo  12425  m1expe  12426  m1expo  12427  m1exp1  12428  divalglemnn  12445  divalglemeunn  12448  divalglemeuneg  12450  divalgmod  12454  ndvdssub  12457  bitsval  12470  bitsfzolem  12481  bitsinv1lem  12488  bitsinv1  12489  gcd0id  12516  bezoutlemnewy  12533  bezoutlema  12536  bezoutlemb  12537  bezoutlemex  12538  bezoutlemaz  12540  bezoutlembz  12541  gcdmultiple  12557  gcdmultiplez  12558  dvdsmulgcd  12562  rplpwr  12564  nn0seqcvgd  12579  dvdslcm  12607  lcmeq0  12609  lcmcl  12610  lcmneg  12612  lcmgcdlem  12615  lcmdvds  12617  lcmid  12618  lcmgcdeq  12621  coprmdvds  12630  mulgcddvds  12632  qredeq  12634  cncongr1  12641  cncongr2  12642  cncongrcoprm  12644  prmind2  12658  isprm6  12685  prmdvdsexp  12686  prmdvdsexpr  12688  sqrt2irr  12700  pw2dvdslemn  12703  pw2dvdseu  12706  oddpwdclemxy  12707  sqpweven  12713  2sqpwodd  12714  sqne2sq  12715  nn0gcdsq  12738  qden1elz  12743  phival  12751  dfphi2  12758  eulerthlemrprm  12767  eulerthlema  12768  prmdiv  12773  prmdiveq  12774  phisum  12779  odzval  12780  odzcllem  12781  odzdvds  12784  reumodprminv  12792  pythagtriplem3  12806  pythagtriplem18  12820  pythagtriplem19  12821  pclem0  12825  pclemub  12826  pclemdc  12827  pcprecl  12828  pcprendvds  12829  pcpremul  12832  pceulem  12833  pceu  12834  pczpre  12836  pcdiv  12841  pcqmul  12842  pcqcl  12845  pcexp  12848  pcxnn0cl  12849  pcxcl  12850  pcge0  12852  pcdvdsb  12859  pcneg  12864  pcabs  12865  pcgcd1  12867  pc2dvds  12869  pc11  12870  pcz  12871  pcprmpw2  12872  pcprmpw  12873  dvdsprmpweq  12874  dvdsprmpweqnn  12875  dvdsprmpweqle  12876  pcaddlem  12878  pcadd  12879  pcfac  12889  oddprmdvds  12893  prmpwdvds  12894  pockthi  12897  infpnlem2  12899  1arithlem1  12902  4sqlemffi  12935  4sqlem12  12941  2expltfac  12978  ennnfonelemnn0  13009  ennnfonelemr  13010  f1ovscpbl  13361  imasaddvallemg  13364  ercpbl  13380  mgm1  13419  mgmidmo  13421  mgmlrid  13428  lidrideqd  13430  lidrididd  13431  grpinvalem  13434  grpinva  13435  gsumfzval  13440  gsumval2  13446  isnsgrp  13455  sgrpass  13457  sgrp1  13460  mndinvmod  13494  imasmnd2  13501  mnd1  13504  mnd1id  13505  mhmpropd  13515  mhmlin  13516  insubm  13534  mhmima  13540  gsumwsubmcl  13545  gsumwmhm  13547  grpinvex  13559  grppropd  13566  dfgrp2  13576  grpidd2  13590  grpinvval  13592  grpinvid1  13601  grplrinv  13606  grpidinv2  13607  grpidinv  13608  grplcan  13611  grpidssd  13625  grpinvssd  13626  dfgrp3mlem  13647  dfgrp3m  13648  grplactcnv  13651  grp1  13655  imasgrp2  13663  mhmlem  13667  mulgnn0gsum  13681  mulginvcom  13700  mulgnn0ass  13711  mulgmodid  13714  issubg  13726  issubg2m  13742  issubg4m  13746  isnsg2  13756  nsgbi  13757  isnsg3  13760  elnmz  13761  nmzbi  13762  ghmlin  13801  ghmrn  13810  ghmnsgima  13821  conjghm  13829  conjnmz  13832  gsumfzconst  13894  rngdi  13919  rngdir  13920  srglz  13964  srgisid  13965  srglmhm  13972  ringid  14005  ringinvnz1ne0  14028  ringinvnzdiv  14029  ring1  14038  ringlghm  14040  imasring  14043  dvdsrtr  14081  lringuplu  14176  issubrng  14179  issubrng2  14190  issubrg  14201  issubrg2  14221  rrgeq0i  14244  rrgeq0  14245  unitrrg  14247  domneq0  14252  lmodlema  14272  islmodd  14273  rmodislmodlem  14330  rmodislmod  14331  lssclg  14344  lss1d  14363  rnglidlmcl  14460  quscrng  14513  cnfldexp  14557  gsumfzfsumlemm  14567  cnfldui  14569  expghmap  14587  zrhval  14597  zrhvalg  14598  znunit  14639  txdis1cn  14968  cnmptcom  14988  psmettri2  15018  isxmet2d  15038  xmeteq0  15049  xmettri2  15051  elblps  15080  elbl  15081  blssps  15117  blss  15118  ssblex  15121  blin2  15122  metss2  15188  comet  15189  bdmopn  15194  txmetcnp  15208  blssioo  15243  divcnap  15255  mpomulcn  15256  expcn  15259  cncfval  15262  cncfi  15268  mulc1cncf  15279  cdivcncfap  15294  mulcncf  15298  expcncf  15299  cnopnap  15301  ellimc3apf  15350  cnlimci  15363  limccnpcntop  15365  limccnp2lem  15366  reldvg  15369  eldvap  15372  dvexp  15401  dvexp2  15402  dvrecap  15403  elplyr  15430  elplyd  15431  ply1termlem  15432  plymullem1  15438  plyadd  15441  plymul  15442  plycoeid3  15447  plycolemc  15448  plyco  15449  plycj  15451  dvply1  15455  dvply2g  15456  sin0pilem2  15472  rpcxpmul2  15603  relogbcxpbap  15655  logbgcd1irr  15657  2irrexpq  15666  2irrexpqap  15668  dvdsppwf1o  15679  mpodvdsmulf1o  15680  fsumdvdsmul  15681  sgmppw  15682  1sgmprm  15684  perfect  15691  lgsneg  15719  lgsdilem  15722  lgsdir  15730  lgsdilem2  15731  lgsdi  15732  lgsne0  15733  lgsdirnn0  15742  lgsdinn0  15743  gausslemma2dlem4  15759  lgseisenlem2  15766  lgseisenlem3  15767  lgseisenlem4  15768  lgsquadlem1  15772  lgsquadlem2  15773  lgsquad2lem2  15777  2lgs  15799  2sqlem6  15815  2sqlem8  15818  2sqlem9  15819  2sqlem10  15820  wlkeq  16100  wlkl1loop  16104  uspgr2wlkeq  16111  upgr2wlkdc  16121  trilpolemclim  16492  trilpolemcl  16493  trilpolemisumle  16494  trilpolemeq1  16496  trilpolemlt1  16497  trilpo  16499  trirec0  16500  redcwlpo  16511  nconstwlpolemgt0  16520  nconstwlpo  16522  neapmkv  16524