Theorem oveq2 5927

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

Syntax hints:   → wi 4   = wceq 1364  ⟨cop 3622  ‘cfv 5255  (class class class)co 5919

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 3158  df-sn 3625  df-pr 3626  df-op 3628  df-uni 3837  df-br 4031  df-iota 5216  df-fv 5263  df-ov 5922

This theorem is referenced by:  oveq12  5928  oveq2i  5930  oveq2d  5935  ovanraleqv  5943  ovrspc2v  5945  oveqrspc2v  5946  rspceov  5961  fovcld  6024  ovmpos  6043  ov2gf  6044  ovi3  6057  caovclg  6073  caovcomg  6076  caovassg  6079  caovcang  6082  caovcan  6085  caovordig  6086  caovordg  6088  caovord  6092  caovdig  6095  caovdirg  6098  caovimo  6114  suppssov1  6129  off  6145  caofdig  6161  omv  6510  oeiv  6511  oasuc  6519  oawordriexmid  6525  omsuc  6527  nna0r  6533  nnm0r  6534  nnacl  6535  nnmcl  6536  nnacom  6539  nnaass  6540  nndi  6541  nnmass  6542  nnmsucr  6543  nnmcom  6544  nnaordi  6563  nnaord  6564  nnmordi  6571  nnmord  6572  nnaordex  6583  nnawordex  6584  nnm00  6585  eroveu  6682  ecopovtrn  6688  ecopovtrng  6691  th3qlem2  6694  th3q  6696  ecovcom  6698  ecovicom  6699  ecovass  6700  ecoviass  6701  ecovdi  6702  ecovidi  6703  exmidpw2en  6970  addcanpig  7396  mulcanpig  7397  addcmpblnq  7429  addclnq  7437  mulclnq  7438  recexnq  7452  recmulnqg  7453  ltanqg  7462  ltmnqg  7463  ltexnqq  7470  enq0ref  7495  enq0tr  7496  addcmpblnq0  7505  mulnnnq0  7512  addclnq0  7513  mulclnq0  7514  distrnq0  7521  mulcomnq0  7522  addassnq0  7524  nq02m  7527  prarloclem3  7559  genipv  7571  genpassl  7586  genpassu  7587  addlocpr  7598  distrlem1prl  7644  distrlem1pru  7645  1idprl  7652  1idpru  7653  ltexprlemell  7660  ltexprlemelu  7661  ltexpri  7675  lteupri  7679  ltaprlem  7680  recexprlem1ssl  7695  recexprlem1ssu  7696  recexpr  7700  cauappcvgprlemm  7707  cauappcvgprlemdisj  7713  cauappcvgprlemloc  7714  cauappcvgprlemladdru  7718  cauappcvgprlemladdrl  7719  cauappcvgprlem1  7721  cauappcvgprlemlim  7723  cauappcvgpr  7724  mulcmpblnrlemg  7802  addclsr  7815  mulclsr  7816  ltasrg  7832  negexsr  7834  recexgt0sr  7835  mulgt0sr  7840  mulextsr1  7843  srpospr  7845  caucvgsrlemgt1  7857  map2psrprg  7867  axaddrcl  7927  axmulrcl  7929  axaddcom  7932  axrnegex  7941  axprecex  7942  axcnre  7943  axpre-ltadd  7948  axpre-mulgt0  7949  axpre-mulext  7950  rereceu  7951  recriota  7952  axcaucvglemres  7961  readdcan  8161  cnegexlem1  8196  cnegex  8199  addcan  8201  negeq  8214  subadd  8224  addid0  8394  ine0  8415  rimul  8606  cru  8623  apreim  8624  recexap  8674  mulcanapd  8682  receuap  8690  divmulap  8696  rerecapb  8864  cju  8982  nnaddcl  9004  nnmulcl  9005  nnsub  9023  nnnn0addcl  9273  zaddcllempos  9357  zaddcl  9360  zdiv  9408  deceq1  9455  deceq2  9456  uzaddcl  9654  zq  9694  qreccl  9710  cnref1o  9719  xaddnemnf  9926  xaddnepnf  9927  xaddcom  9930  xnn0xadd0  9936  xnegdi  9937  xaddass  9938  xlt2add  9949  xlesubadd  9952  xleaddadd  9956  fzsuc2  10148  fzrevral  10174  fzshftral  10177  2ffzeq  10210  exfzdc  10310  exbtwnzlemshrink  10320  rebtwn2zlemshrink  10325  modqval  10398  modqmuladd  10440  modqmuladdnn0  10442  frecuzrdgrrn  10482  frec2uzrdg  10483  frecuzrdgrcl  10484  frecuzrdgsuc  10488  frecuzrdgrclt  10489  frecuzrdgg  10490  frecuzrdgsuctlem  10497  frecfzennn  10500  uzsinds  10518  iseqvalcbv  10533  seq3val  10534  seqvalcd  10535  seqovcd  10541  seq3caopr3  10565  seq3caopr2  10567  seqcaopr2g  10568  seq3f1olemp  10589  seqf1og  10595  seq3id  10599  seq3homo  10601  seq3z  10602  seqhomog  10604  seqfeq4g  10605  seq3distr  10606  expp1  10620  expnegap0  10621  expcllem  10624  expcl2lemap  10625  m1expcl2  10635  expap0  10643  mulexp  10652  expadd  10655  expmul  10658  leexp2r  10667  leexp1a  10668  bernneq  10734  expnbnd  10737  modqexp  10740  nn0ltexp2  10783  expcan  10790  apexp1  10792  facdiv  10812  faclbnd3  10817  faclbnd6  10818  bcval  10823  bcpasc  10840  bccl  10841  fz1eqb  10864  omgadd  10876  hashunlem  10878  hashfzo  10896  hashfzp1  10898  iswrdinn0  10922  wrdnval  10947  eqwrd  10957  shftfvalg  10965  shftfval  10968  cjth  10993  remim  11007  reim0b  11009  cjexp  11040  cnrecnv  11057  cvg1nlemcau  11131  cvg1nlemres  11132  recvguniq  11142  resqrexlemp1rp  11153  resqrexlemfp1  11156  resqrexlemlo  11160  resqrexlemgt0  11167  resqrexlemoverl  11168  resqrexlemglsq  11169  resqrexlemsqa  11171  resqrexlemex  11172  resqrex  11173  absexp  11226  recan  11256  climcn2  11455  subcn2  11457  summodc  11529  fsum3  11533  fsum3cvg3  11542  fsumrev  11589  fisum0diag2  11593  telfsumo  11612  fsumrelem  11617  binomlem  11629  binom  11630  binom1dif  11633  bcxmaslem1  11634  bcxmas  11635  isumshft  11636  divcnv  11643  arisum  11644  trireciplem  11646  expcnvap0  11648  expcnvre  11649  expcnv  11650  explecnv  11651  geosergap  11652  geolim  11657  geolim2  11658  geo2sum  11660  geo2lim  11662  geoisum  11663  geoisumr  11664  geoisum1  11665  geoisum1c  11666  cvgratnnlemsumlt  11674  cvgratz  11678  prodmodc  11724  fprodseq  11729  fprodcl2lem  11751  fprodfac  11761  fprodabs  11762  fprodrev  11765  eftvalcn  11803  efcvgfsum  11813  ege2le3  11817  efcj  11819  efaddlem  11820  efexp  11828  eftlub  11836  efgt1p2  11841  eflegeo  11847  sinval  11848  cosval  11849  demoivreALT  11920  divides  11935  dvdscmul  11964  dvds2ln  11970  dvdstr  11974  odd2np1lem  12016  odd2np1  12017  2tp1odd  12028  opeo  12041  omeo  12042  m1expe  12043  m1expo  12044  m1exp1  12045  divalglemnn  12062  divalglemeunn  12065  divalglemeuneg  12067  divalgmod  12071  ndvdssub  12074  gcd0id  12119  bezoutlemnewy  12136  bezoutlema  12139  bezoutlemb  12140  bezoutlemex  12141  bezoutlemaz  12143  bezoutlembz  12144  gcdmultiple  12160  gcdmultiplez  12161  dvdsmulgcd  12165  rplpwr  12167  nn0seqcvgd  12182  dvdslcm  12210  lcmeq0  12212  lcmcl  12213  lcmneg  12215  lcmgcdlem  12218  lcmdvds  12220  lcmid  12221  lcmgcdeq  12224  coprmdvds  12233  mulgcddvds  12235  qredeq  12237  cncongr1  12244  cncongr2  12245  cncongrcoprm  12247  prmind2  12261  isprm6  12288  prmdvdsexp  12289  prmdvdsexpr  12291  sqrt2irr  12303  pw2dvdslemn  12306  pw2dvdseu  12309  oddpwdclemxy  12310  sqpweven  12316  2sqpwodd  12317  sqne2sq  12318  nn0gcdsq  12341  qden1elz  12346  phival  12354  dfphi2  12361  eulerthlemrprm  12370  eulerthlema  12371  prmdiv  12376  prmdiveq  12377  phisum  12381  odzval  12382  odzcllem  12383  odzdvds  12386  reumodprminv  12394  pythagtriplem3  12408  pythagtriplem18  12422  pythagtriplem19  12423  pclem0  12427  pclemub  12428  pclemdc  12429  pcprecl  12430  pcprendvds  12431  pcpremul  12434  pceulem  12435  pceu  12436  pczpre  12438  pcdiv  12443  pcqmul  12444  pcqcl  12447  pcexp  12450  pcxnn0cl  12451  pcxcl  12452  pcge0  12454  pcdvdsb  12461  pcneg  12466  pcabs  12467  pcgcd1  12469  pc2dvds  12471  pc11  12472  pcz  12473  pcprmpw2  12474  pcprmpw  12475  dvdsprmpweq  12476  dvdsprmpweqnn  12477  dvdsprmpweqle  12478  pcaddlem  12480  pcadd  12481  pcfac  12491  oddprmdvds  12495  prmpwdvds  12496  pockthi  12499  infpnlem2  12501  1arithlem1  12504  4sqlemffi  12537  4sqlem12  12543  ennnfonelemnn0  12582  ennnfonelemr  12583  f1ovscpbl  12898  imasaddvallemg  12901  ercpbl  12917  mgm1  12956  mgmidmo  12958  mgmlrid  12965  lidrideqd  12967  lidrididd  12968  grpinvalem  12971  grpinva  12972  gsumfzval  12977  gsumval2  12983  isnsgrp  12992  sgrpass  12994  sgrp1  12997  mndinvmod  13029  mnd1  13030  mnd1id  13031  mhmpropd  13041  mhmlin  13042  insubm  13060  mhmima  13066  gsumwsubmcl  13071  gsumwmhm  13073  grpinvex  13085  grppropd  13092  dfgrp2  13102  grpidd2  13116  grpinvval  13118  grpinvid1  13127  grplrinv  13132  grpidinv2  13133  grpidinv  13134  grplcan  13137  grpidssd  13151  grpinvssd  13152  dfgrp3mlem  13173  dfgrp3m  13174  grplactcnv  13177  grp1  13181  imasgrp2  13183  mhmlem  13187  mulgnn0gsum  13201  mulginvcom  13220  mulgnn0ass  13231  mulgmodid  13234  issubg  13246  issubg2m  13262  issubg4m  13266  isnsg2  13276  nsgbi  13277  isnsg3  13280  elnmz  13281  nmzbi  13282  ghmlin  13321  ghmrn  13330  ghmnsgima  13341  conjghm  13349  conjnmz  13352  gsumfzconst  13414  rngdi  13439  rngdir  13440  srglz  13484  srgisid  13485  srglmhm  13492  ringid  13525  ringinvnz1ne0  13548  ringinvnzdiv  13549  ring1  13558  ringlghm  13560  imasring  13563  dvdsrtr  13600  lringuplu  13695  issubrng  13698  issubrng2  13709  issubrg  13720  issubrg2  13740  rrgeq0i  13763  rrgeq0  13764  unitrrg  13766  domneq0  13771  lmodlema  13791  islmodd  13792  rmodislmodlem  13849  rmodislmod  13850  lssclg  13863  lss1d  13882  rnglidlmcl  13979  quscrng  14032  cnfldexp  14076  gsumfzfsumlemm  14086  cnfldui  14088  expghmap  14106  zrhval  14116  zrhvalg  14117  znunit  14158  txdis1cn  14457  cnmptcom  14477  psmettri2  14507  isxmet2d  14527  xmeteq0  14538  xmettri2  14540  elblps  14569  elbl  14570  blssps  14606  blss  14607  ssblex  14610  blin2  14611  metss2  14677  comet  14678  bdmopn  14683  txmetcnp  14697  blssioo  14732  divcnap  14744  mpomulcn  14745  expcn  14748  cncfval  14751  cncfi  14757  mulc1cncf  14768  cdivcncfap  14783  mulcncf  14787  expcncf  14788  cnopnap  14790  ellimc3apf  14839  cnlimci  14852  limccnpcntop  14854  limccnp2lem  14855  reldvg  14858  eldvap  14861  dvexp  14890  dvexp2  14891  dvrecap  14892  elplyr  14919  elplyd  14920  ply1termlem  14921  plymullem1  14927  plyadd  14930  plymul  14931  plycolemc  14936  plyco  14937  plycj  14939  dvply1  14943  sin0pilem2  14958  relogbcxpbap  15138  logbgcd1irr  15140  2irrexpq  15149  2irrexpqap  15151  lgsneg  15181  lgsdilem  15184  lgsdir  15192  lgsdilem2  15193  lgsdi  15194  lgsne0  15195  lgsdirnn0  15204  lgsdinn0  15205  gausslemma2dlem4  15221  lgseisenlem2  15228  lgseisenlem3  15229  lgseisenlem4  15230  lgsquadlem1  15234  lgsquadlem2  15235  lgsquad2lem2  15239  2lgs  15261  2sqlem6  15277  2sqlem8  15280  2sqlem9  15281  2sqlem10  15282  trilpolemclim  15596  trilpolemcl  15597  trilpolemisumle  15598  trilpolemeq1  15600  trilpolemlt1  15601  trilpo  15603  trirec0  15604  redcwlpo  15615  nconstwlpolemgt0  15624  nconstwlpo  15626  neapmkv  15628