Theorem oveq2 6009

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 3858	. . 3 |- ( A = B -> <. C , A >. = <. C , B >. )
2	1	fveq2d 5631	. 2 |- ( A = B -> ( F ` <. C , A >. ) = ( F ` <. C , B >. ) )
3		df-ov 6004	. 2 |- ( C F A ) = ( F ` <. C , A >. )
4		df-ov 6004	. 2 |- ( C F B ) = ( F ` <. C , B >. )
5	2, 3, 4	3eqtr4g 2287	1 |- ( A = B -> ( C F A ) = ( C F B ) )

Syntax hints:   -> wi 4   = wceq 1395   <.cop 3669   ` cfv 5318  (class class class)co 6001

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 714  ax-5 1493  ax-7 1494  ax-gen 1495  ax-ie1 1539  ax-ie2 1540  ax-8 1550  ax-10 1551  ax-11 1552  ax-i12 1553  ax-bndl 1555  ax-4 1556  ax-17 1572  ax-i9 1576  ax-ial 1580  ax-i5r 1581  ax-ext 2211

This theorem depends on definitions:  df-bi 117  df-3an 1004  df-tru 1398  df-nf 1507  df-sb 1809  df-clab 2216  df-cleq 2222  df-clel 2225  df-nfc 2361  df-rex 2514  df-v 2801  df-un 3201  df-sn 3672  df-pr 3673  df-op 3675  df-uni 3889  df-br 4084  df-iota 5278  df-fv 5326  df-ov 6004

This theorem is referenced by:  oveq12  6010  oveq2i  6012  oveq2d  6017  ovanraleqv  6025  ovrspc2v  6027  oveqrspc2v  6028  rspceov  6044  fovcld  6109  ovmpos  6128  ov2gf  6129  ovi3  6142  caovclg  6158  caovcomg  6161  caovassg  6164  caovcang  6167  caovcan  6170  caovordig  6171  caovordg  6173  caovord  6177  caovdig  6180  caovdirg  6183  caovimo  6199  suppssov1  6215  off  6231  caofid0l  6245  caofid2  6248  caofdig  6252  omv  6601  oeiv  6602  oasuc  6610  oawordriexmid  6616  omsuc  6618  nna0r  6624  nnm0r  6625  nnacl  6626  nnmcl  6627  nnacom  6630  nnaass  6631  nndi  6632  nnmass  6633  nnmsucr  6634  nnmcom  6635  nnaordi  6654  nnaord  6655  nnmordi  6662  nnmord  6663  nnaordex  6674  nnawordex  6675  nnm00  6676  eroveu  6773  ecopovtrn  6779  ecopovtrng  6782  th3qlem2  6785  th3q  6787  ecovcom  6789  ecovicom  6790  ecovass  6791  ecoviass  6792  ecovdi  6793  ecovidi  6794  exmidpw2en  7074  acneq  7384  addcanpig  7521  mulcanpig  7522  addcmpblnq  7554  addclnq  7562  mulclnq  7563  recexnq  7577  recmulnqg  7578  ltanqg  7587  ltmnqg  7588  ltexnqq  7595  enq0ref  7620  enq0tr  7621  addcmpblnq0  7630  mulnnnq0  7637  addclnq0  7638  mulclnq0  7639  distrnq0  7646  mulcomnq0  7647  addassnq0  7649  nq02m  7652  prarloclem3  7684  genipv  7696  genpassl  7711  genpassu  7712  addlocpr  7723  distrlem1prl  7769  distrlem1pru  7770  1idprl  7777  1idpru  7778  ltexprlemell  7785  ltexprlemelu  7786  ltexpri  7800  lteupri  7804  ltaprlem  7805  recexprlem1ssl  7820  recexprlem1ssu  7821  recexpr  7825  cauappcvgprlemm  7832  cauappcvgprlemdisj  7838  cauappcvgprlemloc  7839  cauappcvgprlemladdru  7843  cauappcvgprlemladdrl  7844  cauappcvgprlem1  7846  cauappcvgprlemlim  7848  cauappcvgpr  7849  mulcmpblnrlemg  7927  addclsr  7940  mulclsr  7941  ltasrg  7957  negexsr  7959  recexgt0sr  7960  mulgt0sr  7965  mulextsr1  7968  srpospr  7970  caucvgsrlemgt1  7982  map2psrprg  7992  axaddrcl  8052  axmulrcl  8054  axaddcom  8057  axrnegex  8066  axprecex  8067  axcnre  8068  axpre-ltadd  8073  axpre-mulgt0  8074  axpre-mulext  8075  rereceu  8076  recriota  8077  axcaucvglemres  8086  readdcan  8286  cnegexlem1  8321  cnegex  8324  addcan  8326  negeq  8339  subadd  8349  addid0  8519  ine0  8540  rimul  8732  cru  8749  apreim  8750  recexap  8800  mulcanapd  8808  receuap  8816  divmulap  8822  rerecapb  8990  cju  9108  nnaddcl  9130  nnmulcl  9131  nnsub  9149  nnnn0addcl  9399  zaddcllempos  9483  zaddcl  9486  zdiv  9535  deceq1  9582  deceq2  9583  uzaddcl  9781  zq  9821  qreccl  9837  cnref1o  9846  xaddnemnf  10053  xaddnepnf  10054  xaddcom  10057  xnn0xadd0  10063  xnegdi  10064  xaddass  10065  xlt2add  10076  xlesubadd  10079  xleaddadd  10083  fzsuc2  10275  fzrevral  10301  fzshftral  10304  2ffzeq  10337  exfzdc  10446  exbtwnzlemshrink  10468  rebtwn2zlemshrink  10473  modqval  10546  modqmuladd  10588  modqmuladdnn0  10590  frecuzrdgrrn  10630  frec2uzrdg  10631  frecuzrdgrcl  10632  frecuzrdgsuc  10636  frecuzrdgrclt  10637  frecuzrdgg  10638  frecuzrdgsuctlem  10645  frecfzennn  10648  uzsinds  10666  iseqvalcbv  10681  seq3val  10682  seqvalcd  10683  seqovcd  10689  seq3caopr3  10713  seq3caopr2  10715  seqcaopr2g  10716  seq3f1olemp  10737  seqf1og  10743  seq3id  10747  seq3homo  10749  seq3z  10750  seqhomog  10752  seqfeq4g  10753  seq3distr  10754  expp1  10768  expnegap0  10769  expcllem  10772  expcl2lemap  10773  m1expcl2  10783  expap0  10791  mulexp  10800  expadd  10803  expmul  10806  leexp2r  10815  leexp1a  10816  bernneq  10882  expnbnd  10885  modqexp  10888  nn0ltexp2  10931  expcan  10938  apexp1  10940  facdiv  10960  faclbnd3  10965  faclbnd6  10966  bcval  10971  bcpasc  10988  bccl  10989  fz1eqb  11012  omgadd  11024  hashunlem  11026  hashfzo  11044  hashfzp1  11046  iswrdinn0  11076  wrdnval  11102  eqwrd  11112  eqs1  11161  pfxeq  11228  ccatopth  11248  wrd2ind  11255  swrdccatin1  11257  swrdccatin2  11261  pfxccatin12lem2  11263  swrdccat3blem  11271  pfxccatid  11273  swrdccatin1d  11275  swrdccatin2d  11276  s2dmg  11322  shftfvalg  11329  shftfval  11332  cjth  11357  remim  11371  reim0b  11373  cjexp  11404  cnrecnv  11421  cvg1nlemcau  11495  cvg1nlemres  11496  recvguniq  11506  resqrexlemp1rp  11517  resqrexlemfp1  11520  resqrexlemlo  11524  resqrexlemgt0  11531  resqrexlemoverl  11532  resqrexlemglsq  11533  resqrexlemsqa  11535  resqrexlemex  11536  resqrex  11537  absexp  11590  recan  11620  climcn2  11820  subcn2  11822  summodc  11894  fsum3  11898  fsum3cvg3  11907  fsumrev  11954  fisum0diag2  11958  telfsumo  11977  fsumrelem  11982  binomlem  11994  binom  11995  binom1dif  11998  bcxmaslem1  11999  bcxmas  12000  isumshft  12001  divcnv  12008  arisum  12009  trireciplem  12011  expcnvap0  12013  expcnvre  12014  expcnv  12015  explecnv  12016  geosergap  12017  geolim  12022  geolim2  12023  geo2sum  12025  geo2lim  12027  geoisum  12028  geoisumr  12029  geoisum1  12030  geoisum1c  12031  cvgratnnlemsumlt  12039  cvgratz  12043  prodmodc  12089  fprodseq  12094  fprodcl2lem  12116  fprodfac  12126  fprodabs  12127  fprodrev  12130  eftvalcn  12168  efcvgfsum  12178  ege2le3  12182  efcj  12184  efaddlem  12185  efexp  12193  eftlub  12201  efgt1p2  12206  eflegeo  12212  sinval  12213  cosval  12214  demoivreALT  12285  divides  12300  dvdscmul  12329  dvds2ln  12335  dvdstr  12339  odd2np1lem  12383  odd2np1  12384  2tp1odd  12395  opeo  12408  omeo  12409  m1expe  12410  m1expo  12411  m1exp1  12412  divalglemnn  12429  divalglemeunn  12432  divalglemeuneg  12434  divalgmod  12438  ndvdssub  12441  bitsval  12454  bitsfzolem  12465  bitsinv1lem  12472  bitsinv1  12473  gcd0id  12500  bezoutlemnewy  12517  bezoutlema  12520  bezoutlemb  12521  bezoutlemex  12522  bezoutlemaz  12524  bezoutlembz  12525  gcdmultiple  12541  gcdmultiplez  12542  dvdsmulgcd  12546  rplpwr  12548  nn0seqcvgd  12563  dvdslcm  12591  lcmeq0  12593  lcmcl  12594  lcmneg  12596  lcmgcdlem  12599  lcmdvds  12601  lcmid  12602  lcmgcdeq  12605  coprmdvds  12614  mulgcddvds  12616  qredeq  12618  cncongr1  12625  cncongr2  12626  cncongrcoprm  12628  prmind2  12642  isprm6  12669  prmdvdsexp  12670  prmdvdsexpr  12672  sqrt2irr  12684  pw2dvdslemn  12687  pw2dvdseu  12690  oddpwdclemxy  12691  sqpweven  12697  2sqpwodd  12698  sqne2sq  12699  nn0gcdsq  12722  qden1elz  12727  phival  12735  dfphi2  12742  eulerthlemrprm  12751  eulerthlema  12752  prmdiv  12757  prmdiveq  12758  phisum  12763  odzval  12764  odzcllem  12765  odzdvds  12768  reumodprminv  12776  pythagtriplem3  12790  pythagtriplem18  12804  pythagtriplem19  12805  pclem0  12809  pclemub  12810  pclemdc  12811  pcprecl  12812  pcprendvds  12813  pcpremul  12816  pceulem  12817  pceu  12818  pczpre  12820  pcdiv  12825  pcqmul  12826  pcqcl  12829  pcexp  12832  pcxnn0cl  12833  pcxcl  12834  pcge0  12836  pcdvdsb  12843  pcneg  12848  pcabs  12849  pcgcd1  12851  pc2dvds  12853  pc11  12854  pcz  12855  pcprmpw2  12856  pcprmpw  12857  dvdsprmpweq  12858  dvdsprmpweqnn  12859  dvdsprmpweqle  12860  pcaddlem  12862  pcadd  12863  pcfac  12873  oddprmdvds  12877  prmpwdvds  12878  pockthi  12881  infpnlem2  12883  1arithlem1  12886  4sqlemffi  12919  4sqlem12  12925  2expltfac  12962  ennnfonelemnn0  12993  ennnfonelemr  12994  f1ovscpbl  13345  imasaddvallemg  13348  ercpbl  13364  mgm1  13403  mgmidmo  13405  mgmlrid  13412  lidrideqd  13414  lidrididd  13415  grpinvalem  13418  grpinva  13419  gsumfzval  13424  gsumval2  13430  isnsgrp  13439  sgrpass  13441  sgrp1  13444  mndinvmod  13478  imasmnd2  13485  mnd1  13488  mnd1id  13489  mhmpropd  13499  mhmlin  13500  insubm  13518  mhmima  13524  gsumwsubmcl  13529  gsumwmhm  13531  grpinvex  13543  grppropd  13550  dfgrp2  13560  grpidd2  13574  grpinvval  13576  grpinvid1  13585  grplrinv  13590  grpidinv2  13591  grpidinv  13592  grplcan  13595  grpidssd  13609  grpinvssd  13610  dfgrp3mlem  13631  dfgrp3m  13632  grplactcnv  13635  grp1  13639  imasgrp2  13647  mhmlem  13651  mulgnn0gsum  13665  mulginvcom  13684  mulgnn0ass  13695  mulgmodid  13698  issubg  13710  issubg2m  13726  issubg4m  13730  isnsg2  13740  nsgbi  13741  isnsg3  13744  elnmz  13745  nmzbi  13746  ghmlin  13785  ghmrn  13794  ghmnsgima  13805  conjghm  13813  conjnmz  13816  gsumfzconst  13878  rngdi  13903  rngdir  13904  srglz  13948  srgisid  13949  srglmhm  13956  ringid  13989  ringinvnz1ne0  14012  ringinvnzdiv  14013  ring1  14022  ringlghm  14024  imasring  14027  dvdsrtr  14065  lringuplu  14160  issubrng  14163  issubrng2  14174  issubrg  14185  issubrg2  14205  rrgeq0i  14228  rrgeq0  14229  unitrrg  14231  domneq0  14236  lmodlema  14256  islmodd  14257  rmodislmodlem  14314  rmodislmod  14315  lssclg  14328  lss1d  14347  rnglidlmcl  14444  quscrng  14497  cnfldexp  14541  gsumfzfsumlemm  14551  cnfldui  14553  expghmap  14571  zrhval  14581  zrhvalg  14582  znunit  14623  txdis1cn  14952  cnmptcom  14972  psmettri2  15002  isxmet2d  15022  xmeteq0  15033  xmettri2  15035  elblps  15064  elbl  15065  blssps  15101  blss  15102  ssblex  15105  blin2  15106  metss2  15172  comet  15173  bdmopn  15178  txmetcnp  15192  blssioo  15227  divcnap  15239  mpomulcn  15240  expcn  15243  cncfval  15246  cncfi  15252  mulc1cncf  15263  cdivcncfap  15278  mulcncf  15282  expcncf  15283  cnopnap  15285  ellimc3apf  15334  cnlimci  15347  limccnpcntop  15349  limccnp2lem  15350  reldvg  15353  eldvap  15356  dvexp  15385  dvexp2  15386  dvrecap  15387  elplyr  15414  elplyd  15415  ply1termlem  15416  plymullem1  15422  plyadd  15425  plymul  15426  plycoeid3  15431  plycolemc  15432  plyco  15433  plycj  15435  dvply1  15439  dvply2g  15440  sin0pilem2  15456  rpcxpmul2  15587  relogbcxpbap  15639  logbgcd1irr  15641  2irrexpq  15650  2irrexpqap  15652  dvdsppwf1o  15663  mpodvdsmulf1o  15664  fsumdvdsmul  15665  sgmppw  15666  1sgmprm  15668  perfect  15675  lgsneg  15703  lgsdilem  15706  lgsdir  15714  lgsdilem2  15715  lgsdi  15716  lgsne0  15717  lgsdirnn0  15726  lgsdinn0  15727  gausslemma2dlem4  15743  lgseisenlem2  15750  lgseisenlem3  15751  lgseisenlem4  15752  lgsquadlem1  15756  lgsquadlem2  15757  lgsquad2lem2  15761  2lgs  15783  2sqlem6  15799  2sqlem8  15802  2sqlem9  15803  2sqlem10  15804  wlkeq  16065  wlkl1loop  16069  uspgr2wlkeq  16076  trilpolemclim  16404  trilpolemcl  16405  trilpolemisumle  16406  trilpolemeq1  16408  trilpolemlt1  16409  trilpo  16411  trirec0  16412  redcwlpo  16423  nconstwlpolemgt0  16432  nconstwlpo  16434  neapmkv  16436