Theorem oveq2 6036

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 3868	. . 3 ⊢ (𝐴 = 𝐵 → ⟨𝐶, 𝐴⟩ = ⟨𝐶, 𝐵⟩)
2	1	fveq2d 5652	. 2 ⊢ (𝐴 = 𝐵 → (𝐹‘⟨𝐶, 𝐴⟩) = (𝐹‘⟨𝐶, 𝐵⟩))
3		df-ov 6031	. 2 ⊢ (𝐶𝐹𝐴) = (𝐹‘⟨𝐶, 𝐴⟩)
4		df-ov 6031	. 2 ⊢ (𝐶𝐹𝐵) = (𝐹‘⟨𝐶, 𝐵⟩)
5	2, 3, 4	3eqtr4g 2289	1 ⊢ (𝐴 = 𝐵 → (𝐶𝐹𝐴) = (𝐶𝐹𝐵))

Syntax hints:   → wi 4   = wceq 1398  ⟨cop 3676  ‘cfv 5333  (class class class)co 6028

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 717  ax-5 1496  ax-7 1497  ax-gen 1498  ax-ie1 1542  ax-ie2 1543  ax-8 1553  ax-10 1554  ax-11 1555  ax-i12 1556  ax-bndl 1558  ax-4 1559  ax-17 1575  ax-i9 1579  ax-ial 1583  ax-i5r 1584  ax-ext 2213

This theorem depends on definitions:  df-bi 117  df-3an 1007  df-tru 1401  df-nf 1510  df-sb 1811  df-clab 2218  df-cleq 2224  df-clel 2227  df-nfc 2364  df-rex 2517  df-v 2805  df-un 3205  df-sn 3679  df-pr 3680  df-op 3682  df-uni 3899  df-br 4094  df-iota 5293  df-fv 5341  df-ov 6031

This theorem is referenced by:  oveq12  6037  oveq2i  6039  oveq2d  6044  ovanraleqv  6052  ovrspc2v  6054  oveqrspc2v  6055  rspceov  6071  fovcld  6136  ovmpos  6155  ov2gf  6156  ovi3  6169  caovclg  6185  caovcomg  6188  caovassg  6191  caovcang  6194  caovcan  6197  caovordig  6198  caovordg  6200  caovord  6204  caovdig  6207  caovdirg  6210  caovimo  6226  suppssov1  6241  off  6257  caofid0l  6271  caofid2  6274  caofdig  6278  suppofss1dcl  6442  suppofss2dcl  6443  omv  6666  oeiv  6667  oasuc  6675  oawordriexmid  6681  omsuc  6683  nna0r  6689  nnm0r  6690  nnacl  6691  nnmcl  6692  nnacom  6695  nnaass  6696  nndi  6697  nnmass  6698  nnmsucr  6699  nnmcom  6700  nnaordi  6719  nnaord  6720  nnmordi  6727  nnmord  6728  nnaordex  6739  nnawordex  6740  nnm00  6741  eroveu  6838  ecopovtrn  6844  ecopovtrng  6847  th3qlem2  6850  th3q  6852  ecovcom  6854  ecovicom  6855  ecovass  6856  ecoviass  6857  ecovdi  6858  ecovidi  6859  exmidpw2en  7147  acneq  7477  addcanpig  7614  mulcanpig  7615  addcmpblnq  7647  addclnq  7655  mulclnq  7656  recexnq  7670  recmulnqg  7671  ltanqg  7680  ltmnqg  7681  ltexnqq  7688  enq0ref  7713  enq0tr  7714  addcmpblnq0  7723  mulnnnq0  7730  addclnq0  7731  mulclnq0  7732  distrnq0  7739  mulcomnq0  7740  addassnq0  7742  nq02m  7745  prarloclem3  7777  genipv  7789  genpassl  7804  genpassu  7805  addlocpr  7816  distrlem1prl  7862  distrlem1pru  7863  1idprl  7870  1idpru  7871  ltexprlemell  7878  ltexprlemelu  7879  ltexpri  7893  lteupri  7897  ltaprlem  7898  recexprlem1ssl  7913  recexprlem1ssu  7914  recexpr  7918  cauappcvgprlemm  7925  cauappcvgprlemdisj  7931  cauappcvgprlemloc  7932  cauappcvgprlemladdru  7936  cauappcvgprlemladdrl  7937  cauappcvgprlem1  7939  cauappcvgprlemlim  7941  cauappcvgpr  7942  mulcmpblnrlemg  8020  addclsr  8033  mulclsr  8034  ltasrg  8050  negexsr  8052  recexgt0sr  8053  mulgt0sr  8058  mulextsr1  8061  srpospr  8063  caucvgsrlemgt1  8075  map2psrprg  8085  axaddrcl  8145  axmulrcl  8147  axaddcom  8150  axrnegex  8159  axprecex  8160  axcnre  8161  axpre-ltadd  8166  axpre-mulgt0  8167  axpre-mulext  8168  rereceu  8169  recriota  8170  axcaucvglemres  8179  readdcan  8378  cnegexlem1  8413  cnegex  8416  addcan  8418  negeq  8431  subadd  8441  addid0  8611  ine0  8632  rimul  8824  cru  8841  apreim  8842  recexap  8892  mulcanapd  8900  receuap  8908  divmulap  8914  rerecapb  9082  cju  9200  nnaddcl  9222  nnmulcl  9223  nnsub  9241  nnnn0addcl  9491  zaddcllempos  9577  zaddcl  9580  zdiv  9629  deceq1  9676  deceq2  9677  uzaddcl  9881  zq  9921  qreccl  9937  cnref1o  9946  xaddnemnf  10153  xaddnepnf  10154  xaddcom  10157  xnn0xadd0  10163  xnegdi  10164  xaddass  10165  xlt2add  10176  xlesubadd  10179  xleaddadd  10183  fzsuc2  10376  fzrevral  10402  fzshftral  10405  2ffzeq  10438  exfzdc  10549  exbtwnzlemshrink  10571  rebtwn2zlemshrink  10576  modqval  10649  modqmuladd  10691  modqmuladdnn0  10693  frecuzrdgrrn  10733  frec2uzrdg  10734  frecuzrdgrcl  10735  frecuzrdgsuc  10739  frecuzrdgrclt  10740  frecuzrdgg  10741  frecuzrdgsuctlem  10748  frecfzennn  10751  uzsinds  10769  iseqvalcbv  10784  seq3val  10785  seqvalcd  10786  seqovcd  10792  seq3caopr3  10816  seq3caopr2  10818  seqcaopr2g  10819  seq3f1olemp  10840  seqf1og  10846  seq3id  10850  seq3homo  10852  seq3z  10853  seqhomog  10855  seqfeq4g  10856  seq3distr  10857  expp1  10871  expnegap0  10872  expcllem  10875  expcl2lemap  10876  m1expcl2  10886  expap0  10894  mulexp  10903  expadd  10906  expmul  10909  leexp2r  10918  leexp1a  10919  bernneq  10985  expnbnd  10988  modqexp  10991  nn0ltexp2  11034  expcan  11041  apexp1  11043  facdiv  11063  faclbnd3  11068  faclbnd6  11069  bcval  11074  bcpasc  11091  bccl  11092  fz1eqb  11115  omgadd  11128  hashunlem  11130  hashfzo  11149  hashfzp1  11151  iswrdinn0  11184  wrdnval  11210  eqwrd  11220  eqs1  11271  pfxeq  11343  ccatopth  11363  wrd2ind  11370  swrdccatin1  11372  swrdccatin2  11376  pfxccatin12lem2  11378  swrdccat3blem  11386  pfxccatid  11388  swrdccatin1d  11390  swrdccatin2d  11391  s2dmg  11437  shftfvalg  11458  shftfval  11461  cjth  11486  remim  11500  reim0b  11502  cjexp  11533  cnrecnv  11550  cvg1nlemcau  11624  cvg1nlemres  11625  recvguniq  11635  resqrexlemp1rp  11646  resqrexlemfp1  11649  resqrexlemlo  11653  resqrexlemgt0  11660  resqrexlemoverl  11661  resqrexlemglsq  11662  resqrexlemsqa  11664  resqrexlemex  11665  resqrex  11666  absexp  11719  recan  11749  climcn2  11949  subcn2  11951  summodc  12024  fsum3  12028  fsum3cvg3  12037  fsumrev  12084  fisum0diag2  12088  telfsumo  12107  fsumrelem  12112  binomlem  12124  binom  12125  binom1dif  12128  bcxmaslem1  12129  bcxmas  12130  isumshft  12131  divcnv  12138  arisum  12139  trireciplem  12141  expcnvap0  12143  expcnvre  12144  expcnv  12145  explecnv  12146  geosergap  12147  geolim  12152  geolim2  12153  geo2sum  12155  geo2lim  12157  geoisum  12158  geoisumr  12159  geoisum1  12160  geoisum1c  12161  cvgratnnlemsumlt  12169  cvgratz  12173  prodmodc  12219  fprodseq  12224  fprodcl2lem  12246  fprodfac  12256  fprodabs  12257  fprodrev  12260  eftvalcn  12298  efcvgfsum  12308  ege2le3  12312  efcj  12314  efaddlem  12315  efexp  12323  eftlub  12331  efgt1p2  12336  eflegeo  12342  sinval  12343  cosval  12344  demoivreALT  12415  divides  12430  dvdscmul  12459  dvds2ln  12465  dvdstr  12469  odd2np1lem  12513  odd2np1  12514  2tp1odd  12525  opeo  12538  omeo  12539  m1expe  12540  m1expo  12541  m1exp1  12542  divalglemnn  12559  divalglemeunn  12562  divalglemeuneg  12564  divalgmod  12568  ndvdssub  12571  bitsval  12584  bitsfzolem  12595  bitsinv1lem  12602  bitsinv1  12603  gcd0id  12630  bezoutlemnewy  12647  bezoutlema  12650  bezoutlemb  12651  bezoutlemex  12652  bezoutlemaz  12654  bezoutlembz  12655  gcdmultiple  12671  gcdmultiplez  12672  dvdsmulgcd  12676  rplpwr  12678  nn0seqcvgd  12693  dvdslcm  12721  lcmeq0  12723  lcmcl  12724  lcmneg  12726  lcmgcdlem  12729  lcmdvds  12731  lcmid  12732  lcmgcdeq  12735  coprmdvds  12744  mulgcddvds  12746  qredeq  12748  cncongr1  12755  cncongr2  12756  cncongrcoprm  12758  prmind2  12772  isprm6  12799  prmdvdsexp  12800  prmdvdsexpr  12802  sqrt2irr  12814  pw2dvdslemn  12817  pw2dvdseu  12820  oddpwdclemxy  12821  sqpweven  12827  2sqpwodd  12828  sqne2sq  12829  nn0gcdsq  12852  qden1elz  12857  phival  12865  dfphi2  12872  eulerthlemrprm  12881  eulerthlema  12882  prmdiv  12887  prmdiveq  12888  phisum  12893  odzval  12894  odzcllem  12895  odzdvds  12898  reumodprminv  12906  pythagtriplem3  12920  pythagtriplem18  12934  pythagtriplem19  12935  pclem0  12939  pclemub  12940  pclemdc  12941  pcprecl  12942  pcprendvds  12943  pcpremul  12946  pceulem  12947  pceu  12948  pczpre  12950  pcdiv  12955  pcqmul  12956  pcqcl  12959  pcexp  12962  pcxnn0cl  12963  pcxcl  12964  pcge0  12966  pcdvdsb  12973  pcneg  12978  pcabs  12979  pcgcd1  12981  pc2dvds  12983  pc11  12984  pcz  12985  pcprmpw2  12986  pcprmpw  12987  dvdsprmpweq  12988  dvdsprmpweqnn  12989  dvdsprmpweqle  12990  pcaddlem  12992  pcadd  12993  pcfac  13003  oddprmdvds  13007  prmpwdvds  13008  pockthi  13011  infpnlem2  13013  1arithlem1  13016  4sqlemffi  13049  4sqlem12  13055  2expltfac  13092  ennnfonelemnn0  13123  ennnfonelemr  13124  f1ovscpbl  13475  imasaddvallemg  13478  ercpbl  13494  mgm1  13533  mgmidmo  13535  mgmlrid  13542  lidrideqd  13544  lidrididd  13545  grpinvalem  13548  grpinva  13549  gsumfzval  13554  gsumval2  13560  isnsgrp  13569  sgrpass  13571  sgrp1  13574  mndinvmod  13608  imasmnd2  13615  mnd1  13618  mnd1id  13619  mhmpropd  13629  mhmlin  13630  insubm  13648  mhmima  13654  gsumwsubmcl  13659  gsumwmhm  13661  grpinvex  13673  grppropd  13680  dfgrp2  13690  grpidd2  13704  grpinvval  13706  grpinvid1  13715  grplrinv  13720  grpidinv2  13721  grpidinv  13722  grplcan  13725  grpidssd  13739  grpinvssd  13740  dfgrp3mlem  13761  dfgrp3m  13762  grplactcnv  13765  grp1  13769  imasgrp2  13777  mhmlem  13781  mulgnn0gsum  13795  mulginvcom  13814  mulgnn0ass  13825  mulgmodid  13828  issubg  13840  issubg2m  13856  issubg4m  13860  isnsg2  13870  nsgbi  13871  isnsg3  13874  elnmz  13875  nmzbi  13876  ghmlin  13915  ghmrn  13924  ghmnsgima  13935  conjghm  13943  conjnmz  13946  gsumfzconst  14008  rngdi  14034  rngdir  14035  srglz  14079  srgisid  14080  srglmhm  14087  ringid  14120  ringinvnz1ne0  14143  ringinvnzdiv  14144  ring1  14153  ringlghm  14155  imasring  14158  dvdsrtr  14196  lringuplu  14291  issubrng  14294  issubrng2  14305  issubrg  14316  issubrg2  14336  rrgeq0i  14359  rrgeq0  14360  unitrrg  14363  domneq0  14368  lmodlema  14388  islmodd  14389  rmodislmodlem  14446  rmodislmod  14447  lssclg  14460  lss1d  14479  rnglidlmcl  14576  quscrng  14629  cnfldexp  14673  gsumfzfsumlemm  14683  cnfldui  14685  expghmap  14703  zrhval  14713  zrhvalg  14714  znunit  14755  txdis1cn  15089  cnmptcom  15109  psmettri2  15139  isxmet2d  15159  xmeteq0  15170  xmettri2  15172  elblps  15201  elbl  15202  blssps  15238  blss  15239  ssblex  15242  blin2  15243  metss2  15309  comet  15310  bdmopn  15315  txmetcnp  15329  blssioo  15364  divcnap  15376  mpomulcn  15377  expcn  15380  cncfval  15383  cncfi  15389  mulc1cncf  15400  cdivcncfap  15415  mulcncf  15419  expcncf  15420  cnopnap  15422  ellimc3apf  15471  cnlimci  15484  limccnpcntop  15486  limccnp2lem  15487  reldvg  15490  eldvap  15493  dvexp  15522  dvexp2  15523  dvrecap  15524  elplyr  15551  elplyd  15552  ply1termlem  15553  plymullem1  15559  plyadd  15562  plymul  15563  plycoeid3  15568  plycolemc  15569  plyco  15570  plycj  15572  dvply1  15576  dvply2g  15577  sin0pilem2  15593  rpcxpmul2  15724  relogbcxpbap  15776  logbgcd1irr  15778  2irrexpq  15787  2irrexpqap  15789  dvdsppwf1o  15803  mpodvdsmulf1o  15804  fsumdvdsmul  15805  sgmppw  15806  1sgmprm  15808  perfect  15815  lgsneg  15843  lgsdilem  15846  lgsdir  15854  lgsdilem2  15855  lgsdi  15856  lgsne0  15857  lgsdirnn0  15866  lgsdinn0  15867  gausslemma2dlem4  15883  lgseisenlem2  15890  lgseisenlem3  15891  lgseisenlem4  15892  lgsquadlem1  15896  lgsquadlem2  15897  lgsquad2lem2  15901  2lgs  15923  2sqlem6  15939  2sqlem8  15942  2sqlem9  15943  2sqlem10  15944  wlkeq  16295  wlkl1loop  16299  uspgr2wlkeq  16306  upgr2wlkdc  16318  clwwlknonmpo  16369  eupth2fi  16420  trilpolemclim  16768  trilpolemcl  16769  trilpolemisumle  16770  trilpolemeq1  16772  trilpolemlt1  16773  trilpo  16775  trirec0  16776  qdiff  16781  redcwlpo  16788  nconstwlpolemgt0  16797  nconstwlpo  16799  neapmkv  16801