Theorem oveq2 6036

Description: Equality theorem for operation value. (Contributed by NM, 28-Feb-1995.)

Assertion

Ref	Expression
oveq2	|- ( A = B -> ( C F A ) = ( C F B ) )

Proof of Theorem oveq2

Step	Hyp	Ref	Expression
1		opeq2 3868	. . 3 |- ( A = B -> <. C , A >. = <. C , B >. )
2	1	fveq2d 5652	. 2 |- ( A = B -> ( F ` <. C , A >. ) = ( F ` <. C , B >. ) )
3		df-ov 6031	. 2 |- ( C F A ) = ( F ` <. C , A >. )
4		df-ov 6031	. 2 |- ( C F B ) = ( F ` <. C , B >. )
5	2, 3, 4	3eqtr4g 2289	1 |- ( A = B -> ( C F A ) = ( C F B ) )

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  7460  addcanpig  7597  mulcanpig  7598  addcmpblnq  7630  addclnq  7638  mulclnq  7639  recexnq  7653  recmulnqg  7654  ltanqg  7663  ltmnqg  7664  ltexnqq  7671  enq0ref  7696  enq0tr  7697  addcmpblnq0  7706  mulnnnq0  7713  addclnq0  7714  mulclnq0  7715  distrnq0  7722  mulcomnq0  7723  addassnq0  7725  nq02m  7728  prarloclem3  7760  genipv  7772  genpassl  7787  genpassu  7788  addlocpr  7799  distrlem1prl  7845  distrlem1pru  7846  1idprl  7853  1idpru  7854  ltexprlemell  7861  ltexprlemelu  7862  ltexpri  7876  lteupri  7880  ltaprlem  7881  recexprlem1ssl  7896  recexprlem1ssu  7897  recexpr  7901  cauappcvgprlemm  7908  cauappcvgprlemdisj  7914  cauappcvgprlemloc  7915  cauappcvgprlemladdru  7919  cauappcvgprlemladdrl  7920  cauappcvgprlem1  7922  cauappcvgprlemlim  7924  cauappcvgpr  7925  mulcmpblnrlemg  8003  addclsr  8016  mulclsr  8017  ltasrg  8033  negexsr  8035  recexgt0sr  8036  mulgt0sr  8041  mulextsr1  8044  srpospr  8046  caucvgsrlemgt1  8058  map2psrprg  8068  axaddrcl  8128  axmulrcl  8130  axaddcom  8133  axrnegex  8142  axprecex  8143  axcnre  8144  axpre-ltadd  8149  axpre-mulgt0  8150  axpre-mulext  8151  rereceu  8152  recriota  8153  axcaucvglemres  8162  readdcan  8361  cnegexlem1  8396  cnegex  8399  addcan  8401  negeq  8414  subadd  8424  addid0  8594  ine0  8615  rimul  8807  cru  8824  apreim  8825  recexap  8875  mulcanapd  8883  receuap  8891  divmulap  8897  rerecapb  9065  cju  9183  nnaddcl  9205  nnmulcl  9206  nnsub  9224  nnnn0addcl  9474  zaddcllempos  9560  zaddcl  9563  zdiv  9612  deceq1  9659  deceq2  9660  uzaddcl  9864  zq  9904  qreccl  9920  cnref1o  9929  xaddnemnf  10136  xaddnepnf  10137  xaddcom  10140  xnn0xadd0  10146  xnegdi  10147  xaddass  10148  xlt2add  10159  xlesubadd  10162  xleaddadd  10166  fzsuc2  10359  fzrevral  10385  fzshftral  10388  2ffzeq  10421  exfzdc  10532  exbtwnzlemshrink  10554  rebtwn2zlemshrink  10559  modqval  10632  modqmuladd  10674  modqmuladdnn0  10676  frecuzrdgrrn  10716  frec2uzrdg  10717  frecuzrdgrcl  10718  frecuzrdgsuc  10722  frecuzrdgrclt  10723  frecuzrdgg  10724  frecuzrdgsuctlem  10731  frecfzennn  10734  uzsinds  10752  iseqvalcbv  10767  seq3val  10768  seqvalcd  10769  seqovcd  10775  seq3caopr3  10799  seq3caopr2  10801  seqcaopr2g  10802  seq3f1olemp  10823  seqf1og  10829  seq3id  10833  seq3homo  10835  seq3z  10836  seqhomog  10838  seqfeq4g  10839  seq3distr  10840  expp1  10854  expnegap0  10855  expcllem  10858  expcl2lemap  10859  m1expcl2  10869  expap0  10877  mulexp  10886  expadd  10889  expmul  10892  leexp2r  10901  leexp1a  10902  bernneq  10968  expnbnd  10971  modqexp  10974  nn0ltexp2  11017  expcan  11024  apexp1  11026  facdiv  11046  faclbnd3  11051  faclbnd6  11052  bcval  11057  bcpasc  11074  bccl  11075  fz1eqb  11098  omgadd  11111  hashunlem  11113  hashfzo  11132  hashfzp1  11134  iswrdinn0  11167  wrdnval  11193  eqwrd  11203  eqs1  11254  pfxeq  11326  ccatopth  11346  wrd2ind  11353  swrdccatin1  11355  swrdccatin2  11359  pfxccatin12lem2  11361  swrdccat3blem  11369  pfxccatid  11371  swrdccatin1d  11373  swrdccatin2d  11374  s2dmg  11420  shftfvalg  11441  shftfval  11444  cjth  11469  remim  11483  reim0b  11485  cjexp  11516  cnrecnv  11533  cvg1nlemcau  11607  cvg1nlemres  11608  recvguniq  11618  resqrexlemp1rp  11629  resqrexlemfp1  11632  resqrexlemlo  11636  resqrexlemgt0  11643  resqrexlemoverl  11644  resqrexlemglsq  11645  resqrexlemsqa  11647  resqrexlemex  11648  resqrex  11649  absexp  11702  recan  11732  climcn2  11932  subcn2  11934  summodc  12007  fsum3  12011  fsum3cvg3  12020  fsumrev  12067  fisum0diag2  12071  telfsumo  12090  fsumrelem  12095  binomlem  12107  binom  12108  binom1dif  12111  bcxmaslem1  12112  bcxmas  12113  isumshft  12114  divcnv  12121  arisum  12122  trireciplem  12124  expcnvap0  12126  expcnvre  12127  expcnv  12128  explecnv  12129  geosergap  12130  geolim  12135  geolim2  12136  geo2sum  12138  geo2lim  12140  geoisum  12141  geoisumr  12142  geoisum1  12143  geoisum1c  12144  cvgratnnlemsumlt  12152  cvgratz  12156  prodmodc  12202  fprodseq  12207  fprodcl2lem  12229  fprodfac  12239  fprodabs  12240  fprodrev  12243  eftvalcn  12281  efcvgfsum  12291  ege2le3  12295  efcj  12297  efaddlem  12298  efexp  12306  eftlub  12314  efgt1p2  12319  eflegeo  12325  sinval  12326  cosval  12327  demoivreALT  12398  divides  12413  dvdscmul  12442  dvds2ln  12448  dvdstr  12452  odd2np1lem  12496  odd2np1  12497  2tp1odd  12508  opeo  12521  omeo  12522  m1expe  12523  m1expo  12524  m1exp1  12525  divalglemnn  12542  divalglemeunn  12545  divalglemeuneg  12547  divalgmod  12551  ndvdssub  12554  bitsval  12567  bitsfzolem  12578  bitsinv1lem  12585  bitsinv1  12586  gcd0id  12613  bezoutlemnewy  12630  bezoutlema  12633  bezoutlemb  12634  bezoutlemex  12635  bezoutlemaz  12637  bezoutlembz  12638  gcdmultiple  12654  gcdmultiplez  12655  dvdsmulgcd  12659  rplpwr  12661  nn0seqcvgd  12676  dvdslcm  12704  lcmeq0  12706  lcmcl  12707  lcmneg  12709  lcmgcdlem  12712  lcmdvds  12714  lcmid  12715  lcmgcdeq  12718  coprmdvds  12727  mulgcddvds  12729  qredeq  12731  cncongr1  12738  cncongr2  12739  cncongrcoprm  12741  prmind2  12755  isprm6  12782  prmdvdsexp  12783  prmdvdsexpr  12785  sqrt2irr  12797  pw2dvdslemn  12800  pw2dvdseu  12803  oddpwdclemxy  12804  sqpweven  12810  2sqpwodd  12811  sqne2sq  12812  nn0gcdsq  12835  qden1elz  12840  phival  12848  dfphi2  12855  eulerthlemrprm  12864  eulerthlema  12865  prmdiv  12870  prmdiveq  12871  phisum  12876  odzval  12877  odzcllem  12878  odzdvds  12881  reumodprminv  12889  pythagtriplem3  12903  pythagtriplem18  12917  pythagtriplem19  12918  pclem0  12922  pclemub  12923  pclemdc  12924  pcprecl  12925  pcprendvds  12926  pcpremul  12929  pceulem  12930  pceu  12931  pczpre  12933  pcdiv  12938  pcqmul  12939  pcqcl  12942  pcexp  12945  pcxnn0cl  12946  pcxcl  12947  pcge0  12949  pcdvdsb  12956  pcneg  12961  pcabs  12962  pcgcd1  12964  pc2dvds  12966  pc11  12967  pcz  12968  pcprmpw2  12969  pcprmpw  12970  dvdsprmpweq  12971  dvdsprmpweqnn  12972  dvdsprmpweqle  12973  pcaddlem  12975  pcadd  12976  pcfac  12986  oddprmdvds  12990  prmpwdvds  12991  pockthi  12994  infpnlem2  12996  1arithlem1  12999  4sqlemffi  13032  4sqlem12  13038  2expltfac  13075  ennnfonelemnn0  13106  ennnfonelemr  13107  f1ovscpbl  13458  imasaddvallemg  13461  ercpbl  13477  mgm1  13516  mgmidmo  13518  mgmlrid  13525  lidrideqd  13527  lidrididd  13528  grpinvalem  13531  grpinva  13532  gsumfzval  13537  gsumval2  13543  isnsgrp  13552  sgrpass  13554  sgrp1  13557  mndinvmod  13591  imasmnd2  13598  mnd1  13601  mnd1id  13602  mhmpropd  13612  mhmlin  13613  insubm  13631  mhmima  13637  gsumwsubmcl  13642  gsumwmhm  13644  grpinvex  13656  grppropd  13663  dfgrp2  13673  grpidd2  13687  grpinvval  13689  grpinvid1  13698  grplrinv  13703  grpidinv2  13704  grpidinv  13705  grplcan  13708  grpidssd  13722  grpinvssd  13723  dfgrp3mlem  13744  dfgrp3m  13745  grplactcnv  13748  grp1  13752  imasgrp2  13760  mhmlem  13764  mulgnn0gsum  13778  mulginvcom  13797  mulgnn0ass  13808  mulgmodid  13811  issubg  13823  issubg2m  13839  issubg4m  13843  isnsg2  13853  nsgbi  13854  isnsg3  13857  elnmz  13858  nmzbi  13859  ghmlin  13898  ghmrn  13907  ghmnsgima  13918  conjghm  13926  conjnmz  13929  gsumfzconst  13991  rngdi  14017  rngdir  14018  srglz  14062  srgisid  14063  srglmhm  14070  ringid  14103  ringinvnz1ne0  14126  ringinvnzdiv  14127  ring1  14136  ringlghm  14138  imasring  14141  dvdsrtr  14179  lringuplu  14274  issubrng  14277  issubrng2  14288  issubrg  14299  issubrg2  14319  rrgeq0i  14342  rrgeq0  14343  unitrrg  14346  domneq0  14351  lmodlema  14371  islmodd  14372  rmodislmodlem  14429  rmodislmod  14430  lssclg  14443  lss1d  14462  rnglidlmcl  14559  quscrng  14612  cnfldexp  14656  gsumfzfsumlemm  14666  cnfldui  14668  expghmap  14686  zrhval  14696  zrhvalg  14697  znunit  14738  txdis1cn  15072  cnmptcom  15092  psmettri2  15122  isxmet2d  15142  xmeteq0  15153  xmettri2  15155  elblps  15184  elbl  15185  blssps  15221  blss  15222  ssblex  15225  blin2  15226  metss2  15292  comet  15293  bdmopn  15298  txmetcnp  15312  blssioo  15347  divcnap  15359  mpomulcn  15360  expcn  15363  cncfval  15366  cncfi  15372  mulc1cncf  15383  cdivcncfap  15398  mulcncf  15402  expcncf  15403  cnopnap  15405  ellimc3apf  15454  cnlimci  15467  limccnpcntop  15469  limccnp2lem  15470  reldvg  15473  eldvap  15476  dvexp  15505  dvexp2  15506  dvrecap  15507  elplyr  15534  elplyd  15535  ply1termlem  15536  plymullem1  15542  plyadd  15545  plymul  15546  plycoeid3  15551  plycolemc  15552  plyco  15553  plycj  15555  dvply1  15559  dvply2g  15560  sin0pilem2  15576  rpcxpmul2  15707  relogbcxpbap  15759  logbgcd1irr  15761  2irrexpq  15770  2irrexpqap  15772  dvdsppwf1o  15786  mpodvdsmulf1o  15787  fsumdvdsmul  15788  sgmppw  15789  1sgmprm  15791  perfect  15798  lgsneg  15826  lgsdilem  15829  lgsdir  15837  lgsdilem2  15838  lgsdi  15839  lgsne0  15840  lgsdirnn0  15849  lgsdinn0  15850  gausslemma2dlem4  15866  lgseisenlem2  15873  lgseisenlem3  15874  lgseisenlem4  15875  lgsquadlem1  15879  lgsquadlem2  15880  lgsquad2lem2  15884  2lgs  15906  2sqlem6  15922  2sqlem8  15925  2sqlem9  15926  2sqlem10  15927  wlkeq  16278  wlkl1loop  16282  uspgr2wlkeq  16289  upgr2wlkdc  16301  clwwlknonmpo  16352  eupth2fi  16403  trilpolemclim  16751  trilpolemcl  16752  trilpolemisumle  16753  trilpolemeq1  16755  trilpolemlt1  16756  trilpo  16758  trirec0  16759  qdiff  16764  redcwlpo  16771  nconstwlpolemgt0  16780  nconstwlpo  16782  neapmkv  16784