Theorem oveq2 6060

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 3886	. . 3 |- ( A = B -> <. C , A >. = <. C , B >. )
2	1	fveq2d 5676	. 2 |- ( A = B -> ( F ` <. C , A >. ) = ( F ` <. C , B >. ) )
3		df-ov 6055	. 2 |- ( C F A ) = ( F ` <. C , A >. )
4		df-ov 6055	. 2 |- ( C F B ) = ( F ` <. C , B >. )
5	2, 3, 4	3eqtr4g 2292	1 |- ( A = B -> ( C F A ) = ( C F B ) )

Syntax hints:   -> wi 4   = wceq 1398   <.cop 3694   ` cfv 5354  (class class class)co 6052

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 2216

This theorem depends on definitions:  df-bi 117  df-3an 1007  df-tru 1401  df-nf 1510  df-sb 1812  df-clab 2221  df-cleq 2227  df-clel 2230  df-nfc 2375  df-rex 2528  df-v 2817  df-un 3217  df-sn 3697  df-pr 3698  df-op 3700  df-uni 3917  df-br 4112  df-iota 5314  df-fv 5362  df-ov 6055

This theorem is referenced by:  oveq12  6061  oveq2i  6063  oveq2d  6068  ovanraleqv  6076  ovrspc2v  6078  oveqrspc2v  6079  rspceov  6095  fovcld  6160  ovmpos  6179  ov2gf  6180  ovi3  6193  caovclg  6209  caovcomg  6212  caovassg  6215  caovcang  6218  caovcan  6221  caovordig  6222  caovordg  6224  caovord  6228  caovdig  6231  caovdirg  6234  caovimo  6250  suppssov1  6265  off  6281  caofid0l  6295  caofid2  6298  caofdig  6302  suppofss1dcl  6466  suppofss2dcl  6467  omv  6690  oeiv  6691  oasuc  6699  oawordriexmid  6705  omsuc  6707  nna0r  6713  nnm0r  6714  nnacl  6715  nnmcl  6716  nnacom  6719  nnaass  6720  nndi  6721  nnmass  6722  nnmsucr  6723  nnmcom  6724  nnaordi  6743  nnaord  6744  nnmordi  6751  nnmord  6752  nnaordex  6763  nnawordex  6764  nnm00  6765  eroveu  6862  ecopovtrn  6868  ecopovtrng  6871  th3qlem2  6874  th3q  6876  ecovcom  6878  ecovicom  6879  ecovass  6880  ecoviass  6881  ecovdi  6882  ecovidi  6883  exmidpw2en  7174  mapfi  7216  acneq  7511  addcanpig  7651  mulcanpig  7652  addcmpblnq  7684  addclnq  7692  mulclnq  7693  recexnq  7707  recmulnqg  7708  ltanqg  7717  ltmnqg  7718  ltexnqq  7725  enq0ref  7750  enq0tr  7751  addcmpblnq0  7760  mulnnnq0  7767  addclnq0  7768  mulclnq0  7769  distrnq0  7776  mulcomnq0  7777  addassnq0  7779  nq02m  7782  prarloclem3  7814  genipv  7826  genpassl  7841  genpassu  7842  addlocpr  7853  distrlem1prl  7899  distrlem1pru  7900  1idprl  7907  1idpru  7908  ltexprlemell  7915  ltexprlemelu  7916  ltexpri  7930  lteupri  7934  ltaprlem  7935  recexprlem1ssl  7950  recexprlem1ssu  7951  recexpr  7955  cauappcvgprlemm  7962  cauappcvgprlemdisj  7968  cauappcvgprlemloc  7969  cauappcvgprlemladdru  7973  cauappcvgprlemladdrl  7974  cauappcvgprlem1  7976  cauappcvgprlemlim  7978  cauappcvgpr  7979  mulcmpblnrlemg  8057  addclsr  8070  mulclsr  8071  ltasrg  8087  negexsr  8089  recexgt0sr  8090  mulgt0sr  8095  mulextsr1  8098  srpospr  8100  caucvgsrlemgt1  8112  map2psrprg  8122  axaddrcl  8182  axmulrcl  8184  axaddcom  8187  axrnegex  8196  axprecex  8197  axcnre  8198  axpre-ltadd  8203  axpre-mulgt0  8204  axpre-mulext  8205  rereceu  8206  recriota  8207  axcaucvglemres  8216  readdcan  8415  cnegexlem1  8450  cnegex  8453  addcan  8455  negeq  8468  subadd  8478  addid0  8648  ine0  8669  rimul  8861  cru  8878  apreim  8879  recexap  8929  mulcanapd  8937  receuap  8945  divmulap  8951  rerecapb  9119  cju  9237  nnaddcl  9259  nnmulcl  9260  nnsub  9278  nnnn0addcl  9528  zaddcllempos  9616  zaddcl  9619  zdiv  9669  deceq1  9716  deceq2  9717  uzaddcl  9921  zq  9961  qreccl  9977  cnref1o  9986  xaddnemnf  10193  xaddnepnf  10194  xaddcom  10197  xnn0xadd0  10203  xnegdi  10204  xaddass  10205  xlt2add  10216  xlesubadd  10219  xleaddadd  10223  fzsuc2  10417  fzrevral  10443  fzshftral  10446  2ffzeq  10479  exfzdc  10590  exbtwnzlemshrink  10612  rebtwn2zlemshrink  10617  modqval  10690  modqmuladd  10732  modqmuladdnn0  10734  frecuzrdgrrn  10774  frec2uzrdg  10775  frecuzrdgrcl  10776  frecuzrdgsuc  10780  frecuzrdgrclt  10781  frecuzrdgg  10782  frecuzrdgsuctlem  10789  frecfzennn  10792  uzsinds  10810  iseqvalcbv  10825  seq3val  10826  seqvalcd  10827  seqovcd  10833  seq3caopr3  10857  seq3caopr2  10859  seqcaopr2g  10860  seq3f1olemp  10881  seqf1og  10887  seq3id  10891  seq3homo  10893  seq3z  10894  seqhomog  10896  seqfeq4g  10897  seq3distr  10898  expp1  10912  expnegap0  10913  expcllem  10916  expcl2lemap  10917  m1expcl2  10927  expap0  10935  mulexp  10944  expadd  10947  expmul  10950  leexp2r  10959  leexp1a  10960  bernneq  11026  expnbnd  11029  modqexp  11032  nn0ltexp2  11075  expcan  11082  apexp1  11084  facdiv  11104  faclbnd3  11109  faclbnd6  11110  bcval  11115  bcpasc  11132  bccl  11133  fz1eqb  11157  omgadd  11170  hashunlem  11172  hashfzo  11191  hashfzp1  11193  hashmap  11196  hashfibclem  11210  hashfibc  11211  iswrdinn0  11233  wrdnval  11259  eqwrd  11269  eqs1  11320  pfxeq  11392  ccatopth  11412  wrd2ind  11419  swrdccatin1  11421  swrdccatin2  11425  pfxccatin12lem2  11427  swrdccat3blem  11435  pfxccatid  11437  swrdccatin1d  11439  swrdccatin2d  11440  s2dmg  11486  shftfvalg  11507  shftfval  11510  cjth  11535  remim  11549  reim0b  11551  cjexp  11582  cnrecnv  11599  cvg1nlemcau  11673  cvg1nlemres  11674  recvguniq  11684  resqrexlemp1rp  11695  resqrexlemfp1  11698  resqrexlemlo  11702  resqrexlemgt0  11709  resqrexlemoverl  11710  resqrexlemglsq  11711  resqrexlemsqa  11713  resqrexlemex  11714  resqrex  11715  absexp  11768  recan  11798  climcn2  11998  subcn2  12000  summodc  12073  fsum3  12077  fsum3cvg3  12086  fsumrev  12133  fisum0diag2  12137  telfsumo  12156  fsumrelem  12161  binomlem  12173  binom  12174  binom1dif  12177  bcxmaslem1  12178  bcxmas  12179  isumshft  12180  divcnv  12187  arisum  12188  trireciplem  12190  expcnvap0  12192  expcnvre  12193  expcnv  12194  explecnv  12195  geosergap  12196  geolim  12201  geolim2  12202  geo2sum  12204  geo2lim  12206  geoisum  12207  geoisumr  12208  geoisum1  12209  geoisum1c  12210  cvgratnnlemsumlt  12218  cvgratz  12222  prodmodc  12268  fprodseq  12273  fprodcl2lem  12295  fprodfac  12305  fprodabs  12306  fprodrev  12309  eftvalcn  12347  efcvgfsum  12357  ege2le3  12361  efcj  12363  efaddlem  12364  efexp  12372  eftlub  12380  efgt1p2  12385  eflegeo  12391  sinval  12392  cosval  12393  demoivreALT  12464  divides  12479  dvdscmul  12508  dvds2ln  12514  dvdstr  12518  odd2np1lem  12562  odd2np1  12563  2tp1odd  12574  opeo  12587  omeo  12588  m1expe  12589  m1expo  12590  m1exp1  12591  divalglemnn  12608  divalglemeunn  12611  divalglemeuneg  12613  divalgmod  12617  ndvdssub  12620  bitsval  12633  bitsfzolem  12644  bitsinv1lem  12651  bitsinv1  12652  gcd0id  12679  bezoutlemnewy  12696  bezoutlema  12699  bezoutlemb  12700  bezoutlemex  12701  bezoutlemaz  12703  bezoutlembz  12704  gcdmultiple  12720  gcdmultiplez  12721  dvdsmulgcd  12725  rplpwr  12727  nn0seqcvgd  12742  dvdslcm  12770  lcmeq0  12772  lcmcl  12773  lcmneg  12775  lcmgcdlem  12778  lcmdvds  12780  lcmid  12781  lcmgcdeq  12784  coprmdvds  12793  mulgcddvds  12795  qredeq  12797  cncongr1  12804  cncongr2  12805  cncongrcoprm  12807  prmind2  12821  isprm6  12848  prmdvdsexp  12849  prmdvdsexpr  12851  sqrt2irr  12863  pw2dvdslemn  12866  pw2dvdseu  12869  oddpwdclemxy  12870  sqpweven  12876  2sqpwodd  12877  sqne2sq  12878  nn0gcdsq  12901  qden1elz  12906  phival  12914  dfphi2  12921  eulerthlemrprm  12930  eulerthlema  12931  prmdiv  12936  prmdiveq  12937  phisum  12942  odzval  12943  odzcllem  12944  odzdvds  12947  reumodprminv  12955  pythagtriplem3  12969  pythagtriplem18  12983  pythagtriplem19  12984  pclem0  12988  pclemub  12989  pclemdc  12990  pcprecl  12991  pcprendvds  12992  pcpremul  12995  pceulem  12996  pceu  12997  pczpre  12999  pcdiv  13004  pcqmul  13005  pcqcl  13008  pcexp  13011  pcxnn0cl  13012  pcxcl  13013  pcge0  13015  pcdvdsb  13022  pcneg  13027  pcabs  13028  pcgcd1  13030  pc2dvds  13032  pc11  13033  pcz  13034  pcprmpw2  13035  pcprmpw  13036  dvdsprmpweq  13037  dvdsprmpweqnn  13038  dvdsprmpweqle  13039  pcaddlem  13041  pcadd  13042  pcfac  13052  oddprmdvds  13056  prmpwdvds  13057  pockthi  13060  infpnlem2  13062  1arithlem1  13065  4sqlemffi  13098  4sqlem12  13104  2expltfac  13141  ballotfilemfval  13150  ballotfilemfc0  13153  ballotfilemfcc  13154  ennnfonelemnn0  13190  ennnfonelemr  13191  f1ovscpbl  13542  imasaddvallemg  13545  ercpbl  13561  mgm1  13600  mgmidmo  13602  mgmlrid  13609  lidrideqd  13611  lidrididd  13612  grpinvalem  13615  grpinva  13616  gsumfzval  13621  gsumval2  13627  isnsgrp  13636  sgrpass  13638  sgrp1  13641  mndinvmod  13675  imasmnd2  13682  mnd1  13685  mnd1id  13686  mhmpropd  13696  mhmlin  13697  insubm  13715  mhmima  13721  gsumwsubmcl  13726  gsumwmhm  13728  grpinvex  13740  grppropd  13747  dfgrp2  13757  grpidd2  13771  grpinvval  13773  grpinvid1  13782  grplrinv  13787  grpidinv2  13788  grpidinv  13789  grplcan  13792  grpidssd  13806  grpinvssd  13807  dfgrp3mlem  13828  dfgrp3m  13829  grplactcnv  13832  grp1  13836  imasgrp2  13844  mhmlem  13848  mulgnn0gsum  13862  mulginvcom  13881  mulgnn0ass  13892  mulgmodid  13895  issubg  13907  issubg2m  13923  issubg4m  13927  isnsg2  13937  nsgbi  13938  isnsg3  13941  elnmz  13942  nmzbi  13943  ghmlin  13982  ghmrn  13991  ghmnsgima  14002  conjghm  14010  conjnmz  14013  gsumfzconst  14075  rngdi  14101  rngdir  14102  srglz  14146  srgisid  14147  srglmhm  14154  ringid  14187  ringinvnz1ne0  14210  ringinvnzdiv  14211  ring1  14220  ringlghm  14222  imasring  14225  dvdsrtr  14263  lringuplu  14358  issubrng  14361  issubrng2  14372  issubrg  14383  issubrg2  14403  rrgeq0i  14426  rrgeq0  14427  unitrrg  14430  domneq0  14435  lmodlema  14457  islmodd  14458  rmodislmodlem  14515  rmodislmod  14516  lssclg  14529  lss1d  14548  rnglidlmcl  14645  quscrng  14698  cnfldexp  14742  gsumfzfsumlemm  14752  cnfldui  14754  expghmap  14772  zrhval  14782  zrhvalg  14783  znunit  14824  txdis1cn  15160  cnmptcom  15180  psmettri2  15210  isxmet2d  15230  xmeteq0  15241  xmettri2  15243  elblps  15272  elbl  15273  blssps  15309  blss  15310  ssblex  15313  blin2  15314  metss2  15380  comet  15381  bdmopn  15386  txmetcnp  15400  blssioo  15435  divcnap  15447  mpomulcn  15448  expcn  15451  cncfval  15454  cncfi  15460  mulc1cncf  15471  cdivcncfap  15486  mulcncf  15490  expcncf  15491  cnopnap  15493  ellimc3apf  15542  cnlimci  15555  limccnpcntop  15557  limccnp2lem  15558  reldvg  15561  eldvap  15564  dvexp  15593  dvexp2  15594  dvrecap  15595  elplyr  15622  elplyd  15623  ply1termlem  15624  plymullem1  15630  plyadd  15633  plymul  15634  plycoeid3  15639  plycolemc  15640  plyco  15641  plycj  15643  dvply1  15647  dvply2g  15648  sin0pilem2  15664  rpcxpmul2  15795  relogbcxpbap  15847  logbgcd1irr  15849  2irrexpq  15858  2irrexpqap  15860  dvdsppwf1o  15874  mpodvdsmulf1o  15875  fsumdvdsmul  15876  sgmppw  15877  1sgmprm  15879  perfect  15886  lgsneg  15914  lgsdilem  15917  lgsdir  15925  lgsdilem2  15926  lgsdi  15927  lgsne0  15928  lgsdirnn0  15937  lgsdinn0  15938  gausslemma2dlem4  15954  lgseisenlem2  15961  lgseisenlem3  15962  lgseisenlem4  15963  lgsquadlem1  15967  lgsquadlem2  15968  lgsquad2lem2  15972  2lgs  15994  2sqlem6  16010  2sqlem8  16013  2sqlem9  16014  2sqlem10  16015  wlkeq  16366  wlkl1loop  16370  uspgr2wlkeq  16377  upgr2wlkdc  16389  clwwlknonmpo  16440  eupth2fi  16491  trilpolemclim  16837  trilpolemcl  16838  trilpolemisumle  16839  trilpolemeq1  16841  trilpolemlt1  16842  trilpo  16844  trirec0  16845  qdiff  16850  redcwlpo  16857  nconstwlpolemgt0  16867  nconstwlpo  16869  neapmkv  16871