Theorem oveq2 5930

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 3809	. . 3 |- ( A = B -> <. C , A >. = <. C , B >. )
2	1	fveq2d 5562	. 2 |- ( A = B -> ( F ` <. C , A >. ) = ( F ` <. C , B >. ) )
3		df-ov 5925	. 2 |- ( C F A ) = ( F ` <. C , A >. )
4		df-ov 5925	. 2 |- ( C F B ) = ( F ` <. C , B >. )
5	2, 3, 4	3eqtr4g 2254	1 |- ( A = B -> ( C F A ) = ( C F B ) )

Syntax hints:   -> wi 4   = wceq 1364   <.cop 3625   ` cfv 5258  (class class class)co 5922

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 1461  ax-7 1462  ax-gen 1463  ax-ie1 1507  ax-ie2 1508  ax-8 1518  ax-10 1519  ax-11 1520  ax-i12 1521  ax-bndl 1523  ax-4 1524  ax-17 1540  ax-i9 1544  ax-ial 1548  ax-i5r 1549  ax-ext 2178

This theorem depends on definitions:  df-bi 117  df-3an 982  df-tru 1367  df-nf 1475  df-sb 1777  df-clab 2183  df-cleq 2189  df-clel 2192  df-nfc 2328  df-rex 2481  df-v 2765  df-un 3161  df-sn 3628  df-pr 3629  df-op 3631  df-uni 3840  df-br 4034  df-iota 5219  df-fv 5266  df-ov 5925

This theorem is referenced by:  oveq12  5931  oveq2i  5933  oveq2d  5938  ovanraleqv  5946  ovrspc2v  5948  oveqrspc2v  5949  rspceov  5964  fovcld  6027  ovmpos  6046  ov2gf  6047  ovi3  6060  caovclg  6076  caovcomg  6079  caovassg  6082  caovcang  6085  caovcan  6088  caovordig  6089  caovordg  6091  caovord  6095  caovdig  6098  caovdirg  6101  caovimo  6117  suppssov1  6132  off  6148  caofdig  6164  omv  6513  oeiv  6514  oasuc  6522  oawordriexmid  6528  omsuc  6530  nna0r  6536  nnm0r  6537  nnacl  6538  nnmcl  6539  nnacom  6542  nnaass  6543  nndi  6544  nnmass  6545  nnmsucr  6546  nnmcom  6547  nnaordi  6566  nnaord  6567  nnmordi  6574  nnmord  6575  nnaordex  6586  nnawordex  6587  nnm00  6588  eroveu  6685  ecopovtrn  6691  ecopovtrng  6694  th3qlem2  6697  th3q  6699  ecovcom  6701  ecovicom  6702  ecovass  6703  ecoviass  6704  ecovdi  6705  ecovidi  6706  exmidpw2en  6973  addcanpig  7401  mulcanpig  7402  addcmpblnq  7434  addclnq  7442  mulclnq  7443  recexnq  7457  recmulnqg  7458  ltanqg  7467  ltmnqg  7468  ltexnqq  7475  enq0ref  7500  enq0tr  7501  addcmpblnq0  7510  mulnnnq0  7517  addclnq0  7518  mulclnq0  7519  distrnq0  7526  mulcomnq0  7527  addassnq0  7529  nq02m  7532  prarloclem3  7564  genipv  7576  genpassl  7591  genpassu  7592  addlocpr  7603  distrlem1prl  7649  distrlem1pru  7650  1idprl  7657  1idpru  7658  ltexprlemell  7665  ltexprlemelu  7666  ltexpri  7680  lteupri  7684  ltaprlem  7685  recexprlem1ssl  7700  recexprlem1ssu  7701  recexpr  7705  cauappcvgprlemm  7712  cauappcvgprlemdisj  7718  cauappcvgprlemloc  7719  cauappcvgprlemladdru  7723  cauappcvgprlemladdrl  7724  cauappcvgprlem1  7726  cauappcvgprlemlim  7728  cauappcvgpr  7729  mulcmpblnrlemg  7807  addclsr  7820  mulclsr  7821  ltasrg  7837  negexsr  7839  recexgt0sr  7840  mulgt0sr  7845  mulextsr1  7848  srpospr  7850  caucvgsrlemgt1  7862  map2psrprg  7872  axaddrcl  7932  axmulrcl  7934  axaddcom  7937  axrnegex  7946  axprecex  7947  axcnre  7948  axpre-ltadd  7953  axpre-mulgt0  7954  axpre-mulext  7955  rereceu  7956  recriota  7957  axcaucvglemres  7966  readdcan  8166  cnegexlem1  8201  cnegex  8204  addcan  8206  negeq  8219  subadd  8229  addid0  8399  ine0  8420  rimul  8612  cru  8629  apreim  8630  recexap  8680  mulcanapd  8688  receuap  8696  divmulap  8702  rerecapb  8870  cju  8988  nnaddcl  9010  nnmulcl  9011  nnsub  9029  nnnn0addcl  9279  zaddcllempos  9363  zaddcl  9366  zdiv  9414  deceq1  9461  deceq2  9462  uzaddcl  9660  zq  9700  qreccl  9716  cnref1o  9725  xaddnemnf  9932  xaddnepnf  9933  xaddcom  9936  xnn0xadd0  9942  xnegdi  9943  xaddass  9944  xlt2add  9955  xlesubadd  9958  xleaddadd  9962  fzsuc2  10154  fzrevral  10180  fzshftral  10183  2ffzeq  10216  exfzdc  10316  exbtwnzlemshrink  10338  rebtwn2zlemshrink  10343  modqval  10416  modqmuladd  10458  modqmuladdnn0  10460  frecuzrdgrrn  10500  frec2uzrdg  10501  frecuzrdgrcl  10502  frecuzrdgsuc  10506  frecuzrdgrclt  10507  frecuzrdgg  10508  frecuzrdgsuctlem  10515  frecfzennn  10518  uzsinds  10536  iseqvalcbv  10551  seq3val  10552  seqvalcd  10553  seqovcd  10559  seq3caopr3  10583  seq3caopr2  10585  seqcaopr2g  10586  seq3f1olemp  10607  seqf1og  10613  seq3id  10617  seq3homo  10619  seq3z  10620  seqhomog  10622  seqfeq4g  10623  seq3distr  10624  expp1  10638  expnegap0  10639  expcllem  10642  expcl2lemap  10643  m1expcl2  10653  expap0  10661  mulexp  10670  expadd  10673  expmul  10676  leexp2r  10685  leexp1a  10686  bernneq  10752  expnbnd  10755  modqexp  10758  nn0ltexp2  10801  expcan  10808  apexp1  10810  facdiv  10830  faclbnd3  10835  faclbnd6  10836  bcval  10841  bcpasc  10858  bccl  10859  fz1eqb  10882  omgadd  10894  hashunlem  10896  hashfzo  10914  hashfzp1  10916  iswrdinn0  10940  wrdnval  10965  eqwrd  10975  shftfvalg  10983  shftfval  10986  cjth  11011  remim  11025  reim0b  11027  cjexp  11058  cnrecnv  11075  cvg1nlemcau  11149  cvg1nlemres  11150  recvguniq  11160  resqrexlemp1rp  11171  resqrexlemfp1  11174  resqrexlemlo  11178  resqrexlemgt0  11185  resqrexlemoverl  11186  resqrexlemglsq  11187  resqrexlemsqa  11189  resqrexlemex  11190  resqrex  11191  absexp  11244  recan  11274  climcn2  11474  subcn2  11476  summodc  11548  fsum3  11552  fsum3cvg3  11561  fsumrev  11608  fisum0diag2  11612  telfsumo  11631  fsumrelem  11636  binomlem  11648  binom  11649  binom1dif  11652  bcxmaslem1  11653  bcxmas  11654  isumshft  11655  divcnv  11662  arisum  11663  trireciplem  11665  expcnvap0  11667  expcnvre  11668  expcnv  11669  explecnv  11670  geosergap  11671  geolim  11676  geolim2  11677  geo2sum  11679  geo2lim  11681  geoisum  11682  geoisumr  11683  geoisum1  11684  geoisum1c  11685  cvgratnnlemsumlt  11693  cvgratz  11697  prodmodc  11743  fprodseq  11748  fprodcl2lem  11770  fprodfac  11780  fprodabs  11781  fprodrev  11784  eftvalcn  11822  efcvgfsum  11832  ege2le3  11836  efcj  11838  efaddlem  11839  efexp  11847  eftlub  11855  efgt1p2  11860  eflegeo  11866  sinval  11867  cosval  11868  demoivreALT  11939  divides  11954  dvdscmul  11983  dvds2ln  11989  dvdstr  11993  odd2np1lem  12037  odd2np1  12038  2tp1odd  12049  opeo  12062  omeo  12063  m1expe  12064  m1expo  12065  m1exp1  12066  divalglemnn  12083  divalglemeunn  12086  divalglemeuneg  12088  divalgmod  12092  ndvdssub  12095  bitsval  12108  bitsfzolem  12118  gcd0id  12146  bezoutlemnewy  12163  bezoutlema  12166  bezoutlemb  12167  bezoutlemex  12168  bezoutlemaz  12170  bezoutlembz  12171  gcdmultiple  12187  gcdmultiplez  12188  dvdsmulgcd  12192  rplpwr  12194  nn0seqcvgd  12209  dvdslcm  12237  lcmeq0  12239  lcmcl  12240  lcmneg  12242  lcmgcdlem  12245  lcmdvds  12247  lcmid  12248  lcmgcdeq  12251  coprmdvds  12260  mulgcddvds  12262  qredeq  12264  cncongr1  12271  cncongr2  12272  cncongrcoprm  12274  prmind2  12288  isprm6  12315  prmdvdsexp  12316  prmdvdsexpr  12318  sqrt2irr  12330  pw2dvdslemn  12333  pw2dvdseu  12336  oddpwdclemxy  12337  sqpweven  12343  2sqpwodd  12344  sqne2sq  12345  nn0gcdsq  12368  qden1elz  12373  phival  12381  dfphi2  12388  eulerthlemrprm  12397  eulerthlema  12398  prmdiv  12403  prmdiveq  12404  phisum  12409  odzval  12410  odzcllem  12411  odzdvds  12414  reumodprminv  12422  pythagtriplem3  12436  pythagtriplem18  12450  pythagtriplem19  12451  pclem0  12455  pclemub  12456  pclemdc  12457  pcprecl  12458  pcprendvds  12459  pcpremul  12462  pceulem  12463  pceu  12464  pczpre  12466  pcdiv  12471  pcqmul  12472  pcqcl  12475  pcexp  12478  pcxnn0cl  12479  pcxcl  12480  pcge0  12482  pcdvdsb  12489  pcneg  12494  pcabs  12495  pcgcd1  12497  pc2dvds  12499  pc11  12500  pcz  12501  pcprmpw2  12502  pcprmpw  12503  dvdsprmpweq  12504  dvdsprmpweqnn  12505  dvdsprmpweqle  12506  pcaddlem  12508  pcadd  12509  pcfac  12519  oddprmdvds  12523  prmpwdvds  12524  pockthi  12527  infpnlem2  12529  1arithlem1  12532  4sqlemffi  12565  4sqlem12  12571  2expltfac  12608  ennnfonelemnn0  12639  ennnfonelemr  12640  f1ovscpbl  12955  imasaddvallemg  12958  ercpbl  12974  mgm1  13013  mgmidmo  13015  mgmlrid  13022  lidrideqd  13024  lidrididd  13025  grpinvalem  13028  grpinva  13029  gsumfzval  13034  gsumval2  13040  isnsgrp  13049  sgrpass  13051  sgrp1  13054  mndinvmod  13086  mnd1  13087  mnd1id  13088  mhmpropd  13098  mhmlin  13099  insubm  13117  mhmima  13123  gsumwsubmcl  13128  gsumwmhm  13130  grpinvex  13142  grppropd  13149  dfgrp2  13159  grpidd2  13173  grpinvval  13175  grpinvid1  13184  grplrinv  13189  grpidinv2  13190  grpidinv  13191  grplcan  13194  grpidssd  13208  grpinvssd  13209  dfgrp3mlem  13230  dfgrp3m  13231  grplactcnv  13234  grp1  13238  imasgrp2  13240  mhmlem  13244  mulgnn0gsum  13258  mulginvcom  13277  mulgnn0ass  13288  mulgmodid  13291  issubg  13303  issubg2m  13319  issubg4m  13323  isnsg2  13333  nsgbi  13334  isnsg3  13337  elnmz  13338  nmzbi  13339  ghmlin  13378  ghmrn  13387  ghmnsgima  13398  conjghm  13406  conjnmz  13409  gsumfzconst  13471  rngdi  13496  rngdir  13497  srglz  13541  srgisid  13542  srglmhm  13549  ringid  13582  ringinvnz1ne0  13605  ringinvnzdiv  13606  ring1  13615  ringlghm  13617  imasring  13620  dvdsrtr  13657  lringuplu  13752  issubrng  13755  issubrng2  13766  issubrg  13777  issubrg2  13797  rrgeq0i  13820  rrgeq0  13821  unitrrg  13823  domneq0  13828  lmodlema  13848  islmodd  13849  rmodislmodlem  13906  rmodislmod  13907  lssclg  13920  lss1d  13939  rnglidlmcl  14036  quscrng  14089  cnfldexp  14133  gsumfzfsumlemm  14143  cnfldui  14145  expghmap  14163  zrhval  14173  zrhvalg  14174  znunit  14215  txdis1cn  14514  cnmptcom  14534  psmettri2  14564  isxmet2d  14584  xmeteq0  14595  xmettri2  14597  elblps  14626  elbl  14627  blssps  14663  blss  14664  ssblex  14667  blin2  14668  metss2  14734  comet  14735  bdmopn  14740  txmetcnp  14754  blssioo  14789  divcnap  14801  mpomulcn  14802  expcn  14805  cncfval  14808  cncfi  14814  mulc1cncf  14825  cdivcncfap  14840  mulcncf  14844  expcncf  14845  cnopnap  14847  ellimc3apf  14896  cnlimci  14909  limccnpcntop  14911  limccnp2lem  14912  reldvg  14915  eldvap  14918  dvexp  14947  dvexp2  14948  dvrecap  14949  elplyr  14976  elplyd  14977  ply1termlem  14978  plymullem1  14984  plyadd  14987  plymul  14988  plycoeid3  14993  plycolemc  14994  plyco  14995  plycj  14997  dvply1  15001  dvply2g  15002  sin0pilem2  15018  rpcxpmul2  15149  relogbcxpbap  15201  logbgcd1irr  15203  2irrexpq  15212  2irrexpqap  15214  dvdsppwf1o  15225  mpodvdsmulf1o  15226  fsumdvdsmul  15227  sgmppw  15228  1sgmprm  15230  perfect  15237  lgsneg  15265  lgsdilem  15268  lgsdir  15276  lgsdilem2  15277  lgsdi  15278  lgsne0  15279  lgsdirnn0  15288  lgsdinn0  15289  gausslemma2dlem4  15305  lgseisenlem2  15312  lgseisenlem3  15313  lgseisenlem4  15314  lgsquadlem1  15318  lgsquadlem2  15319  lgsquad2lem2  15323  2lgs  15345  2sqlem6  15361  2sqlem8  15364  2sqlem9  15365  2sqlem10  15366  trilpolemclim  15680  trilpolemcl  15681  trilpolemisumle  15682  trilpolemeq1  15684  trilpolemlt1  15685  trilpo  15687  trirec0  15688  redcwlpo  15699  nconstwlpolemgt0  15708  nconstwlpo  15710  neapmkv  15712