Theorem oveq2 5931

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 3810	. . 3 |- ( A = B -> <. C , A >. = <. C , B >. )
2	1	fveq2d 5563	. 2 |- ( A = B -> ( F ` <. C , A >. ) = ( F ` <. C , B >. ) )
3		df-ov 5926	. 2 |- ( C F A ) = ( F ` <. C , A >. )
4		df-ov 5926	. 2 |- ( C F B ) = ( F ` <. C , B >. )
5	2, 3, 4	3eqtr4g 2254	1 |- ( A = B -> ( C F A ) = ( C F B ) )

Syntax hints:   -> wi 4   = wceq 1364   <.cop 3626   ` cfv 5259  (class class class)co 5923

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 710  ax-5 1461  ax-7 1462  ax-gen 1463  ax-ie1 1507  ax-ie2 1508  ax-8 1518  ax-10 1519  ax-11 1520  ax-i12 1521  ax-bndl 1523  ax-4 1524  ax-17 1540  ax-i9 1544  ax-ial 1548  ax-i5r 1549  ax-ext 2178

This theorem depends on definitions:  df-bi 117  df-3an 982  df-tru 1367  df-nf 1475  df-sb 1777  df-clab 2183  df-cleq 2189  df-clel 2192  df-nfc 2328  df-rex 2481  df-v 2765  df-un 3161  df-sn 3629  df-pr 3630  df-op 3632  df-uni 3841  df-br 4035  df-iota 5220  df-fv 5267  df-ov 5926

This theorem is referenced by:  oveq12  5932  oveq2i  5934  oveq2d  5939  ovanraleqv  5947  ovrspc2v  5949  oveqrspc2v  5950  rspceov  5965  fovcld  6028  ovmpos  6047  ov2gf  6048  ovi3  6061  caovclg  6077  caovcomg  6080  caovassg  6083  caovcang  6086  caovcan  6089  caovordig  6090  caovordg  6092  caovord  6096  caovdig  6099  caovdirg  6102  caovimo  6118  suppssov1  6133  off  6149  caofdig  6165  omv  6514  oeiv  6515  oasuc  6523  oawordriexmid  6529  omsuc  6531  nna0r  6537  nnm0r  6538  nnacl  6539  nnmcl  6540  nnacom  6543  nnaass  6544  nndi  6545  nnmass  6546  nnmsucr  6547  nnmcom  6548  nnaordi  6567  nnaord  6568  nnmordi  6575  nnmord  6576  nnaordex  6587  nnawordex  6588  nnm00  6589  eroveu  6686  ecopovtrn  6692  ecopovtrng  6695  th3qlem2  6698  th3q  6700  ecovcom  6702  ecovicom  6703  ecovass  6704  ecoviass  6705  ecovdi  6706  ecovidi  6707  exmidpw2en  6974  addcanpig  7403  mulcanpig  7404  addcmpblnq  7436  addclnq  7444  mulclnq  7445  recexnq  7459  recmulnqg  7460  ltanqg  7469  ltmnqg  7470  ltexnqq  7477  enq0ref  7502  enq0tr  7503  addcmpblnq0  7512  mulnnnq0  7519  addclnq0  7520  mulclnq0  7521  distrnq0  7528  mulcomnq0  7529  addassnq0  7531  nq02m  7534  prarloclem3  7566  genipv  7578  genpassl  7593  genpassu  7594  addlocpr  7605  distrlem1prl  7651  distrlem1pru  7652  1idprl  7659  1idpru  7660  ltexprlemell  7667  ltexprlemelu  7668  ltexpri  7682  lteupri  7686  ltaprlem  7687  recexprlem1ssl  7702  recexprlem1ssu  7703  recexpr  7707  cauappcvgprlemm  7714  cauappcvgprlemdisj  7720  cauappcvgprlemloc  7721  cauappcvgprlemladdru  7725  cauappcvgprlemladdrl  7726  cauappcvgprlem1  7728  cauappcvgprlemlim  7730  cauappcvgpr  7731  mulcmpblnrlemg  7809  addclsr  7822  mulclsr  7823  ltasrg  7839  negexsr  7841  recexgt0sr  7842  mulgt0sr  7847  mulextsr1  7850  srpospr  7852  caucvgsrlemgt1  7864  map2psrprg  7874  axaddrcl  7934  axmulrcl  7936  axaddcom  7939  axrnegex  7948  axprecex  7949  axcnre  7950  axpre-ltadd  7955  axpre-mulgt0  7956  axpre-mulext  7957  rereceu  7958  recriota  7959  axcaucvglemres  7968  readdcan  8168  cnegexlem1  8203  cnegex  8206  addcan  8208  negeq  8221  subadd  8231  addid0  8401  ine0  8422  rimul  8614  cru  8631  apreim  8632  recexap  8682  mulcanapd  8690  receuap  8698  divmulap  8704  rerecapb  8872  cju  8990  nnaddcl  9012  nnmulcl  9013  nnsub  9031  nnnn0addcl  9281  zaddcllempos  9365  zaddcl  9368  zdiv  9416  deceq1  9463  deceq2  9464  uzaddcl  9662  zq  9702  qreccl  9718  cnref1o  9727  xaddnemnf  9934  xaddnepnf  9935  xaddcom  9938  xnn0xadd0  9944  xnegdi  9945  xaddass  9946  xlt2add  9957  xlesubadd  9960  xleaddadd  9964  fzsuc2  10156  fzrevral  10182  fzshftral  10185  2ffzeq  10218  exfzdc  10318  exbtwnzlemshrink  10340  rebtwn2zlemshrink  10345  modqval  10418  modqmuladd  10460  modqmuladdnn0  10462  frecuzrdgrrn  10502  frec2uzrdg  10503  frecuzrdgrcl  10504  frecuzrdgsuc  10508  frecuzrdgrclt  10509  frecuzrdgg  10510  frecuzrdgsuctlem  10517  frecfzennn  10520  uzsinds  10538  iseqvalcbv  10553  seq3val  10554  seqvalcd  10555  seqovcd  10561  seq3caopr3  10585  seq3caopr2  10587  seqcaopr2g  10588  seq3f1olemp  10609  seqf1og  10615  seq3id  10619  seq3homo  10621  seq3z  10622  seqhomog  10624  seqfeq4g  10625  seq3distr  10626  expp1  10640  expnegap0  10641  expcllem  10644  expcl2lemap  10645  m1expcl2  10655  expap0  10663  mulexp  10672  expadd  10675  expmul  10678  leexp2r  10687  leexp1a  10688  bernneq  10754  expnbnd  10757  modqexp  10760  nn0ltexp2  10803  expcan  10810  apexp1  10812  facdiv  10832  faclbnd3  10837  faclbnd6  10838  bcval  10843  bcpasc  10860  bccl  10861  fz1eqb  10884  omgadd  10896  hashunlem  10898  hashfzo  10916  hashfzp1  10918  iswrdinn0  10942  wrdnval  10967  eqwrd  10977  shftfvalg  10985  shftfval  10988  cjth  11013  remim  11027  reim0b  11029  cjexp  11060  cnrecnv  11077  cvg1nlemcau  11151  cvg1nlemres  11152  recvguniq  11162  resqrexlemp1rp  11173  resqrexlemfp1  11176  resqrexlemlo  11180  resqrexlemgt0  11187  resqrexlemoverl  11188  resqrexlemglsq  11189  resqrexlemsqa  11191  resqrexlemex  11192  resqrex  11193  absexp  11246  recan  11276  climcn2  11476  subcn2  11478  summodc  11550  fsum3  11554  fsum3cvg3  11563  fsumrev  11610  fisum0diag2  11614  telfsumo  11633  fsumrelem  11638  binomlem  11650  binom  11651  binom1dif  11654  bcxmaslem1  11655  bcxmas  11656  isumshft  11657  divcnv  11664  arisum  11665  trireciplem  11667  expcnvap0  11669  expcnvre  11670  expcnv  11671  explecnv  11672  geosergap  11673  geolim  11678  geolim2  11679  geo2sum  11681  geo2lim  11683  geoisum  11684  geoisumr  11685  geoisum1  11686  geoisum1c  11687  cvgratnnlemsumlt  11695  cvgratz  11699  prodmodc  11745  fprodseq  11750  fprodcl2lem  11772  fprodfac  11782  fprodabs  11783  fprodrev  11786  eftvalcn  11824  efcvgfsum  11834  ege2le3  11838  efcj  11840  efaddlem  11841  efexp  11849  eftlub  11857  efgt1p2  11862  eflegeo  11868  sinval  11869  cosval  11870  demoivreALT  11941  divides  11956  dvdscmul  11985  dvds2ln  11991  dvdstr  11995  odd2np1lem  12039  odd2np1  12040  2tp1odd  12051  opeo  12064  omeo  12065  m1expe  12066  m1expo  12067  m1exp1  12068  divalglemnn  12085  divalglemeunn  12088  divalglemeuneg  12090  divalgmod  12094  ndvdssub  12097  bitsval  12110  bitsfzolem  12121  bitsinv1lem  12128  bitsinv1  12129  gcd0id  12156  bezoutlemnewy  12173  bezoutlema  12176  bezoutlemb  12177  bezoutlemex  12178  bezoutlemaz  12180  bezoutlembz  12181  gcdmultiple  12197  gcdmultiplez  12198  dvdsmulgcd  12202  rplpwr  12204  nn0seqcvgd  12219  dvdslcm  12247  lcmeq0  12249  lcmcl  12250  lcmneg  12252  lcmgcdlem  12255  lcmdvds  12257  lcmid  12258  lcmgcdeq  12261  coprmdvds  12270  mulgcddvds  12272  qredeq  12274  cncongr1  12281  cncongr2  12282  cncongrcoprm  12284  prmind2  12298  isprm6  12325  prmdvdsexp  12326  prmdvdsexpr  12328  sqrt2irr  12340  pw2dvdslemn  12343  pw2dvdseu  12346  oddpwdclemxy  12347  sqpweven  12353  2sqpwodd  12354  sqne2sq  12355  nn0gcdsq  12378  qden1elz  12383  phival  12391  dfphi2  12398  eulerthlemrprm  12407  eulerthlema  12408  prmdiv  12413  prmdiveq  12414  phisum  12419  odzval  12420  odzcllem  12421  odzdvds  12424  reumodprminv  12432  pythagtriplem3  12446  pythagtriplem18  12460  pythagtriplem19  12461  pclem0  12465  pclemub  12466  pclemdc  12467  pcprecl  12468  pcprendvds  12469  pcpremul  12472  pceulem  12473  pceu  12474  pczpre  12476  pcdiv  12481  pcqmul  12482  pcqcl  12485  pcexp  12488  pcxnn0cl  12489  pcxcl  12490  pcge0  12492  pcdvdsb  12499  pcneg  12504  pcabs  12505  pcgcd1  12507  pc2dvds  12509  pc11  12510  pcz  12511  pcprmpw2  12512  pcprmpw  12513  dvdsprmpweq  12514  dvdsprmpweqnn  12515  dvdsprmpweqle  12516  pcaddlem  12518  pcadd  12519  pcfac  12529  oddprmdvds  12533  prmpwdvds  12534  pockthi  12537  infpnlem2  12539  1arithlem1  12542  4sqlemffi  12575  4sqlem12  12581  2expltfac  12618  ennnfonelemnn0  12649  ennnfonelemr  12650  f1ovscpbl  12965  imasaddvallemg  12968  ercpbl  12984  mgm1  13023  mgmidmo  13025  mgmlrid  13032  lidrideqd  13034  lidrididd  13035  grpinvalem  13038  grpinva  13039  gsumfzval  13044  gsumval2  13050  isnsgrp  13059  sgrpass  13061  sgrp1  13064  mndinvmod  13096  mnd1  13097  mnd1id  13098  mhmpropd  13108  mhmlin  13109  insubm  13127  mhmima  13133  gsumwsubmcl  13138  gsumwmhm  13140  grpinvex  13152  grppropd  13159  dfgrp2  13169  grpidd2  13183  grpinvval  13185  grpinvid1  13194  grplrinv  13199  grpidinv2  13200  grpidinv  13201  grplcan  13204  grpidssd  13218  grpinvssd  13219  dfgrp3mlem  13240  dfgrp3m  13241  grplactcnv  13244  grp1  13248  imasgrp2  13250  mhmlem  13254  mulgnn0gsum  13268  mulginvcom  13287  mulgnn0ass  13298  mulgmodid  13301  issubg  13313  issubg2m  13329  issubg4m  13333  isnsg2  13343  nsgbi  13344  isnsg3  13347  elnmz  13348  nmzbi  13349  ghmlin  13388  ghmrn  13397  ghmnsgima  13408  conjghm  13416  conjnmz  13419  gsumfzconst  13481  rngdi  13506  rngdir  13507  srglz  13551  srgisid  13552  srglmhm  13559  ringid  13592  ringinvnz1ne0  13615  ringinvnzdiv  13616  ring1  13625  ringlghm  13627  imasring  13630  dvdsrtr  13667  lringuplu  13762  issubrng  13765  issubrng2  13776  issubrg  13787  issubrg2  13807  rrgeq0i  13830  rrgeq0  13831  unitrrg  13833  domneq0  13838  lmodlema  13858  islmodd  13859  rmodislmodlem  13916  rmodislmod  13917  lssclg  13930  lss1d  13949  rnglidlmcl  14046  quscrng  14099  cnfldexp  14143  gsumfzfsumlemm  14153  cnfldui  14155  expghmap  14173  zrhval  14183  zrhvalg  14184  znunit  14225  txdis1cn  14524  cnmptcom  14544  psmettri2  14574  isxmet2d  14594  xmeteq0  14605  xmettri2  14607  elblps  14636  elbl  14637  blssps  14673  blss  14674  ssblex  14677  blin2  14678  metss2  14744  comet  14745  bdmopn  14750  txmetcnp  14764  blssioo  14799  divcnap  14811  mpomulcn  14812  expcn  14815  cncfval  14818  cncfi  14824  mulc1cncf  14835  cdivcncfap  14850  mulcncf  14854  expcncf  14855  cnopnap  14857  ellimc3apf  14906  cnlimci  14919  limccnpcntop  14921  limccnp2lem  14922  reldvg  14925  eldvap  14928  dvexp  14957  dvexp2  14958  dvrecap  14959  elplyr  14986  elplyd  14987  ply1termlem  14988  plymullem1  14994  plyadd  14997  plymul  14998  plycoeid3  15003  plycolemc  15004  plyco  15005  plycj  15007  dvply1  15011  dvply2g  15012  sin0pilem2  15028  rpcxpmul2  15159  relogbcxpbap  15211  logbgcd1irr  15213  2irrexpq  15222  2irrexpqap  15224  dvdsppwf1o  15235  mpodvdsmulf1o  15236  fsumdvdsmul  15237  sgmppw  15238  1sgmprm  15240  perfect  15247  lgsneg  15275  lgsdilem  15278  lgsdir  15286  lgsdilem2  15287  lgsdi  15288  lgsne0  15289  lgsdirnn0  15298  lgsdinn0  15299  gausslemma2dlem4  15315  lgseisenlem2  15322  lgseisenlem3  15323  lgseisenlem4  15324  lgsquadlem1  15328  lgsquadlem2  15329  lgsquad2lem2  15333  2lgs  15355  2sqlem6  15371  2sqlem8  15374  2sqlem9  15375  2sqlem10  15376  trilpolemclim  15690  trilpolemcl  15691  trilpolemisumle  15692  trilpolemeq1  15694  trilpolemlt1  15695  trilpo  15697  trirec0  15698  redcwlpo  15709  nconstwlpolemgt0  15718  nconstwlpo  15720  neapmkv  15722