Theorem oveq2 6029

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 3863	. . 3 |- ( A = B -> <. C , A >. = <. C , B >. )
2	1	fveq2d 5644	. 2 |- ( A = B -> ( F ` <. C , A >. ) = ( F ` <. C , B >. ) )
3		df-ov 6024	. 2 |- ( C F A ) = ( F ` <. C , A >. )
4		df-ov 6024	. 2 |- ( C F B ) = ( F ` <. C , B >. )
5	2, 3, 4	3eqtr4g 2289	1 |- ( A = B -> ( C F A ) = ( C F B ) )

Syntax hints:   -> wi 4   = wceq 1397   <.cop 3672   ` cfv 5326  (class class class)co 6021

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 716  ax-5 1495  ax-7 1496  ax-gen 1497  ax-ie1 1541  ax-ie2 1542  ax-8 1552  ax-10 1553  ax-11 1554  ax-i12 1555  ax-bndl 1557  ax-4 1558  ax-17 1574  ax-i9 1578  ax-ial 1582  ax-i5r 1583  ax-ext 2213

This theorem depends on definitions:  df-bi 117  df-3an 1006  df-tru 1400  df-nf 1509  df-sb 1811  df-clab 2218  df-cleq 2224  df-clel 2227  df-nfc 2363  df-rex 2516  df-v 2804  df-un 3204  df-sn 3675  df-pr 3676  df-op 3678  df-uni 3894  df-br 4089  df-iota 5286  df-fv 5334  df-ov 6024

This theorem is referenced by:  oveq12  6030  oveq2i  6032  oveq2d  6037  ovanraleqv  6045  ovrspc2v  6047  oveqrspc2v  6048  rspceov  6064  fovcld  6129  ovmpos  6148  ov2gf  6149  ovi3  6162  caovclg  6178  caovcomg  6181  caovassg  6184  caovcang  6187  caovcan  6190  caovordig  6191  caovordg  6193  caovord  6197  caovdig  6200  caovdirg  6203  caovimo  6219  suppssov1  6235  off  6251  caofid0l  6265  caofid2  6268  caofdig  6272  omv  6626  oeiv  6627  oasuc  6635  oawordriexmid  6641  omsuc  6643  nna0r  6649  nnm0r  6650  nnacl  6651  nnmcl  6652  nnacom  6655  nnaass  6656  nndi  6657  nnmass  6658  nnmsucr  6659  nnmcom  6660  nnaordi  6679  nnaord  6680  nnmordi  6687  nnmord  6688  nnaordex  6699  nnawordex  6700  nnm00  6701  eroveu  6798  ecopovtrn  6804  ecopovtrng  6807  th3qlem2  6810  th3q  6812  ecovcom  6814  ecovicom  6815  ecovass  6816  ecoviass  6817  ecovdi  6818  ecovidi  6819  exmidpw2en  7107  acneq  7420  addcanpig  7557  mulcanpig  7558  addcmpblnq  7590  addclnq  7598  mulclnq  7599  recexnq  7613  recmulnqg  7614  ltanqg  7623  ltmnqg  7624  ltexnqq  7631  enq0ref  7656  enq0tr  7657  addcmpblnq0  7666  mulnnnq0  7673  addclnq0  7674  mulclnq0  7675  distrnq0  7682  mulcomnq0  7683  addassnq0  7685  nq02m  7688  prarloclem3  7720  genipv  7732  genpassl  7747  genpassu  7748  addlocpr  7759  distrlem1prl  7805  distrlem1pru  7806  1idprl  7813  1idpru  7814  ltexprlemell  7821  ltexprlemelu  7822  ltexpri  7836  lteupri  7840  ltaprlem  7841  recexprlem1ssl  7856  recexprlem1ssu  7857  recexpr  7861  cauappcvgprlemm  7868  cauappcvgprlemdisj  7874  cauappcvgprlemloc  7875  cauappcvgprlemladdru  7879  cauappcvgprlemladdrl  7880  cauappcvgprlem1  7882  cauappcvgprlemlim  7884  cauappcvgpr  7885  mulcmpblnrlemg  7963  addclsr  7976  mulclsr  7977  ltasrg  7993  negexsr  7995  recexgt0sr  7996  mulgt0sr  8001  mulextsr1  8004  srpospr  8006  caucvgsrlemgt1  8018  map2psrprg  8028  axaddrcl  8088  axmulrcl  8090  axaddcom  8093  axrnegex  8102  axprecex  8103  axcnre  8104  axpre-ltadd  8109  axpre-mulgt0  8110  axpre-mulext  8111  rereceu  8112  recriota  8113  axcaucvglemres  8122  readdcan  8322  cnegexlem1  8357  cnegex  8360  addcan  8362  negeq  8375  subadd  8385  addid0  8555  ine0  8576  rimul  8768  cru  8785  apreim  8786  recexap  8836  mulcanapd  8844  receuap  8852  divmulap  8858  rerecapb  9026  cju  9144  nnaddcl  9166  nnmulcl  9167  nnsub  9185  nnnn0addcl  9435  zaddcllempos  9519  zaddcl  9522  zdiv  9571  deceq1  9618  deceq2  9619  uzaddcl  9823  zq  9863  qreccl  9879  cnref1o  9888  xaddnemnf  10095  xaddnepnf  10096  xaddcom  10099  xnn0xadd0  10105  xnegdi  10106  xaddass  10107  xlt2add  10118  xlesubadd  10121  xleaddadd  10125  fzsuc2  10317  fzrevral  10343  fzshftral  10346  2ffzeq  10379  exfzdc  10490  exbtwnzlemshrink  10512  rebtwn2zlemshrink  10517  modqval  10590  modqmuladd  10632  modqmuladdnn0  10634  frecuzrdgrrn  10674  frec2uzrdg  10675  frecuzrdgrcl  10676  frecuzrdgsuc  10680  frecuzrdgrclt  10681  frecuzrdgg  10682  frecuzrdgsuctlem  10689  frecfzennn  10692  uzsinds  10710  iseqvalcbv  10725  seq3val  10726  seqvalcd  10727  seqovcd  10733  seq3caopr3  10757  seq3caopr2  10759  seqcaopr2g  10760  seq3f1olemp  10781  seqf1og  10787  seq3id  10791  seq3homo  10793  seq3z  10794  seqhomog  10796  seqfeq4g  10797  seq3distr  10798  expp1  10812  expnegap0  10813  expcllem  10816  expcl2lemap  10817  m1expcl2  10827  expap0  10835  mulexp  10844  expadd  10847  expmul  10850  leexp2r  10859  leexp1a  10860  bernneq  10926  expnbnd  10929  modqexp  10932  nn0ltexp2  10975  expcan  10982  apexp1  10984  facdiv  11004  faclbnd3  11009  faclbnd6  11010  bcval  11015  bcpasc  11032  bccl  11033  fz1eqb  11056  omgadd  11069  hashunlem  11071  hashfzo  11090  hashfzp1  11092  iswrdinn0  11125  wrdnval  11151  eqwrd  11161  eqs1  11212  pfxeq  11284  ccatopth  11304  wrd2ind  11311  swrdccatin1  11313  swrdccatin2  11317  pfxccatin12lem2  11319  swrdccat3blem  11327  pfxccatid  11329  swrdccatin1d  11331  swrdccatin2d  11332  s2dmg  11378  shftfvalg  11399  shftfval  11402  cjth  11427  remim  11441  reim0b  11443  cjexp  11474  cnrecnv  11491  cvg1nlemcau  11565  cvg1nlemres  11566  recvguniq  11576  resqrexlemp1rp  11587  resqrexlemfp1  11590  resqrexlemlo  11594  resqrexlemgt0  11601  resqrexlemoverl  11602  resqrexlemglsq  11603  resqrexlemsqa  11605  resqrexlemex  11606  resqrex  11607  absexp  11660  recan  11690  climcn2  11890  subcn2  11892  summodc  11965  fsum3  11969  fsum3cvg3  11978  fsumrev  12025  fisum0diag2  12029  telfsumo  12048  fsumrelem  12053  binomlem  12065  binom  12066  binom1dif  12069  bcxmaslem1  12070  bcxmas  12071  isumshft  12072  divcnv  12079  arisum  12080  trireciplem  12082  expcnvap0  12084  expcnvre  12085  expcnv  12086  explecnv  12087  geosergap  12088  geolim  12093  geolim2  12094  geo2sum  12096  geo2lim  12098  geoisum  12099  geoisumr  12100  geoisum1  12101  geoisum1c  12102  cvgratnnlemsumlt  12110  cvgratz  12114  prodmodc  12160  fprodseq  12165  fprodcl2lem  12187  fprodfac  12197  fprodabs  12198  fprodrev  12201  eftvalcn  12239  efcvgfsum  12249  ege2le3  12253  efcj  12255  efaddlem  12256  efexp  12264  eftlub  12272  efgt1p2  12277  eflegeo  12283  sinval  12284  cosval  12285  demoivreALT  12356  divides  12371  dvdscmul  12400  dvds2ln  12406  dvdstr  12410  odd2np1lem  12454  odd2np1  12455  2tp1odd  12466  opeo  12479  omeo  12480  m1expe  12481  m1expo  12482  m1exp1  12483  divalglemnn  12500  divalglemeunn  12503  divalglemeuneg  12505  divalgmod  12509  ndvdssub  12512  bitsval  12525  bitsfzolem  12536  bitsinv1lem  12543  bitsinv1  12544  gcd0id  12571  bezoutlemnewy  12588  bezoutlema  12591  bezoutlemb  12592  bezoutlemex  12593  bezoutlemaz  12595  bezoutlembz  12596  gcdmultiple  12612  gcdmultiplez  12613  dvdsmulgcd  12617  rplpwr  12619  nn0seqcvgd  12634  dvdslcm  12662  lcmeq0  12664  lcmcl  12665  lcmneg  12667  lcmgcdlem  12670  lcmdvds  12672  lcmid  12673  lcmgcdeq  12676  coprmdvds  12685  mulgcddvds  12687  qredeq  12689  cncongr1  12696  cncongr2  12697  cncongrcoprm  12699  prmind2  12713  isprm6  12740  prmdvdsexp  12741  prmdvdsexpr  12743  sqrt2irr  12755  pw2dvdslemn  12758  pw2dvdseu  12761  oddpwdclemxy  12762  sqpweven  12768  2sqpwodd  12769  sqne2sq  12770  nn0gcdsq  12793  qden1elz  12798  phival  12806  dfphi2  12813  eulerthlemrprm  12822  eulerthlema  12823  prmdiv  12828  prmdiveq  12829  phisum  12834  odzval  12835  odzcllem  12836  odzdvds  12839  reumodprminv  12847  pythagtriplem3  12861  pythagtriplem18  12875  pythagtriplem19  12876  pclem0  12880  pclemub  12881  pclemdc  12882  pcprecl  12883  pcprendvds  12884  pcpremul  12887  pceulem  12888  pceu  12889  pczpre  12891  pcdiv  12896  pcqmul  12897  pcqcl  12900  pcexp  12903  pcxnn0cl  12904  pcxcl  12905  pcge0  12907  pcdvdsb  12914  pcneg  12919  pcabs  12920  pcgcd1  12922  pc2dvds  12924  pc11  12925  pcz  12926  pcprmpw2  12927  pcprmpw  12928  dvdsprmpweq  12929  dvdsprmpweqnn  12930  dvdsprmpweqle  12931  pcaddlem  12933  pcadd  12934  pcfac  12944  oddprmdvds  12948  prmpwdvds  12949  pockthi  12952  infpnlem2  12954  1arithlem1  12957  4sqlemffi  12990  4sqlem12  12996  2expltfac  13033  ennnfonelemnn0  13064  ennnfonelemr  13065  f1ovscpbl  13416  imasaddvallemg  13419  ercpbl  13435  mgm1  13474  mgmidmo  13476  mgmlrid  13483  lidrideqd  13485  lidrididd  13486  grpinvalem  13489  grpinva  13490  gsumfzval  13495  gsumval2  13501  isnsgrp  13510  sgrpass  13512  sgrp1  13515  mndinvmod  13549  imasmnd2  13556  mnd1  13559  mnd1id  13560  mhmpropd  13570  mhmlin  13571  insubm  13589  mhmima  13595  gsumwsubmcl  13600  gsumwmhm  13602  grpinvex  13614  grppropd  13621  dfgrp2  13631  grpidd2  13645  grpinvval  13647  grpinvid1  13656  grplrinv  13661  grpidinv2  13662  grpidinv  13663  grplcan  13666  grpidssd  13680  grpinvssd  13681  dfgrp3mlem  13702  dfgrp3m  13703  grplactcnv  13706  grp1  13710  imasgrp2  13718  mhmlem  13722  mulgnn0gsum  13736  mulginvcom  13755  mulgnn0ass  13766  mulgmodid  13769  issubg  13781  issubg2m  13797  issubg4m  13801  isnsg2  13811  nsgbi  13812  isnsg3  13815  elnmz  13816  nmzbi  13817  ghmlin  13856  ghmrn  13865  ghmnsgima  13876  conjghm  13884  conjnmz  13887  gsumfzconst  13949  rngdi  13975  rngdir  13976  srglz  14020  srgisid  14021  srglmhm  14028  ringid  14061  ringinvnz1ne0  14084  ringinvnzdiv  14085  ring1  14094  ringlghm  14096  imasring  14099  dvdsrtr  14137  lringuplu  14232  issubrng  14235  issubrng2  14246  issubrg  14257  issubrg2  14277  rrgeq0i  14300  rrgeq0  14301  unitrrg  14303  domneq0  14308  lmodlema  14328  islmodd  14329  rmodislmodlem  14386  rmodislmod  14387  lssclg  14400  lss1d  14419  rnglidlmcl  14516  quscrng  14569  cnfldexp  14613  gsumfzfsumlemm  14623  cnfldui  14625  expghmap  14643  zrhval  14653  zrhvalg  14654  znunit  14695  txdis1cn  15029  cnmptcom  15049  psmettri2  15079  isxmet2d  15099  xmeteq0  15110  xmettri2  15112  elblps  15141  elbl  15142  blssps  15178  blss  15179  ssblex  15182  blin2  15183  metss2  15249  comet  15250  bdmopn  15255  txmetcnp  15269  blssioo  15304  divcnap  15316  mpomulcn  15317  expcn  15320  cncfval  15323  cncfi  15329  mulc1cncf  15340  cdivcncfap  15355  mulcncf  15359  expcncf  15360  cnopnap  15362  ellimc3apf  15411  cnlimci  15424  limccnpcntop  15426  limccnp2lem  15427  reldvg  15430  eldvap  15433  dvexp  15462  dvexp2  15463  dvrecap  15464  elplyr  15491  elplyd  15492  ply1termlem  15493  plymullem1  15499  plyadd  15502  plymul  15503  plycoeid3  15508  plycolemc  15509  plyco  15510  plycj  15512  dvply1  15516  dvply2g  15517  sin0pilem2  15533  rpcxpmul2  15664  relogbcxpbap  15716  logbgcd1irr  15718  2irrexpq  15727  2irrexpqap  15729  dvdsppwf1o  15740  mpodvdsmulf1o  15741  fsumdvdsmul  15742  sgmppw  15743  1sgmprm  15745  perfect  15752  lgsneg  15780  lgsdilem  15783  lgsdir  15791  lgsdilem2  15792  lgsdi  15793  lgsne0  15794  lgsdirnn0  15803  lgsdinn0  15804  gausslemma2dlem4  15820  lgseisenlem2  15827  lgseisenlem3  15828  lgseisenlem4  15829  lgsquadlem1  15833  lgsquadlem2  15834  lgsquad2lem2  15838  2lgs  15860  2sqlem6  15876  2sqlem8  15879  2sqlem9  15880  2sqlem10  15881  wlkeq  16232  wlkl1loop  16236  uspgr2wlkeq  16243  upgr2wlkdc  16255  clwwlknonmpo  16306  eupth2fi  16357  trilpolemclim  16699  trilpolemcl  16700  trilpolemisumle  16701  trilpolemeq1  16703  trilpolemlt1  16704  trilpo  16706  trirec0  16707  qdiff  16712  redcwlpo  16719  nconstwlpolemgt0  16728  nconstwlpo  16730  neapmkv  16732