Theorem oveq2 6093

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

This proof depends on syntax axioms:   → wi 4   = wceq 1402  ⟨cop 3712  ‘cfv 5377  (class class class)co 6085

This proof depends on 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 proof 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 3715  df-pr 3716  df-op 3718  df-uni 3936  df-br 4131  df-iota 5337  df-fv 5385  df-ov 6088

This theorem is used by:  oveq12  6094  oveq2i  6096  oveq2d  6101  ovanraleqv  6109  ovrspc2v  6111  oveqrspc2v  6112  rspceov  6128  fovcld  6193  ovmpos  6212  ov2gf  6213  ovi3  6226  caovclg  6242  caovcomg  6245  caovassg  6248  caovcang  6251  caovcan  6254  caovordig  6255  caovordg  6257  caovord  6261  caovdig  6264  caovdirg  6267  caovimo  6283  suppssov1  6299  off  6315  caofid0l  6329  caofid2  6332  caofdig  6336  suppofss1dcl  6504  suppofss2dcl  6505  omv  6728  oeiv  6729  oasuc  6737  oawordriexmid  6743  omsuc  6745  nna0r  6751  nnm0r  6752  nnacl  6753  nnmcl  6754  nnacom  6757  nnaass  6758  nndi  6759  nnmass  6760  nnmsucr  6761  nnmcom  6762  nnaordi  6781  nnaord  6782  nnmordi  6789  nnmord  6790  nnaordex  6801  nnawordex  6802  nnm00  6803  eroveu  6900  ecopovtrn  6906  ecopovtrng  6909  th3qlem2  6912  th3q  6914  ecovcom  6916  ecovicom  6917  ecovass  6918  ecoviass  6919  ecovdi  6920  ecovidi  6921  exmidpw2en  7219  mapfi  7261  acneq  7559  addcanpig  7702  mulcanpig  7703  addcmpblnq  7735  addclnq  7743  mulclnq  7744  recexnq  7758  recmulnqg  7759  ltanqg  7768  ltmnqg  7769  ltexnqq  7776  enq0ref  7801  enq0tr  7802  addcmpblnq0  7811  mulnnnq0  7818  addclnq0  7819  mulclnq0  7820  distrnq0  7827  mulcomnq0  7828  addassnq0  7830  nq02m  7833  prarloclem3  7865  genipv  7877  genpassl  7892  genpassu  7893  addlocpr  7904  distrlem1prl  7950  distrlem1pru  7951  1idprl  7958  1idpru  7959  ltexprlemell  7966  ltexprlemelu  7967  ltexpri  7981  lteupri  7985  ltaprlem  7986  recexprlem1ssl  8001  recexprlem1ssu  8002  recexpr  8006  cauappcvgprlemm  8013  cauappcvgprlemdisj  8019  cauappcvgprlemloc  8020  cauappcvgprlemladdru  8024  cauappcvgprlemladdrl  8025  cauappcvgprlem1  8027  cauappcvgprlemlim  8029  cauappcvgpr  8030  mulcmpblnrlemg  8108  addclsr  8121  mulclsr  8122  ltasrg  8138  negexsr  8140  recexgt0sr  8141  mulgt0sr  8146  mulextsr1  8149  srpospr  8151  caucvgsrlemgt1  8163  map2psrprg  8173  axaddrcl  8233  axmulrcl  8235  axaddcom  8238  axrnegex  8247  axprecex  8248  axcnre  8249  axpre-ltadd  8254  axpre-mulgt0  8255  axpre-mulext  8256  rereceu  8257  recriota  8258  axcaucvglemres  8267  readdcan  8468  cnegexlem1  8503  cnegex  8506  addcan  8508  negeq  8521  subadd  8531  addid0  8701  ine0  8723  rimul  8916  cru  8933  apreim  8934  recexap  8984  mulcanapd  8992  receuap  9002  divmulap  9008  rerecapb  9176  cju  9294  nnaddcl  9327  nnmulcl  9328  nnsub  9346  nnnn0addcl  9598  zaddcllempos  9686  zaddcl  9689  zdiv  9739  deceq1  9786  deceq2  9787  uzaddcl  9996  zq  10036  qreccl  10052  cnref1o  10062  xaddnemnf  10270  xaddnepnf  10271  xaddcom  10274  xnn0xadd0  10280  xnegdi  10281  xaddass  10282  xlt2add  10293  xlesubadd  10296  xleaddadd  10300  fzsuc2  10497  fzrevral  10523  fzshftral  10526  2ffzeq  10559  exfzdc  10670  exbtwnzlemshrink  10694  rebtwn2zlemshrink  10699  modqval  10776  modqmuladd  10818  modqmuladdnn0  10820  frecuzrdgrrn  10860  frec2uzrdg  10861  frecuzrdgrcl  10862  frecuzrdgsuc  10866  frecuzrdgrclt  10867  frecuzrdgg  10868  frecuzrdgsuctlem  10875  frecfzennn  10878  uzsinds  10896  iseqvalcbv  10911  seq3val  10912  seqvalcd  10913  seqovcd  10919  seq3caopr3  10943  seq3caopr2  10945  seqcaopr2g  10946  seq3f1olemp  10967  seqf1og  10973  seq3id  10977  seq3homo  10979  seq3z  10980  seqhomog  10982  seqfeq4g  10983  seq3distr  10984  expp1  10998  expnegap0  10999  expcllem  11002  expcl2lemap  11003  m1expcl2  11013  expap0  11021  mulexp  11030  expadd  11033  expmul  11036  leexp2r  11045  leexp1a  11046  bernneq  11113  expnbnd  11116  modqexp  11119  nn0ltexp2  11163  expcan  11170  apexp1  11172  facdiv  11192  faclbnd3  11197  faclbnd6  11198  bcval  11203  bcpasc  11220  bccl  11221  fz1eqb  11245  omgadd  11258  hashunlem  11260  hashfzo  11279  hashfzp1  11281  hashmap  11284  hashfibclem  11298  hashfibc  11299  hashf1  11303  iswrdinn0  11325  wrdnval  11351  eqwrd  11361  eqs1  11412  pfxeq  11484  ccatopth  11504  wrd2ind  11511  swrdccatin1  11513  swrdccatin2  11517  pfxccatin12lem2  11519  swrdccat3blem  11527  pfxccatid  11529  swrdccatin1d  11531  swrdccatin2d  11532  s2dmg  11578  shftfvalg  11599  shftfval  11602  cjth  11627  remim  11641  reim0b  11643  cjexp  11674  cnrecnv  11692  cvg1nlemcau  11766  cvg1nlemres  11767  recvguniq  11777  resqrexlemp1rp  11788  resqrexlemfp1  11791  resqrexlemlo  11795  resqrexlemgt0  11802  resqrexlemoverl  11803  resqrexlemglsq  11804  resqrexlemsqa  11806  resqrexlemex  11807  resqrex  11808  absexp  11862  recan  11892  climcn2  12094  subcn2  12096  summodc  12169  fsum3  12173  fsum3cvg3  12182  fsumrev  12229  fisum0diag2  12233  telfsumo  12252  fsumrelem  12257  binomlem  12269  binom  12270  binom1dif  12273  bcxmaslem1  12274  bcxmas  12275  isumshft  12276  divcnv  12283  arisum  12284  trireciplem  12286  expcnvap0  12288  expcnvre  12289  expcnv  12290  explecnv  12291  geosergap  12292  geolim  12297  geolim2  12298  geo2sum  12300  geo2lim  12302  geoisum  12303  geoisumr  12304  geoisum1  12305  geoisum1c  12306  cvgratnnlemsumlt  12314  cvgratz  12318  prodmodc  12364  fprodseq  12369  fprodcl2lem  12391  fprodfac  12401  fprodabs  12402  fprodrev  12405  eftvalcn  12443  efcvgfsum  12453  ege2le3  12457  efcj  12459  efaddlem  12460  efexp  12468  eftlub  12476  efgt1p2  12481  eflegeo  12487  sinval  12488  cosval  12489  demoivreALT  12560  divides  12575  dvdscmul  12604  dvds2ln  12610  dvdstr  12614  odd2np1lem  12658  odd2np1  12659  2tp1odd  12670  opeo  12683  omeo  12684  m1expe  12685  m1expo  12686  m1exp1  12687  divalglemnn  12704  divalglemeunn  12707  divalglemeuneg  12709  divalgmod  12713  ndvdssub  12716  bitsval  12729  bitsfzolem  12740  bitsinv1lem  12747  bitsinv1  12748  gcd0id  12775  bezoutlemnewy  12792  bezoutlema  12795  bezoutlemb  12796  bezoutlemex  12797  bezoutlemaz  12799  bezoutlembz  12800  gcdmultiple  12816  gcdmultiplez  12817  dvdsmulgcd  12821  rplpwr  12823  nn0seqcvgd  12838  dvdslcm  12866  lcmeq0  12868  lcmcl  12869  lcmneg  12871  lcmgcdlem  12874  lcmdvds  12876  lcmid  12877  lcmgcdeq  12880  coprmdvds  12889  mulgcddvds  12891  qredeq  12893  cncongr1  12900  cncongr2  12901  cncongrcoprm  12903  prmind2  12917  isprm6  12945  prmdvdsexp  12946  prmdvdsexpr  12948  sqrt2irr  12960  pwbdvdslemn  12963  pwbdvdseu  12966  nnmaxpwlemxy  12967  sqpweven  12974  2sqpwodd  12975  sqne2sq  12976  nn0gcdsq  12999  qden1elz  13004  phival  13014  dfphi2  13021  eulerthlemrprm  13030  eulerthlema  13031  prmdiv  13036  prmdiveq  13037  phisum  13042  odzval  13043  odzcllem  13044  odzdvds  13047  reumodprminv  13055  pythagtriplem3  13069  pythagtriplem18  13083  pythagtriplem19  13084  pclem0  13088  pclemub  13089  pclemdc  13090  pcprecl  13091  pcprendvds  13092  pcpremul  13095  pceulem  13096  pceu  13097  pczpre  13099  pcdiv  13104  pcqmul  13105  pcqcl  13108  pcexp  13111  pcxnn0cl  13112  pcxcl  13113  pcge0  13115  pcdvdsb  13122  pcneg  13127  pcabs  13128  pcgcd1  13130  pc2dvds  13132  pc11  13133  pcz  13134  pcprmpw2  13135  pcprmpw  13136  dvdsprmpweq  13137  dvdsprmpweqnn  13138  dvdsprmpweqle  13139  pcaddlem  13141  pcadd  13142  pcfac  13152  oddprmdvds  13156  prmpwdvds  13157  pockthi  13160  infpnlem2  13162  1arithlem1  13165  4sqlemffi  13198  4sqlem12  13204  2expltfac  13242  ballotfilemfval  13281  ballotfilemfc0  13284  ballotfilemfcc  13285  ballotfilemsv  13305  ballotfilemsf1o  13309  ballotfi  13334  ennnfonelemnn0  13365  ennnfonelemr  13366  f1ovscpbl  13686  imasaddvallemg  13689  ercpbl  13705  mgm1  13743  mgmidmo  13745  mgmlrid  13752  lidrideqd  13754  lidrididd  13755  grpinvalem  13758  grpinva  13759  gzsumfzval  13764  gzsumval2  13767  isnsgrp  13774  sgrpass  13776  sgrp1  13779  mndinvmod  13811  imasmnd2  13812  mnd1  13815  mnd1id  13816  mhmpropd  13826  mhmlin  13827  insubm  13845  mhmima  13851  gzsumwsubmcl  13854  gzsumwmhm  13856  grpinvex  13868  grppropd  13875  dfgrp2  13885  grpidd2  13899  grpinvval  13901  grpinvid1  13910  grplrinv  13915  grpidinv2  13916  grpidinv  13917  grplcan  13920  grpidssd  13934  grpinvssd  13935  dfgrp3mlem  13956  dfgrp3m  13957  grplactcnv  13960  grp1  13964  imasgrp2  13966  mhmlem  13970  mulgnn0gzsum  13984  mulginvcom  14003  mulgnn0ass  14014  mulgmodid  14017  issubg  14029  issubg2m  14045  issubg4m  14049  isnsg2  14059  nsgbi  14060  isnsg3  14063  elnmz  14064  nmzbi  14065  ghmlin  14104  ghmrn  14113  ghmnsgima  14124  conjghm  14132  conjnmz  14135  elcntz  14148  cntzsnval  14150  elcntzsn  14151  cntzi  14156  cntzmhm  14167  gzsumconst  14227  rngdi  14323  rngdir  14324  srglz  14373  srgisid  14374  srglmhm  14381  ringid  14415  ringinvnz1ne0  14438  ringinvnzdiv  14439  ring1  14448  ringlghm  14450  imasring  14453  dvdsrtr  14492  lringuplu  14587  issubrng  14591  issubrng2  14602  issubrg  14613  issubrg2  14633  rrgeq0i  14656  rrgeq0  14657  unitrrg  14660  domneq0  14665  lmodlema  14712  islmodd  14713  rmodislmodlem  14771  rmodislmod  14772  lssclg  14785  lss1d  14804  rnglidlmcl  14901  quscrng  14954  cnfldexp  14998  gsumfsum  15007  cnfldui  15008  expghmap  15026  zrhval  15036  zrhvalg  15037  znunit  15078  assalem  15087  txdis1cn  15470  cnmptcom  15490  psmettri2  15520  isxmet2d  15540  xmeteq0  15551  xmettri2  15553  elblps  15582  elbl  15583  blssps  15619  blss  15620  ssblex  15623  blin2  15624  metss2  15690  comet  15691  bdmopn  15696  txmetcnp  15710  blssioo  15745  divcnap  15757  mpomulcn  15758  expcn  15761  cncfval  15764  cncfi  15770  mulc1cncf  15781  cdivcncfap  15796  mulcncf  15800  expcncf  15801  cnopnap  15803  ellimc3apf  15852  cnlimci  15865  limccnpcntop  15867  limccnp2lem  15868  reldvg  15871  eldvap  15874  dvexp  15903  dvexp2  15904  dvrecap  15905  elplyr  15932  elplyd  15933  ply1termlem  15934  plymullem1  15940  plyadd  15943  plymul  15944  plycoeid3  15949  plycolemc  15950  plyco  15951  plycj  15953  dvply1  15957  dvply2g  15958  sin0pilem2  15975  logfac  16090  rpcxpmul2  16110  relogbcxpbap  16162  logbgcd1irr  16164  2irrexpq  16173  2irrexpqap  16175  zprmlogbaplem2  16177  zprmlogbaplem3  16178  zprmlogbap  16179  log2tlbndlog2  16181  log2ublem2  16183  chtqcl  16205  chtqval  16206  ppiqval  16209  dvdsppwf1o  16244  mpodvdsmulf1o  16245  fsumdvdsmul  16246  sgmppw  16247  1sgmprm  16249  chtublem  16256  chtqub  16257  perfect  16262  bcmono  16265  bclbnd  16268  bposlem2  16273  bposlem7  16278  bposlem8  16279  bposlem9  16280  lgsneg  16309  lgsdilem  16312  lgsdir  16320  lgsdilem2  16321  lgsdi  16322  lgsne0  16323  lgsdirnn0  16332  lgsdinn0  16333  gausslemma2dlem4  16349  lgseisenlem2  16356  lgseisenlem3  16357  lgseisenlem4  16358  lgsquadlem1  16362  lgsquadlem2  16363  lgsquad2lem2  16367  2lgs  16389  2sqlem6  16405  2sqlem8  16408  2sqlem9  16409  2sqlem10  16410  wlkeq  16761  wlkl1loop  16765  uspgr2wlkeq  16772  upgr2wlkdc  16784  clwwlknonmpo  16835  eupth2fi  16886  trilpolemclim  17252  trilpolemcl  17253  trilpolemisumle  17254  trilpolemeq1  17256  trilpolemlt1  17257  trilpo  17259  trirec0  17260  qdiff  17265  redcwlpo  17272  nconstwlpolemgt0  17281  nconstwlpo  17283  neapmkv  17285