Theorem oveq2 6049

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 3877	. . 3 |- ( A = B -> <. C , A >. = <. C , B >. )
2	1	fveq2d 5665	. 2 |- ( A = B -> ( F ` <. C , A >. ) = ( F ` <. C , B >. ) )
3		df-ov 6044	. 2 |- ( C F A ) = ( F ` <. C , A >. )
4		df-ov 6044	. 2 |- ( C F B ) = ( F ` <. C , B >. )
5	2, 3, 4	3eqtr4g 2290	1 |- ( A = B -> ( C F A ) = ( C F B ) )

Syntax hints:   -> wi 4   = wceq 1398   <.cop 3685   ` cfv 5343  (class class class)co 6041

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 2214

This theorem depends on definitions:  df-bi 117  df-3an 1007  df-tru 1401  df-nf 1510  df-sb 1812  df-clab 2219  df-cleq 2225  df-clel 2228  df-nfc 2373  df-rex 2526  df-v 2814  df-un 3214  df-sn 3688  df-pr 3689  df-op 3691  df-uni 3908  df-br 4103  df-iota 5303  df-fv 5351  df-ov 6044

This theorem is referenced by:  oveq12  6050  oveq2i  6052  oveq2d  6057  ovanraleqv  6065  ovrspc2v  6067  oveqrspc2v  6068  rspceov  6084  fovcld  6149  ovmpos  6168  ov2gf  6169  ovi3  6182  caovclg  6198  caovcomg  6201  caovassg  6204  caovcang  6207  caovcan  6210  caovordig  6211  caovordg  6213  caovord  6217  caovdig  6220  caovdirg  6223  caovimo  6239  suppssov1  6254  off  6270  caofid0l  6284  caofid2  6287  caofdig  6291  suppofss1dcl  6455  suppofss2dcl  6456  omv  6679  oeiv  6680  oasuc  6688  oawordriexmid  6694  omsuc  6696  nna0r  6702  nnm0r  6703  nnacl  6704  nnmcl  6705  nnacom  6708  nnaass  6709  nndi  6710  nnmass  6711  nnmsucr  6712  nnmcom  6713  nnaordi  6732  nnaord  6733  nnmordi  6740  nnmord  6741  nnaordex  6752  nnawordex  6753  nnm00  6754  eroveu  6851  ecopovtrn  6857  ecopovtrng  6860  th3qlem2  6863  th3q  6865  ecovcom  6867  ecovicom  6868  ecovass  6869  ecoviass  6870  ecovdi  6871  ecovidi  6872  exmidpw2en  7163  mapfi  7205  acneq  7500  addcanpig  7637  mulcanpig  7638  addcmpblnq  7670  addclnq  7678  mulclnq  7679  recexnq  7693  recmulnqg  7694  ltanqg  7703  ltmnqg  7704  ltexnqq  7711  enq0ref  7736  enq0tr  7737  addcmpblnq0  7746  mulnnnq0  7753  addclnq0  7754  mulclnq0  7755  distrnq0  7762  mulcomnq0  7763  addassnq0  7765  nq02m  7768  prarloclem3  7800  genipv  7812  genpassl  7827  genpassu  7828  addlocpr  7839  distrlem1prl  7885  distrlem1pru  7886  1idprl  7893  1idpru  7894  ltexprlemell  7901  ltexprlemelu  7902  ltexpri  7916  lteupri  7920  ltaprlem  7921  recexprlem1ssl  7936  recexprlem1ssu  7937  recexpr  7941  cauappcvgprlemm  7948  cauappcvgprlemdisj  7954  cauappcvgprlemloc  7955  cauappcvgprlemladdru  7959  cauappcvgprlemladdrl  7960  cauappcvgprlem1  7962  cauappcvgprlemlim  7964  cauappcvgpr  7965  mulcmpblnrlemg  8043  addclsr  8056  mulclsr  8057  ltasrg  8073  negexsr  8075  recexgt0sr  8076  mulgt0sr  8081  mulextsr1  8084  srpospr  8086  caucvgsrlemgt1  8098  map2psrprg  8108  axaddrcl  8168  axmulrcl  8170  axaddcom  8173  axrnegex  8182  axprecex  8183  axcnre  8184  axpre-ltadd  8189  axpre-mulgt0  8190  axpre-mulext  8191  rereceu  8192  recriota  8193  axcaucvglemres  8202  readdcan  8401  cnegexlem1  8436  cnegex  8439  addcan  8441  negeq  8454  subadd  8464  addid0  8634  ine0  8655  rimul  8847  cru  8864  apreim  8865  recexap  8915  mulcanapd  8923  receuap  8931  divmulap  8937  rerecapb  9105  cju  9223  nnaddcl  9245  nnmulcl  9246  nnsub  9264  nnnn0addcl  9514  zaddcllempos  9600  zaddcl  9603  zdiv  9652  deceq1  9699  deceq2  9700  uzaddcl  9904  zq  9944  qreccl  9960  cnref1o  9969  xaddnemnf  10176  xaddnepnf  10177  xaddcom  10180  xnn0xadd0  10186  xnegdi  10187  xaddass  10188  xlt2add  10199  xlesubadd  10202  xleaddadd  10206  fzsuc2  10399  fzrevral  10425  fzshftral  10428  2ffzeq  10461  exfzdc  10572  exbtwnzlemshrink  10594  rebtwn2zlemshrink  10599  modqval  10672  modqmuladd  10714  modqmuladdnn0  10716  frecuzrdgrrn  10756  frec2uzrdg  10757  frecuzrdgrcl  10758  frecuzrdgsuc  10762  frecuzrdgrclt  10763  frecuzrdgg  10764  frecuzrdgsuctlem  10771  frecfzennn  10774  uzsinds  10792  iseqvalcbv  10807  seq3val  10808  seqvalcd  10809  seqovcd  10815  seq3caopr3  10839  seq3caopr2  10841  seqcaopr2g  10842  seq3f1olemp  10863  seqf1og  10869  seq3id  10873  seq3homo  10875  seq3z  10876  seqhomog  10878  seqfeq4g  10879  seq3distr  10880  expp1  10894  expnegap0  10895  expcllem  10898  expcl2lemap  10899  m1expcl2  10909  expap0  10917  mulexp  10926  expadd  10929  expmul  10932  leexp2r  10941  leexp1a  10942  bernneq  11008  expnbnd  11011  modqexp  11014  nn0ltexp2  11057  expcan  11064  apexp1  11066  facdiv  11086  faclbnd3  11091  faclbnd6  11092  bcval  11097  bcpasc  11114  bccl  11115  fz1eqb  11138  omgadd  11151  hashunlem  11153  hashfzo  11172  hashfzp1  11174  iswrdinn0  11207  wrdnval  11233  eqwrd  11243  eqs1  11294  pfxeq  11366  ccatopth  11386  wrd2ind  11393  swrdccatin1  11395  swrdccatin2  11399  pfxccatin12lem2  11401  swrdccat3blem  11409  pfxccatid  11411  swrdccatin1d  11413  swrdccatin2d  11414  s2dmg  11460  shftfvalg  11481  shftfval  11484  cjth  11509  remim  11523  reim0b  11525  cjexp  11556  cnrecnv  11573  cvg1nlemcau  11647  cvg1nlemres  11648  recvguniq  11658  resqrexlemp1rp  11669  resqrexlemfp1  11672  resqrexlemlo  11676  resqrexlemgt0  11683  resqrexlemoverl  11684  resqrexlemglsq  11685  resqrexlemsqa  11687  resqrexlemex  11688  resqrex  11689  absexp  11742  recan  11772  climcn2  11972  subcn2  11974  summodc  12047  fsum3  12051  fsum3cvg3  12060  fsumrev  12107  fisum0diag2  12111  telfsumo  12130  fsumrelem  12135  binomlem  12147  binom  12148  binom1dif  12151  bcxmaslem1  12152  bcxmas  12153  isumshft  12154  divcnv  12161  arisum  12162  trireciplem  12164  expcnvap0  12166  expcnvre  12167  expcnv  12168  explecnv  12169  geosergap  12170  geolim  12175  geolim2  12176  geo2sum  12178  geo2lim  12180  geoisum  12181  geoisumr  12182  geoisum1  12183  geoisum1c  12184  cvgratnnlemsumlt  12192  cvgratz  12196  prodmodc  12242  fprodseq  12247  fprodcl2lem  12269  fprodfac  12279  fprodabs  12280  fprodrev  12283  eftvalcn  12321  efcvgfsum  12331  ege2le3  12335  efcj  12337  efaddlem  12338  efexp  12346  eftlub  12354  efgt1p2  12359  eflegeo  12365  sinval  12366  cosval  12367  demoivreALT  12438  divides  12453  dvdscmul  12482  dvds2ln  12488  dvdstr  12492  odd2np1lem  12536  odd2np1  12537  2tp1odd  12548  opeo  12561  omeo  12562  m1expe  12563  m1expo  12564  m1exp1  12565  divalglemnn  12582  divalglemeunn  12585  divalglemeuneg  12587  divalgmod  12591  ndvdssub  12594  bitsval  12607  bitsfzolem  12618  bitsinv1lem  12625  bitsinv1  12626  gcd0id  12653  bezoutlemnewy  12670  bezoutlema  12673  bezoutlemb  12674  bezoutlemex  12675  bezoutlemaz  12677  bezoutlembz  12678  gcdmultiple  12694  gcdmultiplez  12695  dvdsmulgcd  12699  rplpwr  12701  nn0seqcvgd  12716  dvdslcm  12744  lcmeq0  12746  lcmcl  12747  lcmneg  12749  lcmgcdlem  12752  lcmdvds  12754  lcmid  12755  lcmgcdeq  12758  coprmdvds  12767  mulgcddvds  12769  qredeq  12771  cncongr1  12778  cncongr2  12779  cncongrcoprm  12781  prmind2  12795  isprm6  12822  prmdvdsexp  12823  prmdvdsexpr  12825  sqrt2irr  12837  pw2dvdslemn  12840  pw2dvdseu  12843  oddpwdclemxy  12844  sqpweven  12850  2sqpwodd  12851  sqne2sq  12852  nn0gcdsq  12875  qden1elz  12880  phival  12888  dfphi2  12895  eulerthlemrprm  12904  eulerthlema  12905  prmdiv  12910  prmdiveq  12911  phisum  12916  odzval  12917  odzcllem  12918  odzdvds  12921  reumodprminv  12929  pythagtriplem3  12943  pythagtriplem18  12957  pythagtriplem19  12958  pclem0  12962  pclemub  12963  pclemdc  12964  pcprecl  12965  pcprendvds  12966  pcpremul  12969  pceulem  12970  pceu  12971  pczpre  12973  pcdiv  12978  pcqmul  12979  pcqcl  12982  pcexp  12985  pcxnn0cl  12986  pcxcl  12987  pcge0  12989  pcdvdsb  12996  pcneg  13001  pcabs  13002  pcgcd1  13004  pc2dvds  13006  pc11  13007  pcz  13008  pcprmpw2  13009  pcprmpw  13010  dvdsprmpweq  13011  dvdsprmpweqnn  13012  dvdsprmpweqle  13013  pcaddlem  13015  pcadd  13016  pcfac  13026  oddprmdvds  13030  prmpwdvds  13031  pockthi  13034  infpnlem2  13036  1arithlem1  13039  4sqlemffi  13072  4sqlem12  13078  2expltfac  13115  ennnfonelemnn0  13147  ennnfonelemr  13148  f1ovscpbl  13499  imasaddvallemg  13502  ercpbl  13518  mgm1  13557  mgmidmo  13559  mgmlrid  13566  lidrideqd  13568  lidrididd  13569  grpinvalem  13572  grpinva  13573  gsumfzval  13578  gsumval2  13584  isnsgrp  13593  sgrpass  13595  sgrp1  13598  mndinvmod  13632  imasmnd2  13639  mnd1  13642  mnd1id  13643  mhmpropd  13653  mhmlin  13654  insubm  13672  mhmima  13678  gsumwsubmcl  13683  gsumwmhm  13685  grpinvex  13697  grppropd  13704  dfgrp2  13714  grpidd2  13728  grpinvval  13730  grpinvid1  13739  grplrinv  13744  grpidinv2  13745  grpidinv  13746  grplcan  13749  grpidssd  13763  grpinvssd  13764  dfgrp3mlem  13785  dfgrp3m  13786  grplactcnv  13789  grp1  13793  imasgrp2  13801  mhmlem  13805  mulgnn0gsum  13819  mulginvcom  13838  mulgnn0ass  13849  mulgmodid  13852  issubg  13864  issubg2m  13880  issubg4m  13884  isnsg2  13894  nsgbi  13895  isnsg3  13898  elnmz  13899  nmzbi  13900  ghmlin  13939  ghmrn  13948  ghmnsgima  13959  conjghm  13967  conjnmz  13970  gsumfzconst  14032  rngdi  14058  rngdir  14059  srglz  14103  srgisid  14104  srglmhm  14111  ringid  14144  ringinvnz1ne0  14167  ringinvnzdiv  14168  ring1  14177  ringlghm  14179  imasring  14182  dvdsrtr  14220  lringuplu  14315  issubrng  14318  issubrng2  14329  issubrg  14340  issubrg2  14360  rrgeq0i  14383  rrgeq0  14384  unitrrg  14387  domneq0  14392  lmodlema  14412  islmodd  14413  rmodislmodlem  14470  rmodislmod  14471  lssclg  14484  lss1d  14503  rnglidlmcl  14600  quscrng  14653  cnfldexp  14697  gsumfzfsumlemm  14707  cnfldui  14709  expghmap  14727  zrhval  14737  zrhvalg  14738  znunit  14779  txdis1cn  15113  cnmptcom  15133  psmettri2  15163  isxmet2d  15183  xmeteq0  15194  xmettri2  15196  elblps  15225  elbl  15226  blssps  15262  blss  15263  ssblex  15266  blin2  15267  metss2  15333  comet  15334  bdmopn  15339  txmetcnp  15353  blssioo  15388  divcnap  15400  mpomulcn  15401  expcn  15404  cncfval  15407  cncfi  15413  mulc1cncf  15424  cdivcncfap  15439  mulcncf  15443  expcncf  15444  cnopnap  15446  ellimc3apf  15495  cnlimci  15508  limccnpcntop  15510  limccnp2lem  15511  reldvg  15514  eldvap  15517  dvexp  15546  dvexp2  15547  dvrecap  15548  elplyr  15575  elplyd  15576  ply1termlem  15577  plymullem1  15583  plyadd  15586  plymul  15587  plycoeid3  15592  plycolemc  15593  plyco  15594  plycj  15596  dvply1  15600  dvply2g  15601  sin0pilem2  15617  rpcxpmul2  15748  relogbcxpbap  15800  logbgcd1irr  15802  2irrexpq  15811  2irrexpqap  15813  dvdsppwf1o  15827  mpodvdsmulf1o  15828  fsumdvdsmul  15829  sgmppw  15830  1sgmprm  15832  perfect  15839  lgsneg  15867  lgsdilem  15870  lgsdir  15878  lgsdilem2  15879  lgsdi  15880  lgsne0  15881  lgsdirnn0  15890  lgsdinn0  15891  gausslemma2dlem4  15907  lgseisenlem2  15914  lgseisenlem3  15915  lgseisenlem4  15916  lgsquadlem1  15920  lgsquadlem2  15921  lgsquad2lem2  15925  2lgs  15947  2sqlem6  15963  2sqlem8  15966  2sqlem9  15967  2sqlem10  15968  wlkeq  16319  wlkl1loop  16323  uspgr2wlkeq  16330  upgr2wlkdc  16342  clwwlknonmpo  16393  eupth2fi  16444  trilpolemclim  16790  trilpolemcl  16791  trilpolemisumle  16792  trilpolemeq1  16794  trilpolemlt1  16795  trilpo  16797  trirec0  16798  qdiff  16803  redcwlpo  16810  nconstwlpolemgt0  16819  nconstwlpo  16821  neapmkv  16823