Theorem oveq2 5883

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 3780	. . 3 |- ( A = B -> <. C , A >. = <. C , B >. )
2	1	fveq2d 5520	. 2 |- ( A = B -> ( F ` <. C , A >. ) = ( F ` <. C , B >. ) )
3		df-ov 5878	. 2 |- ( C F A ) = ( F ` <. C , A >. )
4		df-ov 5878	. 2 |- ( C F B ) = ( F ` <. C , B >. )
5	2, 3, 4	3eqtr4g 2235	1 |- ( A = B -> ( C F A ) = ( C F B ) )

Syntax hints:   -> wi 4   = wceq 1353   <.cop 3596   ` cfv 5217  (class class class)co 5875

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 709  ax-5 1447  ax-7 1448  ax-gen 1449  ax-ie1 1493  ax-ie2 1494  ax-8 1504  ax-10 1505  ax-11 1506  ax-i12 1507  ax-bndl 1509  ax-4 1510  ax-17 1526  ax-i9 1530  ax-ial 1534  ax-i5r 1535  ax-ext 2159

This theorem depends on definitions:  df-bi 117  df-3an 980  df-tru 1356  df-nf 1461  df-sb 1763  df-clab 2164  df-cleq 2170  df-clel 2173  df-nfc 2308  df-rex 2461  df-v 2740  df-un 3134  df-sn 3599  df-pr 3600  df-op 3602  df-uni 3811  df-br 4005  df-iota 5179  df-fv 5225  df-ov 5878

This theorem is referenced by:  oveq12  5884  oveq2i  5886  oveq2d  5891  ovanraleqv  5899  ovrspc2v  5901  oveqrspc2v  5902  rspceov  5917  fovcl  5980  ovmpos  5998  ov2gf  5999  ovi3  6011  caovclg  6027  caovcomg  6030  caovassg  6033  caovcang  6036  caovcan  6039  caovordig  6040  caovordg  6042  caovord  6046  caovdig  6049  caovdirg  6052  caovimo  6068  suppssov1  6080  off  6095  omv  6456  oeiv  6457  oasuc  6465  oawordriexmid  6471  omsuc  6473  nna0r  6479  nnm0r  6480  nnacl  6481  nnmcl  6482  nnacom  6485  nnaass  6486  nndi  6487  nnmass  6488  nnmsucr  6489  nnmcom  6490  nnaordi  6509  nnaord  6510  nnmordi  6517  nnmord  6518  nnaordex  6529  nnawordex  6530  nnm00  6531  eroveu  6626  ecopovtrn  6632  ecopovtrng  6635  th3qlem2  6638  th3q  6640  ecovcom  6642  ecovicom  6643  ecovass  6644  ecoviass  6645  ecovdi  6646  ecovidi  6647  addcanpig  7333  mulcanpig  7334  addcmpblnq  7366  addclnq  7374  mulclnq  7375  recexnq  7389  recmulnqg  7390  ltanqg  7399  ltmnqg  7400  ltexnqq  7407  enq0ref  7432  enq0tr  7433  addcmpblnq0  7442  mulnnnq0  7449  addclnq0  7450  mulclnq0  7451  distrnq0  7458  mulcomnq0  7459  addassnq0  7461  nq02m  7464  prarloclem3  7496  genipv  7508  genpassl  7523  genpassu  7524  addlocpr  7535  distrlem1prl  7581  distrlem1pru  7582  1idprl  7589  1idpru  7590  ltexprlemell  7597  ltexprlemelu  7598  ltexpri  7612  lteupri  7616  ltaprlem  7617  recexprlem1ssl  7632  recexprlem1ssu  7633  recexpr  7637  cauappcvgprlemm  7644  cauappcvgprlemdisj  7650  cauappcvgprlemloc  7651  cauappcvgprlemladdru  7655  cauappcvgprlemladdrl  7656  cauappcvgprlem1  7658  cauappcvgprlemlim  7660  cauappcvgpr  7661  mulcmpblnrlemg  7739  addclsr  7752  mulclsr  7753  ltasrg  7769  negexsr  7771  recexgt0sr  7772  mulgt0sr  7777  mulextsr1  7780  srpospr  7782  caucvgsrlemgt1  7794  map2psrprg  7804  axaddrcl  7864  axmulrcl  7866  axaddcom  7869  axrnegex  7878  axprecex  7879  axcnre  7880  axpre-ltadd  7885  axpre-mulgt0  7886  axpre-mulext  7887  rereceu  7888  recriota  7889  axcaucvglemres  7898  readdcan  8097  cnegexlem1  8132  cnegex  8135  addcan  8137  negeq  8150  subadd  8160  addid0  8330  ine0  8351  rimul  8542  cru  8559  apreim  8560  recexap  8610  mulcanapd  8618  receuap  8626  divmulap  8632  rerecapb  8800  cju  8918  nnaddcl  8939  nnmulcl  8940  nnsub  8958  nnnn0addcl  9206  zaddcllempos  9290  zaddcl  9293  zdiv  9341  deceq1  9388  deceq2  9389  uzaddcl  9586  zq  9626  qreccl  9642  cnref1o  9650  xaddnemnf  9857  xaddnepnf  9858  xaddcom  9861  xnn0xadd0  9867  xnegdi  9868  xaddass  9869  xlt2add  9880  xlesubadd  9883  xleaddadd  9887  fzsuc2  10079  fzrevral  10105  fzshftral  10108  2ffzeq  10141  exfzdc  10240  exbtwnzlemshrink  10249  rebtwn2zlemshrink  10254  modqval  10324  modqmuladd  10366  modqmuladdnn0  10368  frecuzrdgrrn  10408  frec2uzrdg  10409  frecuzrdgrcl  10410  frecuzrdgsuc  10414  frecuzrdgrclt  10415  frecuzrdgg  10416  frecuzrdgsuctlem  10423  frecfzennn  10426  uzsinds  10442  iseqvalcbv  10457  seq3val  10458  seqvalcd  10459  seqovcd  10463  seq3caopr3  10481  seq3caopr2  10482  seq3f1olemp  10502  seq3id  10508  seq3homo  10510  seq3z  10511  seq3distr  10513  expp1  10527  expnegap0  10528  expcllem  10531  expcl2lemap  10532  m1expcl2  10542  expap0  10550  mulexp  10559  expadd  10562  expmul  10565  leexp2r  10574  leexp1a  10575  bernneq  10641  expnbnd  10644  modqexp  10647  nn0ltexp2  10689  expcan  10696  apexp1  10698  facdiv  10718  faclbnd3  10723  faclbnd6  10724  bcval  10729  bcpasc  10746  bccl  10747  fz1eqb  10770  omgadd  10782  hashunlem  10784  hashfzo  10802  hashfzp1  10804  shftfvalg  10827  shftfval  10830  cjth  10855  remim  10869  reim0b  10871  cjexp  10902  cnrecnv  10919  cvg1nlemcau  10993  cvg1nlemres  10994  recvguniq  11004  resqrexlemp1rp  11015  resqrexlemfp1  11018  resqrexlemlo  11022  resqrexlemgt0  11029  resqrexlemoverl  11030  resqrexlemglsq  11031  resqrexlemsqa  11033  resqrexlemex  11034  resqrex  11035  absexp  11088  recan  11118  climcn2  11317  subcn2  11319  summodc  11391  fsum3  11395  fsum3cvg3  11404  fsumrev  11451  fisum0diag2  11455  telfsumo  11474  fsumrelem  11479  binomlem  11491  binom  11492  binom1dif  11495  bcxmaslem1  11496  bcxmas  11497  isumshft  11498  divcnv  11505  arisum  11506  trireciplem  11508  expcnvap0  11510  expcnvre  11511  expcnv  11512  explecnv  11513  geosergap  11514  geolim  11519  geolim2  11520  geo2sum  11522  geo2lim  11524  geoisum  11525  geoisumr  11526  geoisum1  11527  geoisum1c  11528  cvgratnnlemsumlt  11536  cvgratz  11540  prodmodc  11586  fprodseq  11591  fprodcl2lem  11613  fprodfac  11623  fprodabs  11624  fprodrev  11627  eftvalcn  11665  efcvgfsum  11675  ege2le3  11679  efcj  11681  efaddlem  11682  efexp  11690  eftlub  11698  efgt1p2  11703  eflegeo  11709  sinval  11710  cosval  11711  demoivreALT  11781  divides  11796  dvdscmul  11825  dvds2ln  11831  dvdstr  11835  odd2np1lem  11877  odd2np1  11878  2tp1odd  11889  opeo  11902  omeo  11903  m1expe  11904  m1expo  11905  m1exp1  11906  divalglemnn  11923  divalglemeunn  11926  divalglemeuneg  11928  divalgmod  11932  ndvdssub  11935  gcd0id  11980  bezoutlemnewy  11997  bezoutlema  12000  bezoutlemb  12001  bezoutlemex  12002  bezoutlemaz  12004  bezoutlembz  12005  gcdmultiple  12021  gcdmultiplez  12022  dvdsmulgcd  12026  rplpwr  12028  nn0seqcvgd  12041  dvdslcm  12069  lcmeq0  12071  lcmcl  12072  lcmneg  12074  lcmgcdlem  12077  lcmdvds  12079  lcmid  12080  lcmgcdeq  12083  coprmdvds  12092  mulgcddvds  12094  qredeq  12096  cncongr1  12103  cncongr2  12104  cncongrcoprm  12106  prmind2  12120  isprm6  12147  prmdvdsexp  12148  prmdvdsexpr  12150  sqrt2irr  12162  pw2dvdslemn  12165  pw2dvdseu  12168  oddpwdclemxy  12169  sqpweven  12175  2sqpwodd  12176  sqne2sq  12177  nn0gcdsq  12200  qden1elz  12205  phival  12213  dfphi2  12220  eulerthlemrprm  12229  eulerthlema  12230  prmdiv  12235  prmdiveq  12236  phisum  12240  odzval  12241  odzcllem  12242  odzdvds  12245  reumodprminv  12253  pythagtriplem3  12267  pythagtriplem18  12281  pythagtriplem19  12282  pclem0  12286  pclemub  12287  pclemdc  12288  pcprecl  12289  pcprendvds  12290  pcpremul  12293  pceulem  12294  pceu  12295  pczpre  12297  pcdiv  12302  pcqmul  12303  pcqcl  12306  pcexp  12309  pcxnn0cl  12310  pcxcl  12311  pcge0  12312  pcdvdsb  12319  pcneg  12324  pcabs  12325  pcgcd1  12327  pc2dvds  12329  pc11  12330  pcz  12331  pcprmpw2  12332  pcprmpw  12333  dvdsprmpweq  12334  dvdsprmpweqnn  12335  dvdsprmpweqle  12336  pcaddlem  12338  pcadd  12339  pcfac  12348  oddprmdvds  12352  prmpwdvds  12353  pockthi  12356  infpnlem2  12358  1arithlem1  12361  ennnfonelemnn0  12423  ennnfonelemr  12424  f1ovscpbl  12733  imasaddvallemg  12736  ercpbl  12750  mgm1  12789  mgmidmo  12791  mgmlrid  12798  lidrideqd  12800  lidrididd  12801  grprinvlem  12804  grprinvd  12805  isnsgrp  12812  sgrpass  12814  sgrp1  12816  mndinvmod  12846  mnd1  12847  mnd1id  12848  mhmpropd  12857  mhmlin  12858  insubm  12872  mhmima  12875  grpinvex  12887  grppropd  12893  dfgrp2  12902  grpidd2  12914  grpinvval  12916  grpinvid1  12924  grplrinv  12927  grpidinv2  12928  grpidinv  12929  grplcan  12932  grpidssd  12946  grpinvssd  12947  dfgrp3mlem  12968  dfgrp3m  12969  grplactcnv  12972  grp1  12976  mhmlem  12978  mulginvcom  13008  mulgnn0ass  13019  mulgmodid  13022  issubg  13033  issubg2m  13049  issubg4m  13053  isnsg2  13063  nsgbi  13064  isnsg3  13067  elnmz  13068  nmzbi  13069  srglz  13168  srgisid  13169  srglmhm  13176  ringid  13209  ringinvnz1ne0  13226  ringinvnzdiv  13227  ring1  13236  dvdsrtr  13270  lringuplu  13337  issubrg  13342  issubrg2  13362  lmodlema  13382  islmodd  13383  rmodislmodlem  13440  rmodislmod  13441  cnfldexp  13474  txdis1cn  13781  cnmptcom  13801  psmettri2  13831  isxmet2d  13851  xmeteq0  13862  xmettri2  13864  elblps  13893  elbl  13894  blssps  13930  blss  13931  ssblex  13934  blin2  13935  metss2  14001  comet  14002  bdmopn  14007  txmetcnp  14021  blssioo  14048  divcnap  14058  cncfval  14062  cncfi  14068  mulc1cncf  14079  cdivcncfap  14090  mulcncf  14094  expcncf  14095  cnopnap  14097  ellimc3apf  14132  cnlimci  14145  limccnpcntop  14147  limccnp2lem  14148  reldvg  14151  eldvap  14154  dvexp  14178  dvexp2  14179  dvrecap  14180  sin0pilem2  14206  relogbcxpbap  14386  logbgcd1irr  14388  2irrexpq  14397  2irrexpqap  14399  lgsneg  14428  lgsdilem  14431  lgsdir  14439  lgsdilem2  14440  lgsdi  14441  lgsne0  14442  lgsdirnn0  14451  lgsdinn0  14452  lgseisenlem2  14454  2sqlem6  14470  2sqlem8  14473  2sqlem9  14474  2sqlem10  14475  trilpolemclim  14787  trilpolemcl  14788  trilpolemisumle  14789  trilpolemeq1  14791  trilpolemlt1  14792  trilpo  14794  trirec0  14795  redcwlpo  14806  nconstwlpolemgt0  14814  nconstwlpo  14816  neapmkv  14818