Theorem oveq2 6083

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 3900	. . 3 ⊢ (𝐴 = 𝐵 → ⟨𝐶, 𝐴⟩ = ⟨𝐶, 𝐵⟩)
2	1	fveq2d 5694	. 2 ⊢ (𝐴 = 𝐵 → (𝐹‘⟨𝐶, 𝐴⟩) = (𝐹‘⟨𝐶, 𝐵⟩))
3		df-ov 6078	. 2 ⊢ (𝐶𝐹𝐴) = (𝐹‘⟨𝐶, 𝐴⟩)
4		df-ov 6078	. 2 ⊢ (𝐶𝐹𝐵) = (𝐹‘⟨𝐶, 𝐵⟩)
5	2, 3, 4	3eqtr4g 2296	1 ⊢ (𝐴 = 𝐵 → (𝐶𝐹𝐴) = (𝐶𝐹𝐵))

Syntax hints:   → wi 4   = wceq 1402  ⟨cop 3708  ‘cfv 5372  (class class class)co 6075

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 721  ax-5 1500  ax-7 1501  ax-gen 1502  ax-ie1 1546  ax-ie2 1547  ax-8 1557  ax-10 1558  ax-11 1559  ax-i12 1560  ax-bndl 1562  ax-4 1563  ax-17 1579  ax-i9 1583  ax-ial 1587  ax-i5r 1588  ax-ext 2220

This theorem depends on definitions:  df-bi 117  df-3an 1011  df-tru 1405  df-nf 1514  df-sb 1816  df-clab 2225  df-cleq 2231  df-clel 2234  df-nfc 2381  df-rex 2534  df-v 2823  df-un 3224  df-sn 3711  df-pr 3712  df-op 3714  df-uni 3931  df-br 4126  df-iota 5332  df-fv 5380  df-ov 6078

This theorem is referenced by:  oveq12  6084  oveq2i  6086  oveq2d  6091  ovanraleqv  6099  ovrspc2v  6101  oveqrspc2v  6102  rspceov  6118  fovcld  6183  ovmpos  6202  ov2gf  6203  ovi3  6216  caovclg  6232  caovcomg  6235  caovassg  6238  caovcang  6241  caovcan  6244  caovordig  6245  caovordg  6247  caovord  6251  caovdig  6254  caovdirg  6257  caovimo  6273  suppssov1  6289  off  6305  caofid0l  6319  caofid2  6322  caofdig  6326  suppofss1dcl  6494  suppofss2dcl  6495  omv  6718  oeiv  6719  oasuc  6727  oawordriexmid  6733  omsuc  6735  nna0r  6741  nnm0r  6742  nnacl  6743  nnmcl  6744  nnacom  6747  nnaass  6748  nndi  6749  nnmass  6750  nnmsucr  6751  nnmcom  6752  nnaordi  6771  nnaord  6772  nnmordi  6779  nnmord  6780  nnaordex  6791  nnawordex  6792  nnm00  6793  eroveu  6890  ecopovtrn  6896  ecopovtrng  6899  th3qlem2  6902  th3q  6904  ecovcom  6906  ecovicom  6907  ecovass  6908  ecoviass  6909  ecovdi  6910  ecovidi  6911  exmidpw2en  7209  mapfi  7251  acneq  7548  addcanpig  7691  mulcanpig  7692  addcmpblnq  7724  addclnq  7732  mulclnq  7733  recexnq  7747  recmulnqg  7748  ltanqg  7757  ltmnqg  7758  ltexnqq  7765  enq0ref  7790  enq0tr  7791  addcmpblnq0  7800  mulnnnq0  7807  addclnq0  7808  mulclnq0  7809  distrnq0  7816  mulcomnq0  7817  addassnq0  7819  nq02m  7822  prarloclem3  7854  genipv  7866  genpassl  7881  genpassu  7882  addlocpr  7893  distrlem1prl  7939  distrlem1pru  7940  1idprl  7947  1idpru  7948  ltexprlemell  7955  ltexprlemelu  7956  ltexpri  7970  lteupri  7974  ltaprlem  7975  recexprlem1ssl  7990  recexprlem1ssu  7991  recexpr  7995  cauappcvgprlemm  8002  cauappcvgprlemdisj  8008  cauappcvgprlemloc  8009  cauappcvgprlemladdru  8013  cauappcvgprlemladdrl  8014  cauappcvgprlem1  8016  cauappcvgprlemlim  8018  cauappcvgpr  8019  mulcmpblnrlemg  8097  addclsr  8110  mulclsr  8111  ltasrg  8127  negexsr  8129  recexgt0sr  8130  mulgt0sr  8135  mulextsr1  8138  srpospr  8140  caucvgsrlemgt1  8152  map2psrprg  8162  axaddrcl  8222  axmulrcl  8224  axaddcom  8227  axrnegex  8236  axprecex  8237  axcnre  8238  axpre-ltadd  8243  axpre-mulgt0  8244  axpre-mulext  8245  rereceu  8246  recriota  8247  axcaucvglemres  8256  readdcan  8456  cnegexlem1  8491  cnegex  8494  addcan  8496  negeq  8509  subadd  8519  addid0  8689  ine0  8711  rimul  8903  cru  8920  apreim  8921  recexap  8971  mulcanapd  8979  receuap  8989  divmulap  8995  rerecapb  9163  cju  9281  nnaddcl  9303  nnmulcl  9304  nnsub  9322  nnnn0addcl  9572  zaddcllempos  9660  zaddcl  9663  zdiv  9713  deceq1  9760  deceq2  9761  uzaddcl  9965  zq  10005  qreccl  10021  cnref1o  10030  xaddnemnf  10238  xaddnepnf  10239  xaddcom  10242  xnn0xadd0  10248  xnegdi  10249  xaddass  10250  xlt2add  10261  xlesubadd  10264  xleaddadd  10268  fzsuc2  10464  fzrevral  10490  fzshftral  10493  2ffzeq  10526  exfzdc  10637  exbtwnzlemshrink  10661  rebtwn2zlemshrink  10666  modqval  10739  modqmuladd  10781  modqmuladdnn0  10783  frecuzrdgrrn  10823  frec2uzrdg  10824  frecuzrdgrcl  10825  frecuzrdgsuc  10829  frecuzrdgrclt  10830  frecuzrdgg  10831  frecuzrdgsuctlem  10838  frecfzennn  10841  uzsinds  10859  iseqvalcbv  10874  seq3val  10875  seqvalcd  10876  seqovcd  10882  seq3caopr3  10906  seq3caopr2  10908  seqcaopr2g  10909  seq3f1olemp  10930  seqf1og  10936  seq3id  10940  seq3homo  10942  seq3z  10943  seqhomog  10945  seqfeq4g  10946  seq3distr  10947  expp1  10961  expnegap0  10962  expcllem  10965  expcl2lemap  10966  m1expcl2  10976  expap0  10984  mulexp  10993  expadd  10996  expmul  10999  leexp2r  11008  leexp1a  11009  bernneq  11076  expnbnd  11079  modqexp  11082  nn0ltexp2  11125  expcan  11132  apexp1  11134  facdiv  11154  faclbnd3  11159  faclbnd6  11160  bcval  11165  bcpasc  11182  bccl  11183  fz1eqb  11207  omgadd  11220  hashunlem  11222  hashfzo  11241  hashfzp1  11243  hashmap  11246  hashfibclem  11260  hashfibc  11261  hashf1  11265  iswrdinn0  11287  wrdnval  11313  eqwrd  11323  eqs1  11374  pfxeq  11446  ccatopth  11466  wrd2ind  11473  swrdccatin1  11475  swrdccatin2  11479  pfxccatin12lem2  11481  swrdccat3blem  11489  pfxccatid  11491  swrdccatin1d  11493  swrdccatin2d  11494  s2dmg  11540  shftfvalg  11561  shftfval  11564  cjth  11589  remim  11603  reim0b  11605  cjexp  11636  cnrecnv  11654  cvg1nlemcau  11728  cvg1nlemres  11729  recvguniq  11739  resqrexlemp1rp  11750  resqrexlemfp1  11753  resqrexlemlo  11757  resqrexlemgt0  11764  resqrexlemoverl  11765  resqrexlemglsq  11766  resqrexlemsqa  11768  resqrexlemex  11769  resqrex  11770  absexp  11823  recan  11853  climcn2  12053  subcn2  12055  summodc  12128  fsum3  12132  fsum3cvg3  12141  fsumrev  12188  fisum0diag2  12192  telfsumo  12211  fsumrelem  12216  binomlem  12228  binom  12229  binom1dif  12232  bcxmaslem1  12233  bcxmas  12234  isumshft  12235  divcnv  12242  arisum  12243  trireciplem  12245  expcnvap0  12247  expcnvre  12248  expcnv  12249  explecnv  12250  geosergap  12251  geolim  12256  geolim2  12257  geo2sum  12259  geo2lim  12261  geoisum  12262  geoisumr  12263  geoisum1  12264  geoisum1c  12265  cvgratnnlemsumlt  12273  cvgratz  12277  prodmodc  12323  fprodseq  12328  fprodcl2lem  12350  fprodfac  12360  fprodabs  12361  fprodrev  12364  eftvalcn  12402  efcvgfsum  12412  ege2le3  12416  efcj  12418  efaddlem  12419  efexp  12427  eftlub  12435  efgt1p2  12440  eflegeo  12446  sinval  12447  cosval  12448  demoivreALT  12519  divides  12534  dvdscmul  12563  dvds2ln  12569  dvdstr  12573  odd2np1lem  12617  odd2np1  12618  2tp1odd  12629  opeo  12642  omeo  12643  m1expe  12644  m1expo  12645  m1exp1  12646  divalglemnn  12663  divalglemeunn  12666  divalglemeuneg  12668  divalgmod  12672  ndvdssub  12675  bitsval  12688  bitsfzolem  12699  bitsinv1lem  12706  bitsinv1  12707  gcd0id  12734  bezoutlemnewy  12751  bezoutlema  12754  bezoutlemb  12755  bezoutlemex  12756  bezoutlemaz  12758  bezoutlembz  12759  gcdmultiple  12775  gcdmultiplez  12776  dvdsmulgcd  12780  rplpwr  12782  nn0seqcvgd  12797  dvdslcm  12825  lcmeq0  12827  lcmcl  12828  lcmneg  12830  lcmgcdlem  12833  lcmdvds  12835  lcmid  12836  lcmgcdeq  12839  coprmdvds  12848  mulgcddvds  12850  qredeq  12852  cncongr1  12859  cncongr2  12860  cncongrcoprm  12862  prmind2  12876  isprm6  12903  prmdvdsexp  12904  prmdvdsexpr  12906  sqrt2irr  12918  pw2dvdslemn  12921  pw2dvdseu  12924  oddpwdclemxy  12925  sqpweven  12931  2sqpwodd  12932  sqne2sq  12933  nn0gcdsq  12956  qden1elz  12961  phival  12969  dfphi2  12976  eulerthlemrprm  12985  eulerthlema  12986  prmdiv  12991  prmdiveq  12992  phisum  12997  odzval  12998  odzcllem  12999  odzdvds  13002  reumodprminv  13010  pythagtriplem3  13024  pythagtriplem18  13038  pythagtriplem19  13039  pclem0  13043  pclemub  13044  pclemdc  13045  pcprecl  13046  pcprendvds  13047  pcpremul  13050  pceulem  13051  pceu  13052  pczpre  13054  pcdiv  13059  pcqmul  13060  pcqcl  13063  pcexp  13066  pcxnn0cl  13067  pcxcl  13068  pcge0  13070  pcdvdsb  13077  pcneg  13082  pcabs  13083  pcgcd1  13085  pc2dvds  13087  pc11  13088  pcz  13089  pcprmpw2  13090  pcprmpw  13091  dvdsprmpweq  13092  dvdsprmpweqnn  13093  dvdsprmpweqle  13094  pcaddlem  13096  pcadd  13097  pcfac  13107  oddprmdvds  13111  prmpwdvds  13112  pockthi  13115  infpnlem2  13117  1arithlem1  13120  4sqlemffi  13153  4sqlem12  13159  2expltfac  13196  ballotfilemfval  13207  ballotfilemfc0  13210  ballotfilemfcc  13211  ballotfilemsv  13231  ballotfilemsf1o  13235  ballotfi  13260  ennnfonelemnn0  13291  ennnfonelemr  13292  f1ovscpbl  13610  imasaddvallemg  13613  ercpbl  13629  mgm1  13667  mgmidmo  13669  mgmlrid  13676  lidrideqd  13678  lidrididd  13679  grpinvalem  13682  grpinva  13683  gzsumfzval  13688  gzsumval2  13691  isnsgrp  13698  sgrpass  13700  sgrp1  13703  mndinvmod  13735  imasmnd2  13736  mnd1  13739  mnd1id  13740  mhmpropd  13750  mhmlin  13751  insubm  13769  mhmima  13775  gzsumwsubmcl  13778  gzsumwmhm  13780  grpinvex  13792  grppropd  13799  dfgrp2  13809  grpidd2  13823  grpinvval  13825  grpinvid1  13834  grplrinv  13839  grpidinv2  13840  grpidinv  13841  grplcan  13844  grpidssd  13858  grpinvssd  13859  dfgrp3mlem  13880  dfgrp3m  13881  grplactcnv  13884  grp1  13888  imasgrp2  13890  mhmlem  13894  mulgnn0gzsum  13908  mulginvcom  13927  mulgnn0ass  13938  mulgmodid  13941  issubg  13953  issubg2m  13969  issubg4m  13973  isnsg2  13983  nsgbi  13984  isnsg3  13987  elnmz  13988  nmzbi  13989  ghmlin  14028  ghmrn  14037  ghmnsgima  14048  conjghm  14056  conjnmz  14059  gzsumconst  14120  rngdi  14214  rngdir  14215  srglz  14263  srgisid  14264  srglmhm  14271  ringid  14304  ringinvnz1ne0  14327  ringinvnzdiv  14328  ring1  14337  ringlghm  14339  imasring  14342  dvdsrtr  14381  lringuplu  14476  issubrng  14480  issubrng2  14491  issubrg  14502  issubrg2  14522  rrgeq0i  14545  rrgeq0  14546  unitrrg  14549  domneq0  14554  lmodlema  14601  islmodd  14602  rmodislmodlem  14659  rmodislmod  14660  lssclg  14673  lss1d  14692  rnglidlmcl  14789  quscrng  14842  cnfldexp  14886  gsumfsum  14895  cnfldui  14896  expghmap  14914  zrhval  14924  zrhvalg  14925  znunit  14966  txdis1cn  15302  cnmptcom  15322  psmettri2  15352  isxmet2d  15372  xmeteq0  15383  xmettri2  15385  elblps  15414  elbl  15415  blssps  15451  blss  15452  ssblex  15455  blin2  15456  metss2  15522  comet  15523  bdmopn  15528  txmetcnp  15542  blssioo  15577  divcnap  15589  mpomulcn  15590  expcn  15593  cncfval  15596  cncfi  15602  mulc1cncf  15613  cdivcncfap  15628  mulcncf  15632  expcncf  15633  cnopnap  15635  ellimc3apf  15684  cnlimci  15697  limccnpcntop  15699  limccnp2lem  15700  reldvg  15703  eldvap  15706  dvexp  15735  dvexp2  15736  dvrecap  15737  elplyr  15764  elplyd  15765  ply1termlem  15766  plymullem1  15772  plyadd  15775  plymul  15776  plycoeid3  15781  plycolemc  15782  plyco  15783  plycj  15785  dvply1  15789  dvply2g  15790  sin0pilem2  15806  logfac  15918  rpcxpmul2  15938  relogbcxpbap  15990  logbgcd1irr  15992  2irrexpq  16001  2irrexpqap  16003  dvdsppwf1o  16017  mpodvdsmulf1o  16018  fsumdvdsmul  16019  sgmppw  16020  1sgmprm  16022  perfect  16029  lgsneg  16057  lgsdilem  16060  lgsdir  16068  lgsdilem2  16069  lgsdi  16070  lgsne0  16071  lgsdirnn0  16080  lgsdinn0  16081  gausslemma2dlem4  16097  lgseisenlem2  16104  lgseisenlem3  16105  lgseisenlem4  16106  lgsquadlem1  16110  lgsquadlem2  16111  lgsquad2lem2  16115  2lgs  16137  2sqlem6  16153  2sqlem8  16156  2sqlem9  16157  2sqlem10  16158  wlkeq  16509  wlkl1loop  16513  uspgr2wlkeq  16520  upgr2wlkdc  16532  clwwlknonmpo  16583  eupth2fi  16634  trilpolemclim  16990  trilpolemcl  16991  trilpolemisumle  16992  trilpolemeq1  16994  trilpolemlt1  16995  trilpo  16997  trirec0  16998  qdiff  17003  redcwlpo  17010  nconstwlpolemgt0  17019  nconstwlpo  17021  neapmkv  17023