Theorem oveq2 5896

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 3791	. . 3 |- ( A = B -> <. C , A >. = <. C , B >. )
2	1	fveq2d 5531	. 2 |- ( A = B -> ( F ` <. C , A >. ) = ( F ` <. C , B >. ) )
3		df-ov 5891	. 2 |- ( C F A ) = ( F ` <. C , A >. )
4		df-ov 5891	. 2 |- ( C F B ) = ( F ` <. C , B >. )
5	2, 3, 4	3eqtr4g 2245	1 |- ( A = B -> ( C F A ) = ( C F B ) )

Syntax hints:   -> wi 4   = wceq 1363   <.cop 3607   ` cfv 5228  (class class class)co 5888

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 710  ax-5 1457  ax-7 1458  ax-gen 1459  ax-ie1 1503  ax-ie2 1504  ax-8 1514  ax-10 1515  ax-11 1516  ax-i12 1517  ax-bndl 1519  ax-4 1520  ax-17 1536  ax-i9 1540  ax-ial 1544  ax-i5r 1545  ax-ext 2169

This theorem depends on definitions:  df-bi 117  df-3an 981  df-tru 1366  df-nf 1471  df-sb 1773  df-clab 2174  df-cleq 2180  df-clel 2183  df-nfc 2318  df-rex 2471  df-v 2751  df-un 3145  df-sn 3610  df-pr 3611  df-op 3613  df-uni 3822  df-br 4016  df-iota 5190  df-fv 5236  df-ov 5891

This theorem is referenced by:  oveq12  5897  oveq2i  5899  oveq2d  5904  ovanraleqv  5912  ovrspc2v  5914  oveqrspc2v  5915  rspceov  5930  fovcld  5993  ovmpos  6012  ov2gf  6013  ovi3  6025  caovclg  6041  caovcomg  6044  caovassg  6047  caovcang  6050  caovcan  6053  caovordig  6054  caovordg  6056  caovord  6060  caovdig  6063  caovdirg  6066  caovimo  6082  suppssov1  6094  off  6109  omv  6470  oeiv  6471  oasuc  6479  oawordriexmid  6485  omsuc  6487  nna0r  6493  nnm0r  6494  nnacl  6495  nnmcl  6496  nnacom  6499  nnaass  6500  nndi  6501  nnmass  6502  nnmsucr  6503  nnmcom  6504  nnaordi  6523  nnaord  6524  nnmordi  6531  nnmord  6532  nnaordex  6543  nnawordex  6544  nnm00  6545  eroveu  6640  ecopovtrn  6646  ecopovtrng  6649  th3qlem2  6652  th3q  6654  ecovcom  6656  ecovicom  6657  ecovass  6658  ecoviass  6659  ecovdi  6660  ecovidi  6661  addcanpig  7347  mulcanpig  7348  addcmpblnq  7380  addclnq  7388  mulclnq  7389  recexnq  7403  recmulnqg  7404  ltanqg  7413  ltmnqg  7414  ltexnqq  7421  enq0ref  7446  enq0tr  7447  addcmpblnq0  7456  mulnnnq0  7463  addclnq0  7464  mulclnq0  7465  distrnq0  7472  mulcomnq0  7473  addassnq0  7475  nq02m  7478  prarloclem3  7510  genipv  7522  genpassl  7537  genpassu  7538  addlocpr  7549  distrlem1prl  7595  distrlem1pru  7596  1idprl  7603  1idpru  7604  ltexprlemell  7611  ltexprlemelu  7612  ltexpri  7626  lteupri  7630  ltaprlem  7631  recexprlem1ssl  7646  recexprlem1ssu  7647  recexpr  7651  cauappcvgprlemm  7658  cauappcvgprlemdisj  7664  cauappcvgprlemloc  7665  cauappcvgprlemladdru  7669  cauappcvgprlemladdrl  7670  cauappcvgprlem1  7672  cauappcvgprlemlim  7674  cauappcvgpr  7675  mulcmpblnrlemg  7753  addclsr  7766  mulclsr  7767  ltasrg  7783  negexsr  7785  recexgt0sr  7786  mulgt0sr  7791  mulextsr1  7794  srpospr  7796  caucvgsrlemgt1  7808  map2psrprg  7818  axaddrcl  7878  axmulrcl  7880  axaddcom  7883  axrnegex  7892  axprecex  7893  axcnre  7894  axpre-ltadd  7899  axpre-mulgt0  7900  axpre-mulext  7901  rereceu  7902  recriota  7903  axcaucvglemres  7912  readdcan  8111  cnegexlem1  8146  cnegex  8149  addcan  8151  negeq  8164  subadd  8174  addid0  8344  ine0  8365  rimul  8556  cru  8573  apreim  8574  recexap  8624  mulcanapd  8632  receuap  8640  divmulap  8646  rerecapb  8814  cju  8932  nnaddcl  8953  nnmulcl  8954  nnsub  8972  nnnn0addcl  9220  zaddcllempos  9304  zaddcl  9307  zdiv  9355  deceq1  9402  deceq2  9403  uzaddcl  9600  zq  9640  qreccl  9656  cnref1o  9664  xaddnemnf  9871  xaddnepnf  9872  xaddcom  9875  xnn0xadd0  9881  xnegdi  9882  xaddass  9883  xlt2add  9894  xlesubadd  9897  xleaddadd  9901  fzsuc2  10093  fzrevral  10119  fzshftral  10122  2ffzeq  10155  exfzdc  10254  exbtwnzlemshrink  10263  rebtwn2zlemshrink  10268  modqval  10338  modqmuladd  10380  modqmuladdnn0  10382  frecuzrdgrrn  10422  frec2uzrdg  10423  frecuzrdgrcl  10424  frecuzrdgsuc  10428  frecuzrdgrclt  10429  frecuzrdgg  10430  frecuzrdgsuctlem  10437  frecfzennn  10440  uzsinds  10456  iseqvalcbv  10471  seq3val  10472  seqvalcd  10473  seqovcd  10477  seq3caopr3  10495  seq3caopr2  10496  seq3f1olemp  10516  seq3id  10522  seq3homo  10524  seq3z  10525  seq3distr  10527  expp1  10541  expnegap0  10542  expcllem  10545  expcl2lemap  10546  m1expcl2  10556  expap0  10564  mulexp  10573  expadd  10576  expmul  10579  leexp2r  10588  leexp1a  10589  bernneq  10655  expnbnd  10658  modqexp  10661  nn0ltexp2  10703  expcan  10710  apexp1  10712  facdiv  10732  faclbnd3  10737  faclbnd6  10738  bcval  10743  bcpasc  10760  bccl  10761  fz1eqb  10784  omgadd  10796  hashunlem  10798  hashfzo  10816  hashfzp1  10818  shftfvalg  10841  shftfval  10844  cjth  10869  remim  10883  reim0b  10885  cjexp  10916  cnrecnv  10933  cvg1nlemcau  11007  cvg1nlemres  11008  recvguniq  11018  resqrexlemp1rp  11029  resqrexlemfp1  11032  resqrexlemlo  11036  resqrexlemgt0  11043  resqrexlemoverl  11044  resqrexlemglsq  11045  resqrexlemsqa  11047  resqrexlemex  11048  resqrex  11049  absexp  11102  recan  11132  climcn2  11331  subcn2  11333  summodc  11405  fsum3  11409  fsum3cvg3  11418  fsumrev  11465  fisum0diag2  11469  telfsumo  11488  fsumrelem  11493  binomlem  11505  binom  11506  binom1dif  11509  bcxmaslem1  11510  bcxmas  11511  isumshft  11512  divcnv  11519  arisum  11520  trireciplem  11522  expcnvap0  11524  expcnvre  11525  expcnv  11526  explecnv  11527  geosergap  11528  geolim  11533  geolim2  11534  geo2sum  11536  geo2lim  11538  geoisum  11539  geoisumr  11540  geoisum1  11541  geoisum1c  11542  cvgratnnlemsumlt  11550  cvgratz  11554  prodmodc  11600  fprodseq  11605  fprodcl2lem  11627  fprodfac  11637  fprodabs  11638  fprodrev  11641  eftvalcn  11679  efcvgfsum  11689  ege2le3  11693  efcj  11695  efaddlem  11696  efexp  11704  eftlub  11712  efgt1p2  11717  eflegeo  11723  sinval  11724  cosval  11725  demoivreALT  11795  divides  11810  dvdscmul  11839  dvds2ln  11845  dvdstr  11849  odd2np1lem  11891  odd2np1  11892  2tp1odd  11903  opeo  11916  omeo  11917  m1expe  11918  m1expo  11919  m1exp1  11920  divalglemnn  11937  divalglemeunn  11940  divalglemeuneg  11942  divalgmod  11946  ndvdssub  11949  gcd0id  11994  bezoutlemnewy  12011  bezoutlema  12014  bezoutlemb  12015  bezoutlemex  12016  bezoutlemaz  12018  bezoutlembz  12019  gcdmultiple  12035  gcdmultiplez  12036  dvdsmulgcd  12040  rplpwr  12042  nn0seqcvgd  12055  dvdslcm  12083  lcmeq0  12085  lcmcl  12086  lcmneg  12088  lcmgcdlem  12091  lcmdvds  12093  lcmid  12094  lcmgcdeq  12097  coprmdvds  12106  mulgcddvds  12108  qredeq  12110  cncongr1  12117  cncongr2  12118  cncongrcoprm  12120  prmind2  12134  isprm6  12161  prmdvdsexp  12162  prmdvdsexpr  12164  sqrt2irr  12176  pw2dvdslemn  12179  pw2dvdseu  12182  oddpwdclemxy  12183  sqpweven  12189  2sqpwodd  12190  sqne2sq  12191  nn0gcdsq  12214  qden1elz  12219  phival  12227  dfphi2  12234  eulerthlemrprm  12243  eulerthlema  12244  prmdiv  12249  prmdiveq  12250  phisum  12254  odzval  12255  odzcllem  12256  odzdvds  12259  reumodprminv  12267  pythagtriplem3  12281  pythagtriplem18  12295  pythagtriplem19  12296  pclem0  12300  pclemub  12301  pclemdc  12302  pcprecl  12303  pcprendvds  12304  pcpremul  12307  pceulem  12308  pceu  12309  pczpre  12311  pcdiv  12316  pcqmul  12317  pcqcl  12320  pcexp  12323  pcxnn0cl  12324  pcxcl  12325  pcge0  12326  pcdvdsb  12333  pcneg  12338  pcabs  12339  pcgcd1  12341  pc2dvds  12343  pc11  12344  pcz  12345  pcprmpw2  12346  pcprmpw  12347  dvdsprmpweq  12348  dvdsprmpweqnn  12349  dvdsprmpweqle  12350  pcaddlem  12352  pcadd  12353  pcfac  12362  oddprmdvds  12366  prmpwdvds  12367  pockthi  12370  infpnlem2  12372  1arithlem1  12375  ennnfonelemnn0  12437  ennnfonelemr  12438  f1ovscpbl  12751  imasaddvallemg  12754  ercpbl  12769  mgm1  12808  mgmidmo  12810  mgmlrid  12817  lidrideqd  12819  lidrididd  12820  grpinvalem  12823  grpinva  12824  isnsgrp  12831  sgrpass  12833  sgrp1  12836  mndinvmod  12868  mnd1  12869  mnd1id  12870  mhmpropd  12879  mhmlin  12880  insubm  12894  mhmima  12897  grpinvex  12909  grppropd  12915  dfgrp2  12924  grpidd2  12938  grpinvval  12940  grpinvid1  12949  grplrinv  12954  grpidinv2  12955  grpidinv  12956  grplcan  12959  grpidssd  12973  grpinvssd  12974  dfgrp3mlem  12995  dfgrp3m  12996  grplactcnv  12999  grp1  13003  imasgrp2  13005  mhmlem  13009  mulginvcom  13040  mulgnn0ass  13051  mulgmodid  13054  issubg  13065  issubg2m  13081  issubg4m  13085  isnsg2  13095  nsgbi  13096  isnsg3  13099  elnmz  13100  nmzbi  13101  rngdi  13192  rngdir  13193  srglz  13237  srgisid  13238  srglmhm  13245  ringid  13278  ringinvnz1ne0  13299  ringinvnzdiv  13300  ring1  13309  imasring  13312  dvdsrtr  13349  lringuplu  13416  issubrng  13419  issubrng2  13430  issubrg  13441  issubrg2  13461  lmodlema  13481  islmodd  13482  rmodislmodlem  13539  rmodislmod  13540  lssclg  13553  lss1d  13572  rnglidlmcl  13669  quscrng  13720  cnfldexp  13753  txdis1cn  14074  cnmptcom  14094  psmettri2  14124  isxmet2d  14144  xmeteq0  14155  xmettri2  14157  elblps  14186  elbl  14187  blssps  14223  blss  14224  ssblex  14227  blin2  14228  metss2  14294  comet  14295  bdmopn  14300  txmetcnp  14314  blssioo  14341  divcnap  14351  cncfval  14355  cncfi  14361  mulc1cncf  14372  cdivcncfap  14383  mulcncf  14387  expcncf  14388  cnopnap  14390  ellimc3apf  14425  cnlimci  14438  limccnpcntop  14440  limccnp2lem  14441  reldvg  14444  eldvap  14447  dvexp  14471  dvexp2  14472  dvrecap  14473  sin0pilem2  14499  relogbcxpbap  14679  logbgcd1irr  14681  2irrexpq  14690  2irrexpqap  14692  lgsneg  14721  lgsdilem  14724  lgsdir  14732  lgsdilem2  14733  lgsdi  14734  lgsne0  14735  lgsdirnn0  14744  lgsdinn0  14745  lgseisenlem2  14747  2sqlem6  14763  2sqlem8  14766  2sqlem9  14767  2sqlem10  14768  trilpolemclim  15081  trilpolemcl  15082  trilpolemisumle  15083  trilpolemeq1  15085  trilpolemlt1  15086  trilpo  15088  trirec0  15089  redcwlpo  15100  nconstwlpolemgt0  15109  nconstwlpo  15111  neapmkv  15113