Theorem oveq2 5844

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 3753	. . 3 ⊢ (𝐴 = 𝐵 → ⟨𝐶, 𝐴⟩ = ⟨𝐶, 𝐵⟩)
2	1	fveq2d 5484	. 2 ⊢ (𝐴 = 𝐵 → (𝐹‘⟨𝐶, 𝐴⟩) = (𝐹‘⟨𝐶, 𝐵⟩))
3		df-ov 5839	. 2 ⊢ (𝐶𝐹𝐴) = (𝐹‘⟨𝐶, 𝐴⟩)
4		df-ov 5839	. 2 ⊢ (𝐶𝐹𝐵) = (𝐹‘⟨𝐶, 𝐵⟩)
5	2, 3, 4	3eqtr4g 2222	1 ⊢ (𝐴 = 𝐵 → (𝐶𝐹𝐴) = (𝐶𝐹𝐵))

Syntax hints:   → wi 4   = wceq 1342  ⟨cop 3573  ‘cfv 5182  (class class class)co 5836

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-ia1 105  ax-ia2 106  ax-ia3 107  ax-io 699  ax-5 1434  ax-7 1435  ax-gen 1436  ax-ie1 1480  ax-ie2 1481  ax-8 1491  ax-10 1492  ax-11 1493  ax-i12 1494  ax-bndl 1496  ax-4 1497  ax-17 1513  ax-i9 1517  ax-ial 1521  ax-i5r 1522  ax-ext 2146

This theorem depends on definitions:  df-bi 116  df-3an 969  df-tru 1345  df-nf 1448  df-sb 1750  df-clab 2151  df-cleq 2157  df-clel 2160  df-nfc 2295  df-rex 2448  df-v 2723  df-un 3115  df-sn 3576  df-pr 3577  df-op 3579  df-uni 3784  df-br 3977  df-iota 5147  df-fv 5190  df-ov 5839

This theorem is referenced by:  oveq12  5845  oveq2i  5847  oveq2d  5852  ovanraleqv  5860  rspceov  5875  fovcl  5938  ovmpos  5956  ov2gf  5957  ovi3  5969  caovclg  5985  caovcomg  5988  caovassg  5991  caovcang  5994  caovcan  5997  caovordig  5998  caovordg  6000  caovord  6004  caovdig  6007  caovdirg  6010  caovimo  6026  grprinvlem  6027  grprinvd  6028  suppssov1  6041  off  6056  omv  6414  oeiv  6415  oasuc  6423  oawordriexmid  6429  omsuc  6431  nna0r  6437  nnm0r  6438  nnacl  6439  nnmcl  6440  nnacom  6443  nnaass  6444  nndi  6445  nnmass  6446  nnmsucr  6447  nnmcom  6448  nnaordi  6467  nnaord  6468  nnmordi  6475  nnmord  6476  nnaordex  6486  nnawordex  6487  nnm00  6488  eroveu  6583  ecopovtrn  6589  ecopovtrng  6592  th3qlem2  6595  th3q  6597  ecovcom  6599  ecovicom  6600  ecovass  6601  ecoviass  6602  ecovdi  6603  ecovidi  6604  addcanpig  7266  mulcanpig  7267  addcmpblnq  7299  addclnq  7307  mulclnq  7308  recexnq  7322  recmulnqg  7323  ltanqg  7332  ltmnqg  7333  ltexnqq  7340  enq0ref  7365  enq0tr  7366  addcmpblnq0  7375  mulnnnq0  7382  addclnq0  7383  mulclnq0  7384  distrnq0  7391  mulcomnq0  7392  addassnq0  7394  nq02m  7397  prarloclem3  7429  genipv  7441  genpassl  7456  genpassu  7457  addlocpr  7468  distrlem1prl  7514  distrlem1pru  7515  1idprl  7522  1idpru  7523  ltexprlemell  7530  ltexprlemelu  7531  ltexpri  7545  lteupri  7549  ltaprlem  7550  recexprlem1ssl  7565  recexprlem1ssu  7566  recexpr  7570  cauappcvgprlemm  7577  cauappcvgprlemdisj  7583  cauappcvgprlemloc  7584  cauappcvgprlemladdru  7588  cauappcvgprlemladdrl  7589  cauappcvgprlem1  7591  cauappcvgprlemlim  7593  cauappcvgpr  7594  mulcmpblnrlemg  7672  addclsr  7685  mulclsr  7686  ltasrg  7702  negexsr  7704  recexgt0sr  7705  mulgt0sr  7710  mulextsr1  7713  srpospr  7715  caucvgsrlemgt1  7727  map2psrprg  7737  axaddrcl  7797  axmulrcl  7799  axaddcom  7802  axrnegex  7811  axprecex  7812  axcnre  7813  axpre-ltadd  7818  axpre-mulgt0  7819  axpre-mulext  7820  rereceu  7821  recriota  7822  axcaucvglemres  7831  readdcan  8029  cnegexlem1  8064  cnegex  8067  addcan  8069  negeq  8082  subadd  8092  addid0  8262  ine0  8283  rimul  8474  cru  8491  apreim  8492  recexap  8541  mulcanapd  8549  receuap  8557  divmulap  8562  cju  8847  nnaddcl  8868  nnmulcl  8869  nnsub  8887  nnnn0addcl  9135  zaddcllempos  9219  zaddcl  9222  zdiv  9270  deceq1  9317  deceq2  9318  uzaddcl  9515  zq  9555  qreccl  9571  cnref1o  9579  xaddnemnf  9784  xaddnepnf  9785  xaddcom  9788  xnn0xadd0  9794  xnegdi  9795  xaddass  9796  xlt2add  9807  xlesubadd  9810  xleaddadd  9814  fzsuc2  10004  fzrevral  10030  fzshftral  10033  2ffzeq  10066  exfzdc  10165  exbtwnzlemshrink  10174  rebtwn2zlemshrink  10179  modqval  10249  modqmuladd  10291  modqmuladdnn0  10293  frecuzrdgrrn  10333  frec2uzrdg  10334  frecuzrdgrcl  10335  frecuzrdgsuc  10339  frecuzrdgrclt  10340  frecuzrdgg  10341  frecuzrdgsuctlem  10348  frecfzennn  10351  uzsinds  10367  iseqvalcbv  10382  seq3val  10383  seqvalcd  10384  seqovcd  10388  seq3caopr3  10406  seq3caopr2  10407  seq3f1olemp  10427  seq3id  10433  seq3homo  10435  seq3z  10436  seq3distr  10438  expp1  10452  expnegap0  10453  expcllem  10456  expcl2lemap  10457  m1expcl2  10467  expap0  10475  mulexp  10484  expadd  10487  expmul  10490  leexp2r  10499  leexp1a  10500  bernneq  10564  expnbnd  10567  modqexp  10570  nn0ltexp2  10612  expcan  10618  apexp1  10620  facdiv  10640  faclbnd3  10645  faclbnd6  10646  bcval  10651  bcpasc  10668  bccl  10669  fz1eqb  10693  omgadd  10704  hashunlem  10706  hashfzo  10724  hashfzp1  10726  shftfvalg  10746  shftfval  10749  cjth  10774  remim  10788  reim0b  10790  cjexp  10821  cnrecnv  10838  cvg1nlemcau  10912  cvg1nlemres  10913  recvguniq  10923  resqrexlemp1rp  10934  resqrexlemfp1  10937  resqrexlemlo  10941  resqrexlemgt0  10948  resqrexlemoverl  10949  resqrexlemglsq  10950  resqrexlemsqa  10952  resqrexlemex  10953  resqrex  10954  absexp  11007  recan  11037  climcn2  11236  subcn2  11238  summodc  11310  fsum3  11314  fsum3cvg3  11323  fsumrev  11370  fisum0diag2  11374  telfsumo  11393  fsumrelem  11398  binomlem  11410  binom  11411  binom1dif  11414  bcxmaslem1  11415  bcxmas  11416  isumshft  11417  divcnv  11424  arisum  11425  trireciplem  11427  expcnvap0  11429  expcnvre  11430  expcnv  11431  explecnv  11432  geosergap  11433  geolim  11438  geolim2  11439  geo2sum  11441  geo2lim  11443  geoisum  11444  geoisumr  11445  geoisum1  11446  geoisum1c  11447  cvgratnnlemsumlt  11455  cvgratz  11459  prodmodc  11505  fprodseq  11510  fprodcl2lem  11532  fprodfac  11542  fprodabs  11543  fprodrev  11546  eftvalcn  11584  efcvgfsum  11594  ege2le3  11598  efcj  11600  efaddlem  11601  efexp  11609  eftlub  11617  efgt1p2  11622  eflegeo  11628  sinval  11629  cosval  11630  demoivreALT  11700  divides  11715  dvdscmul  11744  dvds2ln  11750  dvdstr  11754  odd2np1lem  11794  odd2np1  11795  2tp1odd  11806  opeo  11819  omeo  11820  m1expe  11821  m1expo  11822  m1exp1  11823  divalglemnn  11840  divalglemeunn  11843  divalglemeuneg  11845  divalgmod  11849  ndvdssub  11852  gcd0id  11897  bezoutlemnewy  11914  bezoutlema  11917  bezoutlemb  11918  bezoutlemex  11919  bezoutlemaz  11921  bezoutlembz  11922  gcdmultiple  11938  gcdmultiplez  11939  dvdsmulgcd  11943  rplpwr  11945  nn0seqcvgd  11952  dvdslcm  11980  lcmeq0  11982  lcmcl  11983  lcmneg  11985  lcmgcdlem  11988  lcmdvds  11990  lcmid  11991  lcmgcdeq  11994  coprmdvds  12003  mulgcddvds  12005  qredeq  12007  cncongr1  12014  cncongr2  12015  cncongrcoprm  12017  prmind2  12031  isprm6  12056  prmdvdsexp  12057  prmdvdsexpr  12059  sqrt2irr  12071  pw2dvdslemn  12074  pw2dvdseu  12077  oddpwdclemxy  12078  sqpweven  12084  2sqpwodd  12085  sqne2sq  12086  nn0gcdsq  12109  qden1elz  12114  phival  12122  dfphi2  12129  eulerthlemrprm  12138  eulerthlema  12139  prmdiv  12144  prmdiveq  12145  phisum  12149  odzval  12150  odzcllem  12151  odzdvds  12154  reumodprminv  12162  pythagtriplem3  12176  pythagtriplem18  12190  pythagtriplem19  12191  pclem0  12195  pclemub  12196  pclemdc  12197  pcprecl  12198  pcprendvds  12199  pcpremul  12202  pceulem  12203  pceu  12204  pczpre  12206  pcdiv  12211  pcqmul  12212  pcqcl  12215  pcexp  12218  pcxnn0cl  12219  pcxcl  12220  pcge0  12221  pcdvdsb  12228  pcneg  12233  pcabs  12234  pcgcd1  12236  pc2dvds  12238  pc11  12239  pcz  12240  pcprmpw2  12241  pcprmpw  12242  dvdsprmpweq  12243  dvdsprmpweqnn  12244  dvdsprmpweqle  12245  pcaddlem  12247  pcadd  12248  pcfac  12257  oddprmdvds  12261  ennnfonelemnn0  12292  ennnfonelemr  12293  txdis1cn  12819  cnmptcom  12839  psmettri2  12869  isxmet2d  12889  xmeteq0  12900  xmettri2  12902  elblps  12931  elbl  12932  blssps  12968  blss  12969  ssblex  12972  blin2  12973  metss2  13039  comet  13040  bdmopn  13045  txmetcnp  13059  blssioo  13086  divcnap  13096  cncfval  13100  cncfi  13106  mulc1cncf  13117  cdivcncfap  13128  mulcncf  13132  expcncf  13133  cnopnap  13135  ellimc3apf  13170  cnlimci  13183  limccnpcntop  13185  limccnp2lem  13186  reldvg  13189  eldvap  13192  dvexp  13216  dvexp2  13217  dvrecap  13218  sin0pilem2  13244  relogbcxpbap  13424  logbgcd1irr  13426  2irrexpq  13435  2irrexpqap  13437  trilpolemclim  13749  trilpolemcl  13750  trilpolemisumle  13751  trilpolemeq1  13753  trilpolemlt1  13754  trilpo  13756  trirec0  13757  redcwlpo  13768  nconstwlpolemgt0  13776  nconstwlpo  13778  neapmkv  13780