Theorem oveq2 6086

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 3903	. . 3 |- ( A = B -> <. C , A >. = <. C , B >. )
2	1	fveq2d 5697	. 2 |- ( A = B -> ( F ` <. C , A >. ) = ( F ` <. C , B >. ) )
3		df-ov 6081	. 2 |- ( C F A ) = ( F ` <. C , A >. )
4		df-ov 6081	. 2 |- ( C F B ) = ( F ` <. C , B >. )
5	2, 3, 4	3eqtr4g 2296	1 |- ( A = B -> ( C F A ) = ( C F B ) )

Syntax hints:   -> wi 4   = wceq 1402   <.cop 3711   ` cfv 5375  (class class class)co 6078

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 721  ax-5 1500  ax-7 1501  ax-gen 1502  ax-ie1 1546  ax-ie2 1547  ax-8 1557  ax-10 1558  ax-11 1559  ax-i12 1560  ax-bndl 1562  ax-4 1563  ax-17 1579  ax-i9 1583  ax-ial 1587  ax-i5r 1588  ax-ext 2220

This theorem depends on definitions:  df-bi 117  df-3an 1011  df-tru 1405  df-nf 1514  df-sb 1816  df-clab 2225  df-cleq 2231  df-clel 2234  df-nfc 2381  df-rex 2534  df-v 2823  df-un 3224  df-sn 3714  df-pr 3715  df-op 3717  df-uni 3934  df-br 4129  df-iota 5335  df-fv 5383  df-ov 6081

This theorem is referenced by:  oveq12  6087  oveq2i  6089  oveq2d  6094  ovanraleqv  6102  ovrspc2v  6104  oveqrspc2v  6105  rspceov  6121  fovcld  6186  ovmpos  6205  ov2gf  6206  ovi3  6219  caovclg  6235  caovcomg  6238  caovassg  6241  caovcang  6244  caovcan  6247  caovordig  6248  caovordg  6250  caovord  6254  caovdig  6257  caovdirg  6260  caovimo  6276  suppssov1  6292  off  6308  caofid0l  6322  caofid2  6325  caofdig  6329  suppofss1dcl  6497  suppofss2dcl  6498  omv  6721  oeiv  6722  oasuc  6730  oawordriexmid  6736  omsuc  6738  nna0r  6744  nnm0r  6745  nnacl  6746  nnmcl  6747  nnacom  6750  nnaass  6751  nndi  6752  nnmass  6753  nnmsucr  6754  nnmcom  6755  nnaordi  6774  nnaord  6775  nnmordi  6782  nnmord  6783  nnaordex  6794  nnawordex  6795  nnm00  6796  eroveu  6893  ecopovtrn  6899  ecopovtrng  6902  th3qlem2  6905  th3q  6907  ecovcom  6909  ecovicom  6910  ecovass  6911  ecoviass  6912  ecovdi  6913  ecovidi  6914  exmidpw2en  7212  mapfi  7254  acneq  7551  addcanpig  7694  mulcanpig  7695  addcmpblnq  7727  addclnq  7735  mulclnq  7736  recexnq  7750  recmulnqg  7751  ltanqg  7760  ltmnqg  7761  ltexnqq  7768  enq0ref  7793  enq0tr  7794  addcmpblnq0  7803  mulnnnq0  7810  addclnq0  7811  mulclnq0  7812  distrnq0  7819  mulcomnq0  7820  addassnq0  7822  nq02m  7825  prarloclem3  7857  genipv  7869  genpassl  7884  genpassu  7885  addlocpr  7896  distrlem1prl  7942  distrlem1pru  7943  1idprl  7950  1idpru  7951  ltexprlemell  7958  ltexprlemelu  7959  ltexpri  7973  lteupri  7977  ltaprlem  7978  recexprlem1ssl  7993  recexprlem1ssu  7994  recexpr  7998  cauappcvgprlemm  8005  cauappcvgprlemdisj  8011  cauappcvgprlemloc  8012  cauappcvgprlemladdru  8016  cauappcvgprlemladdrl  8017  cauappcvgprlem1  8019  cauappcvgprlemlim  8021  cauappcvgpr  8022  mulcmpblnrlemg  8100  addclsr  8113  mulclsr  8114  ltasrg  8130  negexsr  8132  recexgt0sr  8133  mulgt0sr  8138  mulextsr1  8141  srpospr  8143  caucvgsrlemgt1  8155  map2psrprg  8165  axaddrcl  8225  axmulrcl  8227  axaddcom  8230  axrnegex  8239  axprecex  8240  axcnre  8241  axpre-ltadd  8246  axpre-mulgt0  8247  axpre-mulext  8248  rereceu  8249  recriota  8250  axcaucvglemres  8259  readdcan  8459  cnegexlem1  8494  cnegex  8497  addcan  8499  negeq  8512  subadd  8522  addid0  8692  ine0  8714  rimul  8906  cru  8923  apreim  8924  recexap  8974  mulcanapd  8982  receuap  8992  divmulap  8998  rerecapb  9166  cju  9284  nnaddcl  9306  nnmulcl  9307  nnsub  9325  nnnn0addcl  9575  zaddcllempos  9663  zaddcl  9666  zdiv  9716  deceq1  9763  deceq2  9764  uzaddcl  9968  zq  10008  qreccl  10024  cnref1o  10033  xaddnemnf  10241  xaddnepnf  10242  xaddcom  10245  xnn0xadd0  10251  xnegdi  10252  xaddass  10253  xlt2add  10264  xlesubadd  10267  xleaddadd  10271  fzsuc2  10467  fzrevral  10493  fzshftral  10496  2ffzeq  10529  exfzdc  10640  exbtwnzlemshrink  10664  rebtwn2zlemshrink  10669  modqval  10742  modqmuladd  10784  modqmuladdnn0  10786  frecuzrdgrrn  10826  frec2uzrdg  10827  frecuzrdgrcl  10828  frecuzrdgsuc  10832  frecuzrdgrclt  10833  frecuzrdgg  10834  frecuzrdgsuctlem  10841  frecfzennn  10844  uzsinds  10862  iseqvalcbv  10877  seq3val  10878  seqvalcd  10879  seqovcd  10885  seq3caopr3  10909  seq3caopr2  10911  seqcaopr2g  10912  seq3f1olemp  10933  seqf1og  10939  seq3id  10943  seq3homo  10945  seq3z  10946  seqhomog  10948  seqfeq4g  10949  seq3distr  10950  expp1  10964  expnegap0  10965  expcllem  10968  expcl2lemap  10969  m1expcl2  10979  expap0  10987  mulexp  10996  expadd  10999  expmul  11002  leexp2r  11011  leexp1a  11012  bernneq  11079  expnbnd  11082  modqexp  11085  nn0ltexp2  11128  expcan  11135  apexp1  11137  facdiv  11157  faclbnd3  11162  faclbnd6  11163  bcval  11168  bcpasc  11185  bccl  11186  fz1eqb  11210  omgadd  11223  hashunlem  11225  hashfzo  11244  hashfzp1  11246  hashmap  11249  hashfibclem  11263  hashfibc  11264  hashf1  11268  iswrdinn0  11290  wrdnval  11316  eqwrd  11326  eqs1  11377  pfxeq  11449  ccatopth  11469  wrd2ind  11476  swrdccatin1  11478  swrdccatin2  11482  pfxccatin12lem2  11484  swrdccat3blem  11492  pfxccatid  11494  swrdccatin1d  11496  swrdccatin2d  11497  s2dmg  11543  shftfvalg  11564  shftfval  11567  cjth  11592  remim  11606  reim0b  11608  cjexp  11639  cnrecnv  11657  cvg1nlemcau  11731  cvg1nlemres  11732  recvguniq  11742  resqrexlemp1rp  11753  resqrexlemfp1  11756  resqrexlemlo  11760  resqrexlemgt0  11767  resqrexlemoverl  11768  resqrexlemglsq  11769  resqrexlemsqa  11771  resqrexlemex  11772  resqrex  11773  absexp  11826  recan  11856  climcn2  12056  subcn2  12058  summodc  12131  fsum3  12135  fsum3cvg3  12144  fsumrev  12191  fisum0diag2  12195  telfsumo  12214  fsumrelem  12219  binomlem  12231  binom  12232  binom1dif  12235  bcxmaslem1  12236  bcxmas  12237  isumshft  12238  divcnv  12245  arisum  12246  trireciplem  12248  expcnvap0  12250  expcnvre  12251  expcnv  12252  explecnv  12253  geosergap  12254  geolim  12259  geolim2  12260  geo2sum  12262  geo2lim  12264  geoisum  12265  geoisumr  12266  geoisum1  12267  geoisum1c  12268  cvgratnnlemsumlt  12276  cvgratz  12280  prodmodc  12326  fprodseq  12331  fprodcl2lem  12353  fprodfac  12363  fprodabs  12364  fprodrev  12367  eftvalcn  12405  efcvgfsum  12415  ege2le3  12419  efcj  12421  efaddlem  12422  efexp  12430  eftlub  12438  efgt1p2  12443  eflegeo  12449  sinval  12450  cosval  12451  demoivreALT  12522  divides  12537  dvdscmul  12566  dvds2ln  12572  dvdstr  12576  odd2np1lem  12620  odd2np1  12621  2tp1odd  12632  opeo  12645  omeo  12646  m1expe  12647  m1expo  12648  m1exp1  12649  divalglemnn  12666  divalglemeunn  12669  divalglemeuneg  12671  divalgmod  12675  ndvdssub  12678  bitsval  12691  bitsfzolem  12702  bitsinv1lem  12709  bitsinv1  12710  gcd0id  12737  bezoutlemnewy  12754  bezoutlema  12757  bezoutlemb  12758  bezoutlemex  12759  bezoutlemaz  12761  bezoutlembz  12762  gcdmultiple  12778  gcdmultiplez  12779  dvdsmulgcd  12783  rplpwr  12785  nn0seqcvgd  12800  dvdslcm  12828  lcmeq0  12830  lcmcl  12831  lcmneg  12833  lcmgcdlem  12836  lcmdvds  12838  lcmid  12839  lcmgcdeq  12842  coprmdvds  12851  mulgcddvds  12853  qredeq  12855  cncongr1  12862  cncongr2  12863  cncongrcoprm  12865  prmind2  12879  isprm6  12906  prmdvdsexp  12907  prmdvdsexpr  12909  sqrt2irr  12921  pw2dvdslemn  12924  pw2dvdseu  12927  oddpwdclemxy  12928  sqpweven  12934  2sqpwodd  12935  sqne2sq  12936  nn0gcdsq  12959  qden1elz  12964  phival  12972  dfphi2  12979  eulerthlemrprm  12988  eulerthlema  12989  prmdiv  12994  prmdiveq  12995  phisum  13000  odzval  13001  odzcllem  13002  odzdvds  13005  reumodprminv  13013  pythagtriplem3  13027  pythagtriplem18  13041  pythagtriplem19  13042  pclem0  13046  pclemub  13047  pclemdc  13048  pcprecl  13049  pcprendvds  13050  pcpremul  13053  pceulem  13054  pceu  13055  pczpre  13057  pcdiv  13062  pcqmul  13063  pcqcl  13066  pcexp  13069  pcxnn0cl  13070  pcxcl  13071  pcge0  13073  pcdvdsb  13080  pcneg  13085  pcabs  13086  pcgcd1  13088  pc2dvds  13090  pc11  13091  pcz  13092  pcprmpw2  13093  pcprmpw  13094  dvdsprmpweq  13095  dvdsprmpweqnn  13096  dvdsprmpweqle  13097  pcaddlem  13099  pcadd  13100  pcfac  13110  oddprmdvds  13114  prmpwdvds  13115  pockthi  13118  infpnlem2  13120  1arithlem1  13123  4sqlemffi  13156  4sqlem12  13162  2expltfac  13199  ballotfilemfval  13210  ballotfilemfc0  13213  ballotfilemfcc  13214  ballotfilemsv  13234  ballotfilemsf1o  13238  ballotfi  13263  ennnfonelemnn0  13294  ennnfonelemr  13295  f1ovscpbl  13613  imasaddvallemg  13616  ercpbl  13632  mgm1  13670  mgmidmo  13672  mgmlrid  13679  lidrideqd  13681  lidrididd  13682  grpinvalem  13685  grpinva  13686  gzsumfzval  13691  gzsumval2  13694  isnsgrp  13701  sgrpass  13703  sgrp1  13706  mndinvmod  13738  imasmnd2  13739  mnd1  13742  mnd1id  13743  mhmpropd  13753  mhmlin  13754  insubm  13772  mhmima  13778  gzsumwsubmcl  13781  gzsumwmhm  13783  grpinvex  13795  grppropd  13802  dfgrp2  13812  grpidd2  13826  grpinvval  13828  grpinvid1  13837  grplrinv  13842  grpidinv2  13843  grpidinv  13844  grplcan  13847  grpidssd  13861  grpinvssd  13862  dfgrp3mlem  13883  dfgrp3m  13884  grplactcnv  13887  grp1  13891  imasgrp2  13893  mhmlem  13897  mulgnn0gzsum  13911  mulginvcom  13930  mulgnn0ass  13941  mulgmodid  13944  issubg  13956  issubg2m  13972  issubg4m  13976  isnsg2  13986  nsgbi  13987  isnsg3  13990  elnmz  13991  nmzbi  13992  ghmlin  14031  ghmrn  14040  ghmnsgima  14051  conjghm  14059  conjnmz  14062  gzsumconst  14123  rngdi  14217  rngdir  14218  srglz  14266  srgisid  14267  srglmhm  14274  ringid  14307  ringinvnz1ne0  14330  ringinvnzdiv  14331  ring1  14340  ringlghm  14342  imasring  14345  dvdsrtr  14384  lringuplu  14479  issubrng  14483  issubrng2  14494  issubrg  14505  issubrg2  14525  rrgeq0i  14548  rrgeq0  14549  unitrrg  14552  domneq0  14557  lmodlema  14604  islmodd  14605  rmodislmodlem  14662  rmodislmod  14663  lssclg  14676  lss1d  14695  rnglidlmcl  14792  quscrng  14845  cnfldexp  14889  gsumfsum  14898  cnfldui  14899  expghmap  14917  zrhval  14927  zrhvalg  14928  znunit  14969  txdis1cn  15305  cnmptcom  15325  psmettri2  15355  isxmet2d  15375  xmeteq0  15386  xmettri2  15388  elblps  15417  elbl  15418  blssps  15454  blss  15455  ssblex  15458  blin2  15459  metss2  15525  comet  15526  bdmopn  15531  txmetcnp  15545  blssioo  15580  divcnap  15592  mpomulcn  15593  expcn  15596  cncfval  15599  cncfi  15605  mulc1cncf  15616  cdivcncfap  15631  mulcncf  15635  expcncf  15636  cnopnap  15638  ellimc3apf  15687  cnlimci  15700  limccnpcntop  15702  limccnp2lem  15703  reldvg  15706  eldvap  15709  dvexp  15738  dvexp2  15739  dvrecap  15740  elplyr  15767  elplyd  15768  ply1termlem  15769  plymullem1  15775  plyadd  15778  plymul  15779  plycoeid3  15784  plycolemc  15785  plyco  15786  plycj  15788  dvply1  15792  dvply2g  15793  sin0pilem2  15809  logfac  15921  rpcxpmul2  15941  relogbcxpbap  15993  logbgcd1irr  15995  2irrexpq  16004  2irrexpqap  16006  dvdsppwf1o  16020  mpodvdsmulf1o  16021  fsumdvdsmul  16022  sgmppw  16023  1sgmprm  16025  perfect  16032  lgsneg  16060  lgsdilem  16063  lgsdir  16071  lgsdilem2  16072  lgsdi  16073  lgsne0  16074  lgsdirnn0  16083  lgsdinn0  16084  gausslemma2dlem4  16100  lgseisenlem2  16107  lgseisenlem3  16108  lgseisenlem4  16109  lgsquadlem1  16113  lgsquadlem2  16114  lgsquad2lem2  16118  2lgs  16140  2sqlem6  16156  2sqlem8  16159  2sqlem9  16160  2sqlem10  16161  wlkeq  16512  wlkl1loop  16516  uspgr2wlkeq  16523  upgr2wlkdc  16535  clwwlknonmpo  16586  eupth2fi  16637  trilpolemclim  16993  trilpolemcl  16994  trilpolemisumle  16995  trilpolemeq1  16997  trilpolemlt1  16998  trilpo  17000  trirec0  17001  qdiff  17006  redcwlpo  17013  nconstwlpolemgt0  17022  nconstwlpo  17024  neapmkv  17026