Theorem oveq2 5975

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 3834	. . 3 ⊢ (𝐴 = 𝐵 → ⟨𝐶, 𝐴⟩ = ⟨𝐶, 𝐵⟩)
2	1	fveq2d 5603	. 2 ⊢ (𝐴 = 𝐵 → (𝐹‘⟨𝐶, 𝐴⟩) = (𝐹‘⟨𝐶, 𝐵⟩))
3		df-ov 5970	. 2 ⊢ (𝐶𝐹𝐴) = (𝐹‘⟨𝐶, 𝐴⟩)
4		df-ov 5970	. 2 ⊢ (𝐶𝐹𝐵) = (𝐹‘⟨𝐶, 𝐵⟩)
5	2, 3, 4	3eqtr4g 2265	1 ⊢ (𝐴 = 𝐵 → (𝐶𝐹𝐴) = (𝐶𝐹𝐵))

Syntax hints:   → wi 4   = wceq 1373  ⟨cop 3646  ‘cfv 5290  (class class class)co 5967

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 711  ax-5 1471  ax-7 1472  ax-gen 1473  ax-ie1 1517  ax-ie2 1518  ax-8 1528  ax-10 1529  ax-11 1530  ax-i12 1531  ax-bndl 1533  ax-4 1534  ax-17 1550  ax-i9 1554  ax-ial 1558  ax-i5r 1559  ax-ext 2189

This theorem depends on definitions:  df-bi 117  df-3an 983  df-tru 1376  df-nf 1485  df-sb 1787  df-clab 2194  df-cleq 2200  df-clel 2203  df-nfc 2339  df-rex 2492  df-v 2778  df-un 3178  df-sn 3649  df-pr 3650  df-op 3652  df-uni 3865  df-br 4060  df-iota 5251  df-fv 5298  df-ov 5970

This theorem is referenced by:  oveq12  5976  oveq2i  5978  oveq2d  5983  ovanraleqv  5991  ovrspc2v  5993  oveqrspc2v  5994  rspceov  6010  fovcld  6073  ovmpos  6092  ov2gf  6093  ovi3  6106  caovclg  6122  caovcomg  6125  caovassg  6128  caovcang  6131  caovcan  6134  caovordig  6135  caovordg  6137  caovord  6141  caovdig  6144  caovdirg  6147  caovimo  6163  suppssov1  6178  off  6194  caofid0l  6208  caofid2  6211  caofdig  6215  omv  6564  oeiv  6565  oasuc  6573  oawordriexmid  6579  omsuc  6581  nna0r  6587  nnm0r  6588  nnacl  6589  nnmcl  6590  nnacom  6593  nnaass  6594  nndi  6595  nnmass  6596  nnmsucr  6597  nnmcom  6598  nnaordi  6617  nnaord  6618  nnmordi  6625  nnmord  6626  nnaordex  6637  nnawordex  6638  nnm00  6639  eroveu  6736  ecopovtrn  6742  ecopovtrng  6745  th3qlem2  6748  th3q  6750  ecovcom  6752  ecovicom  6753  ecovass  6754  ecoviass  6755  ecovdi  6756  ecovidi  6757  exmidpw2en  7035  acneq  7345  addcanpig  7482  mulcanpig  7483  addcmpblnq  7515  addclnq  7523  mulclnq  7524  recexnq  7538  recmulnqg  7539  ltanqg  7548  ltmnqg  7549  ltexnqq  7556  enq0ref  7581  enq0tr  7582  addcmpblnq0  7591  mulnnnq0  7598  addclnq0  7599  mulclnq0  7600  distrnq0  7607  mulcomnq0  7608  addassnq0  7610  nq02m  7613  prarloclem3  7645  genipv  7657  genpassl  7672  genpassu  7673  addlocpr  7684  distrlem1prl  7730  distrlem1pru  7731  1idprl  7738  1idpru  7739  ltexprlemell  7746  ltexprlemelu  7747  ltexpri  7761  lteupri  7765  ltaprlem  7766  recexprlem1ssl  7781  recexprlem1ssu  7782  recexpr  7786  cauappcvgprlemm  7793  cauappcvgprlemdisj  7799  cauappcvgprlemloc  7800  cauappcvgprlemladdru  7804  cauappcvgprlemladdrl  7805  cauappcvgprlem1  7807  cauappcvgprlemlim  7809  cauappcvgpr  7810  mulcmpblnrlemg  7888  addclsr  7901  mulclsr  7902  ltasrg  7918  negexsr  7920  recexgt0sr  7921  mulgt0sr  7926  mulextsr1  7929  srpospr  7931  caucvgsrlemgt1  7943  map2psrprg  7953  axaddrcl  8013  axmulrcl  8015  axaddcom  8018  axrnegex  8027  axprecex  8028  axcnre  8029  axpre-ltadd  8034  axpre-mulgt0  8035  axpre-mulext  8036  rereceu  8037  recriota  8038  axcaucvglemres  8047  readdcan  8247  cnegexlem1  8282  cnegex  8285  addcan  8287  negeq  8300  subadd  8310  addid0  8480  ine0  8501  rimul  8693  cru  8710  apreim  8711  recexap  8761  mulcanapd  8769  receuap  8777  divmulap  8783  rerecapb  8951  cju  9069  nnaddcl  9091  nnmulcl  9092  nnsub  9110  nnnn0addcl  9360  zaddcllempos  9444  zaddcl  9447  zdiv  9496  deceq1  9543  deceq2  9544  uzaddcl  9742  zq  9782  qreccl  9798  cnref1o  9807  xaddnemnf  10014  xaddnepnf  10015  xaddcom  10018  xnn0xadd0  10024  xnegdi  10025  xaddass  10026  xlt2add  10037  xlesubadd  10040  xleaddadd  10044  fzsuc2  10236  fzrevral  10262  fzshftral  10265  2ffzeq  10298  exfzdc  10406  exbtwnzlemshrink  10428  rebtwn2zlemshrink  10433  modqval  10506  modqmuladd  10548  modqmuladdnn0  10550  frecuzrdgrrn  10590  frec2uzrdg  10591  frecuzrdgrcl  10592  frecuzrdgsuc  10596  frecuzrdgrclt  10597  frecuzrdgg  10598  frecuzrdgsuctlem  10605  frecfzennn  10608  uzsinds  10626  iseqvalcbv  10641  seq3val  10642  seqvalcd  10643  seqovcd  10649  seq3caopr3  10673  seq3caopr2  10675  seqcaopr2g  10676  seq3f1olemp  10697  seqf1og  10703  seq3id  10707  seq3homo  10709  seq3z  10710  seqhomog  10712  seqfeq4g  10713  seq3distr  10714  expp1  10728  expnegap0  10729  expcllem  10732  expcl2lemap  10733  m1expcl2  10743  expap0  10751  mulexp  10760  expadd  10763  expmul  10766  leexp2r  10775  leexp1a  10776  bernneq  10842  expnbnd  10845  modqexp  10848  nn0ltexp2  10891  expcan  10898  apexp1  10900  facdiv  10920  faclbnd3  10925  faclbnd6  10926  bcval  10931  bcpasc  10948  bccl  10949  fz1eqb  10972  omgadd  10984  hashunlem  10986  hashfzo  11004  hashfzp1  11006  iswrdinn0  11036  wrdnval  11061  eqwrd  11071  eqs1  11120  pfxeq  11187  ccatopth  11207  wrd2ind  11214  swrdccatin1  11216  swrdccatin2  11220  pfxccatin12lem2  11222  swrdccat3blem  11230  pfxccatid  11232  swrdccatin1d  11234  swrdccatin2d  11235  shftfvalg  11244  shftfval  11247  cjth  11272  remim  11286  reim0b  11288  cjexp  11319  cnrecnv  11336  cvg1nlemcau  11410  cvg1nlemres  11411  recvguniq  11421  resqrexlemp1rp  11432  resqrexlemfp1  11435  resqrexlemlo  11439  resqrexlemgt0  11446  resqrexlemoverl  11447  resqrexlemglsq  11448  resqrexlemsqa  11450  resqrexlemex  11451  resqrex  11452  absexp  11505  recan  11535  climcn2  11735  subcn2  11737  summodc  11809  fsum3  11813  fsum3cvg3  11822  fsumrev  11869  fisum0diag2  11873  telfsumo  11892  fsumrelem  11897  binomlem  11909  binom  11910  binom1dif  11913  bcxmaslem1  11914  bcxmas  11915  isumshft  11916  divcnv  11923  arisum  11924  trireciplem  11926  expcnvap0  11928  expcnvre  11929  expcnv  11930  explecnv  11931  geosergap  11932  geolim  11937  geolim2  11938  geo2sum  11940  geo2lim  11942  geoisum  11943  geoisumr  11944  geoisum1  11945  geoisum1c  11946  cvgratnnlemsumlt  11954  cvgratz  11958  prodmodc  12004  fprodseq  12009  fprodcl2lem  12031  fprodfac  12041  fprodabs  12042  fprodrev  12045  eftvalcn  12083  efcvgfsum  12093  ege2le3  12097  efcj  12099  efaddlem  12100  efexp  12108  eftlub  12116  efgt1p2  12121  eflegeo  12127  sinval  12128  cosval  12129  demoivreALT  12200  divides  12215  dvdscmul  12244  dvds2ln  12250  dvdstr  12254  odd2np1lem  12298  odd2np1  12299  2tp1odd  12310  opeo  12323  omeo  12324  m1expe  12325  m1expo  12326  m1exp1  12327  divalglemnn  12344  divalglemeunn  12347  divalglemeuneg  12349  divalgmod  12353  ndvdssub  12356  bitsval  12369  bitsfzolem  12380  bitsinv1lem  12387  bitsinv1  12388  gcd0id  12415  bezoutlemnewy  12432  bezoutlema  12435  bezoutlemb  12436  bezoutlemex  12437  bezoutlemaz  12439  bezoutlembz  12440  gcdmultiple  12456  gcdmultiplez  12457  dvdsmulgcd  12461  rplpwr  12463  nn0seqcvgd  12478  dvdslcm  12506  lcmeq0  12508  lcmcl  12509  lcmneg  12511  lcmgcdlem  12514  lcmdvds  12516  lcmid  12517  lcmgcdeq  12520  coprmdvds  12529  mulgcddvds  12531  qredeq  12533  cncongr1  12540  cncongr2  12541  cncongrcoprm  12543  prmind2  12557  isprm6  12584  prmdvdsexp  12585  prmdvdsexpr  12587  sqrt2irr  12599  pw2dvdslemn  12602  pw2dvdseu  12605  oddpwdclemxy  12606  sqpweven  12612  2sqpwodd  12613  sqne2sq  12614  nn0gcdsq  12637  qden1elz  12642  phival  12650  dfphi2  12657  eulerthlemrprm  12666  eulerthlema  12667  prmdiv  12672  prmdiveq  12673  phisum  12678  odzval  12679  odzcllem  12680  odzdvds  12683  reumodprminv  12691  pythagtriplem3  12705  pythagtriplem18  12719  pythagtriplem19  12720  pclem0  12724  pclemub  12725  pclemdc  12726  pcprecl  12727  pcprendvds  12728  pcpremul  12731  pceulem  12732  pceu  12733  pczpre  12735  pcdiv  12740  pcqmul  12741  pcqcl  12744  pcexp  12747  pcxnn0cl  12748  pcxcl  12749  pcge0  12751  pcdvdsb  12758  pcneg  12763  pcabs  12764  pcgcd1  12766  pc2dvds  12768  pc11  12769  pcz  12770  pcprmpw2  12771  pcprmpw  12772  dvdsprmpweq  12773  dvdsprmpweqnn  12774  dvdsprmpweqle  12775  pcaddlem  12777  pcadd  12778  pcfac  12788  oddprmdvds  12792  prmpwdvds  12793  pockthi  12796  infpnlem2  12798  1arithlem1  12801  4sqlemffi  12834  4sqlem12  12840  2expltfac  12877  ennnfonelemnn0  12908  ennnfonelemr  12909  f1ovscpbl  13259  imasaddvallemg  13262  ercpbl  13278  mgm1  13317  mgmidmo  13319  mgmlrid  13326  lidrideqd  13328  lidrididd  13329  grpinvalem  13332  grpinva  13333  gsumfzval  13338  gsumval2  13344  isnsgrp  13353  sgrpass  13355  sgrp1  13358  mndinvmod  13392  imasmnd2  13399  mnd1  13402  mnd1id  13403  mhmpropd  13413  mhmlin  13414  insubm  13432  mhmima  13438  gsumwsubmcl  13443  gsumwmhm  13445  grpinvex  13457  grppropd  13464  dfgrp2  13474  grpidd2  13488  grpinvval  13490  grpinvid1  13499  grplrinv  13504  grpidinv2  13505  grpidinv  13506  grplcan  13509  grpidssd  13523  grpinvssd  13524  dfgrp3mlem  13545  dfgrp3m  13546  grplactcnv  13549  grp1  13553  imasgrp2  13561  mhmlem  13565  mulgnn0gsum  13579  mulginvcom  13598  mulgnn0ass  13609  mulgmodid  13612  issubg  13624  issubg2m  13640  issubg4m  13644  isnsg2  13654  nsgbi  13655  isnsg3  13658  elnmz  13659  nmzbi  13660  ghmlin  13699  ghmrn  13708  ghmnsgima  13719  conjghm  13727  conjnmz  13730  gsumfzconst  13792  rngdi  13817  rngdir  13818  srglz  13862  srgisid  13863  srglmhm  13870  ringid  13903  ringinvnz1ne0  13926  ringinvnzdiv  13927  ring1  13936  ringlghm  13938  imasring  13941  dvdsrtr  13978  lringuplu  14073  issubrng  14076  issubrng2  14087  issubrg  14098  issubrg2  14118  rrgeq0i  14141  rrgeq0  14142  unitrrg  14144  domneq0  14149  lmodlema  14169  islmodd  14170  rmodislmodlem  14227  rmodislmod  14228  lssclg  14241  lss1d  14260  rnglidlmcl  14357  quscrng  14410  cnfldexp  14454  gsumfzfsumlemm  14464  cnfldui  14466  expghmap  14484  zrhval  14494  zrhvalg  14495  znunit  14536  txdis1cn  14865  cnmptcom  14885  psmettri2  14915  isxmet2d  14935  xmeteq0  14946  xmettri2  14948  elblps  14977  elbl  14978  blssps  15014  blss  15015  ssblex  15018  blin2  15019  metss2  15085  comet  15086  bdmopn  15091  txmetcnp  15105  blssioo  15140  divcnap  15152  mpomulcn  15153  expcn  15156  cncfval  15159  cncfi  15165  mulc1cncf  15176  cdivcncfap  15191  mulcncf  15195  expcncf  15196  cnopnap  15198  ellimc3apf  15247  cnlimci  15260  limccnpcntop  15262  limccnp2lem  15263  reldvg  15266  eldvap  15269  dvexp  15298  dvexp2  15299  dvrecap  15300  elplyr  15327  elplyd  15328  ply1termlem  15329  plymullem1  15335  plyadd  15338  plymul  15339  plycoeid3  15344  plycolemc  15345  plyco  15346  plycj  15348  dvply1  15352  dvply2g  15353  sin0pilem2  15369  rpcxpmul2  15500  relogbcxpbap  15552  logbgcd1irr  15554  2irrexpq  15563  2irrexpqap  15565  dvdsppwf1o  15576  mpodvdsmulf1o  15577  fsumdvdsmul  15578  sgmppw  15579  1sgmprm  15581  perfect  15588  lgsneg  15616  lgsdilem  15619  lgsdir  15627  lgsdilem2  15628  lgsdi  15629  lgsne0  15630  lgsdirnn0  15639  lgsdinn0  15640  gausslemma2dlem4  15656  lgseisenlem2  15663  lgseisenlem3  15664  lgseisenlem4  15665  lgsquadlem1  15669  lgsquadlem2  15670  lgsquad2lem2  15674  2lgs  15696  2sqlem6  15712  2sqlem8  15715  2sqlem9  15716  2sqlem10  15717  trilpolemclim  16177  trilpolemcl  16178  trilpolemisumle  16179  trilpolemeq1  16181  trilpolemlt1  16182  trilpo  16184  trirec0  16185  redcwlpo  16196  nconstwlpolemgt0  16205  nconstwlpo  16207  neapmkv  16209