Theorem oveq2 6093

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 3905	. . 3 |- ( A = B -> <. C , A >. = <. C , B >. )
2	1	fveq2d 5699	. 2 |- ( A = B -> ( F ` <. C , A >. ) = ( F ` <. C , B >. ) )
3		df-ov 6088	. 2 |- ( C F A ) = ( F ` <. C , A >. )
4		df-ov 6088	. 2 |- ( C F B ) = ( F ` <. C , B >. )
5	2, 3, 4	3eqtr4g 2296	1 |- ( A = B -> ( C F A ) = ( C F B ) )

This proof depends on syntax axioms:   -> wi 4   = wceq 1402   <.cop 3712   ` cfv 5377  (class class class)co 6085

This proof depends on axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-ia1 106  ax-ia2 107  ax-ia3 108  ax-io 721  ax-5 1500  ax-7 1501  ax-gen 1502  ax-ie1 1546  ax-ie2 1547  ax-8 1557  ax-10 1558  ax-11 1559  ax-i12 1560  ax-bndl 1562  ax-4 1563  ax-17 1579  ax-i9 1583  ax-ial 1587  ax-i5r 1588  ax-ext 2220

This proof depends on definitions:  df-bi 117  df-3an 1011  df-tru 1405  df-nf 1514  df-sb 1816  df-clab 2225  df-cleq 2231  df-clel 2234  df-nfc 2381  df-rex 2534  df-v 2823  df-un 3224  df-sn 3715  df-pr 3716  df-op 3718  df-uni 3936  df-br 4131  df-iota 5337  df-fv 5385  df-ov 6088

This theorem is used by:  oveq12  6094  oveq2i  6096  oveq2d  6101  ovanraleqv  6109  ovrspc2v  6111  oveqrspc2v  6112  rspceov  6128  fovcld  6193  ovmpos  6212  ov2gf  6213  ovi3  6226  caovclg  6242  caovcomg  6245  caovassg  6248  caovcang  6251  caovcan  6254  caovordig  6255  caovordg  6257  caovord  6261  caovdig  6264  caovdirg  6267  caovimo  6283  suppssov1  6299  off  6315  caofid0l  6329  caofid2  6332  caofdig  6336  suppofss1dcl  6504  suppofss2dcl  6505  omv  6728  oeiv  6729  oasuc  6737  oawordriexmid  6743  omsuc  6745  nna0r  6751  nnm0r  6752  nnacl  6753  nnmcl  6754  nnacom  6757  nnaass  6758  nndi  6759  nnmass  6760  nnmsucr  6761  nnmcom  6762  nnaordi  6781  nnaord  6782  nnmordi  6789  nnmord  6790  nnaordex  6801  nnawordex  6802  nnm00  6803  eroveu  6900  ecopovtrn  6906  ecopovtrng  6909  th3qlem2  6912  th3q  6914  ecovcom  6916  ecovicom  6917  ecovass  6918  ecoviass  6919  ecovdi  6920  ecovidi  6921  exmidpw2en  7219  mapfi  7261  acneq  7558  addcanpig  7701  mulcanpig  7702  addcmpblnq  7734  addclnq  7742  mulclnq  7743  recexnq  7757  recmulnqg  7758  ltanqg  7767  ltmnqg  7768  ltexnqq  7775  enq0ref  7800  enq0tr  7801  addcmpblnq0  7810  mulnnnq0  7817  addclnq0  7818  mulclnq0  7819  distrnq0  7826  mulcomnq0  7827  addassnq0  7829  nq02m  7832  prarloclem3  7864  genipv  7876  genpassl  7891  genpassu  7892  addlocpr  7903  distrlem1prl  7949  distrlem1pru  7950  1idprl  7957  1idpru  7958  ltexprlemell  7965  ltexprlemelu  7966  ltexpri  7980  lteupri  7984  ltaprlem  7985  recexprlem1ssl  8000  recexprlem1ssu  8001  recexpr  8005  cauappcvgprlemm  8012  cauappcvgprlemdisj  8018  cauappcvgprlemloc  8019  cauappcvgprlemladdru  8023  cauappcvgprlemladdrl  8024  cauappcvgprlem1  8026  cauappcvgprlemlim  8028  cauappcvgpr  8029  mulcmpblnrlemg  8107  addclsr  8120  mulclsr  8121  ltasrg  8137  negexsr  8139  recexgt0sr  8140  mulgt0sr  8145  mulextsr1  8148  srpospr  8150  caucvgsrlemgt1  8162  map2psrprg  8172  axaddrcl  8232  axmulrcl  8234  axaddcom  8237  axrnegex  8246  axprecex  8247  axcnre  8248  axpre-ltadd  8253  axpre-mulgt0  8254  axpre-mulext  8255  rereceu  8256  recriota  8257  axcaucvglemres  8266  readdcan  8467  cnegexlem1  8502  cnegex  8505  addcan  8507  negeq  8520  subadd  8530  addid0  8700  ine0  8722  rimul  8915  cru  8932  apreim  8933  recexap  8983  mulcanapd  8991  receuap  9001  divmulap  9007  rerecapb  9175  cju  9293  nnaddcl  9326  nnmulcl  9327  nnsub  9345  nnnn0addcl  9597  zaddcllempos  9685  zaddcl  9688  zdiv  9738  deceq1  9785  deceq2  9786  uzaddcl  9995  zq  10035  qreccl  10051  cnref1o  10061  xaddnemnf  10269  xaddnepnf  10270  xaddcom  10273  xnn0xadd0  10279  xnegdi  10280  xaddass  10281  xlt2add  10292  xlesubadd  10295  xleaddadd  10299  fzsuc2  10496  fzrevral  10522  fzshftral  10525  2ffzeq  10558  exfzdc  10669  exbtwnzlemshrink  10693  rebtwn2zlemshrink  10698  modqval  10774  modqmuladd  10816  modqmuladdnn0  10818  frecuzrdgrrn  10858  frec2uzrdg  10859  frecuzrdgrcl  10860  frecuzrdgsuc  10864  frecuzrdgrclt  10865  frecuzrdgg  10866  frecuzrdgsuctlem  10873  frecfzennn  10876  uzsinds  10894  iseqvalcbv  10909  seq3val  10910  seqvalcd  10911  seqovcd  10917  seq3caopr3  10941  seq3caopr2  10943  seqcaopr2g  10944  seq3f1olemp  10965  seqf1og  10971  seq3id  10975  seq3homo  10977  seq3z  10978  seqhomog  10980  seqfeq4g  10981  seq3distr  10982  expp1  10996  expnegap0  10997  expcllem  11000  expcl2lemap  11001  m1expcl2  11011  expap0  11019  mulexp  11028  expadd  11031  expmul  11034  leexp2r  11043  leexp1a  11044  bernneq  11111  expnbnd  11114  modqexp  11117  nn0ltexp2  11161  expcan  11168  apexp1  11170  facdiv  11190  faclbnd3  11195  faclbnd6  11196  bcval  11201  bcpasc  11218  bccl  11219  fz1eqb  11243  omgadd  11256  hashunlem  11258  hashfzo  11277  hashfzp1  11279  hashmap  11282  hashfibclem  11296  hashfibc  11297  hashf1  11301  iswrdinn0  11323  wrdnval  11349  eqwrd  11359  eqs1  11410  pfxeq  11482  ccatopth  11502  wrd2ind  11509  swrdccatin1  11511  swrdccatin2  11515  pfxccatin12lem2  11517  swrdccat3blem  11525  pfxccatid  11527  swrdccatin1d  11529  swrdccatin2d  11530  s2dmg  11576  shftfvalg  11597  shftfval  11600  cjth  11625  remim  11639  reim0b  11641  cjexp  11672  cnrecnv  11690  cvg1nlemcau  11764  cvg1nlemres  11765  recvguniq  11775  resqrexlemp1rp  11786  resqrexlemfp1  11789  resqrexlemlo  11793  resqrexlemgt0  11800  resqrexlemoverl  11801  resqrexlemglsq  11802  resqrexlemsqa  11804  resqrexlemex  11805  resqrex  11806  absexp  11860  recan  11890  climcn2  12091  subcn2  12093  summodc  12166  fsum3  12170  fsum3cvg3  12179  fsumrev  12226  fisum0diag2  12230  telfsumo  12249  fsumrelem  12254  binomlem  12266  binom  12267  binom1dif  12270  bcxmaslem1  12271  bcxmas  12272  isumshft  12273  divcnv  12280  arisum  12281  trireciplem  12283  expcnvap0  12285  expcnvre  12286  expcnv  12287  explecnv  12288  geosergap  12289  geolim  12294  geolim2  12295  geo2sum  12297  geo2lim  12299  geoisum  12300  geoisumr  12301  geoisum1  12302  geoisum1c  12303  cvgratnnlemsumlt  12311  cvgratz  12315  prodmodc  12361  fprodseq  12366  fprodcl2lem  12388  fprodfac  12398  fprodabs  12399  fprodrev  12402  eftvalcn  12440  efcvgfsum  12450  ege2le3  12454  efcj  12456  efaddlem  12457  efexp  12465  eftlub  12473  efgt1p2  12478  eflegeo  12484  sinval  12485  cosval  12486  demoivreALT  12557  divides  12572  dvdscmul  12601  dvds2ln  12607  dvdstr  12611  odd2np1lem  12655  odd2np1  12656  2tp1odd  12667  opeo  12680  omeo  12681  m1expe  12682  m1expo  12683  m1exp1  12684  divalglemnn  12701  divalglemeunn  12704  divalglemeuneg  12706  divalgmod  12710  ndvdssub  12713  bitsval  12726  bitsfzolem  12737  bitsinv1lem  12744  bitsinv1  12745  gcd0id  12772  bezoutlemnewy  12789  bezoutlema  12792  bezoutlemb  12793  bezoutlemex  12794  bezoutlemaz  12796  bezoutlembz  12797  gcdmultiple  12813  gcdmultiplez  12814  dvdsmulgcd  12818  rplpwr  12820  nn0seqcvgd  12835  dvdslcm  12863  lcmeq0  12865  lcmcl  12866  lcmneg  12868  lcmgcdlem  12871  lcmdvds  12873  lcmid  12874  lcmgcdeq  12877  coprmdvds  12886  mulgcddvds  12888  qredeq  12890  cncongr1  12897  cncongr2  12898  cncongrcoprm  12900  prmind2  12914  isprm6  12942  prmdvdsexp  12943  prmdvdsexpr  12945  sqrt2irr  12957  pwbdvdslemn  12960  pwbdvdseu  12963  nnmaxpwlemxy  12964  sqpweven  12971  2sqpwodd  12972  sqne2sq  12973  nn0gcdsq  12996  qden1elz  13001  phival  13011  dfphi2  13018  eulerthlemrprm  13027  eulerthlema  13028  prmdiv  13033  prmdiveq  13034  phisum  13039  odzval  13040  odzcllem  13041  odzdvds  13044  reumodprminv  13052  pythagtriplem3  13066  pythagtriplem18  13080  pythagtriplem19  13081  pclem0  13085  pclemub  13086  pclemdc  13087  pcprecl  13088  pcprendvds  13089  pcpremul  13092  pceulem  13093  pceu  13094  pczpre  13096  pcdiv  13101  pcqmul  13102  pcqcl  13105  pcexp  13108  pcxnn0cl  13109  pcxcl  13110  pcge0  13112  pcdvdsb  13119  pcneg  13124  pcabs  13125  pcgcd1  13127  pc2dvds  13129  pc11  13130  pcz  13131  pcprmpw2  13132  pcprmpw  13133  dvdsprmpweq  13134  dvdsprmpweqnn  13135  dvdsprmpweqle  13136  pcaddlem  13138  pcadd  13139  pcfac  13149  oddprmdvds  13153  prmpwdvds  13154  pockthi  13157  infpnlem2  13159  1arithlem1  13162  4sqlemffi  13195  4sqlem12  13201  2expltfac  13239  ballotfilemfval  13278  ballotfilemfc0  13281  ballotfilemfcc  13282  ballotfilemsv  13302  ballotfilemsf1o  13306  ballotfi  13331  ennnfonelemnn0  13362  ennnfonelemr  13363  f1ovscpbl  13682  imasaddvallemg  13685  ercpbl  13701  mgm1  13739  mgmidmo  13741  mgmlrid  13748  lidrideqd  13750  lidrididd  13751  grpinvalem  13754  grpinva  13755  gzsumfzval  13760  gzsumval2  13763  isnsgrp  13770  sgrpass  13772  sgrp1  13775  mndinvmod  13807  imasmnd2  13808  mnd1  13811  mnd1id  13812  mhmpropd  13822  mhmlin  13823  insubm  13841  mhmima  13847  gzsumwsubmcl  13850  gzsumwmhm  13852  grpinvex  13864  grppropd  13871  dfgrp2  13881  grpidd2  13895  grpinvval  13897  grpinvid1  13906  grplrinv  13911  grpidinv2  13912  grpidinv  13913  grplcan  13916  grpidssd  13930  grpinvssd  13931  dfgrp3mlem  13952  dfgrp3m  13953  grplactcnv  13956  grp1  13960  imasgrp2  13962  mhmlem  13966  mulgnn0gzsum  13980  mulginvcom  13999  mulgnn0ass  14010  mulgmodid  14013  issubg  14025  issubg2m  14041  issubg4m  14045  isnsg2  14055  nsgbi  14056  isnsg3  14059  elnmz  14060  nmzbi  14061  ghmlin  14100  ghmrn  14109  ghmnsgima  14120  conjghm  14128  conjnmz  14131  gzsumconst  14192  rngdi  14288  rngdir  14289  srglz  14338  srgisid  14339  srglmhm  14346  ringid  14380  ringinvnz1ne0  14403  ringinvnzdiv  14404  ring1  14413  ringlghm  14415  imasring  14418  dvdsrtr  14457  lringuplu  14552  issubrng  14556  issubrng2  14567  issubrg  14578  issubrg2  14598  rrgeq0i  14621  rrgeq0  14622  unitrrg  14625  domneq0  14630  lmodlema  14677  islmodd  14678  rmodislmodlem  14736  rmodislmod  14737  lssclg  14750  lss1d  14769  rnglidlmcl  14866  quscrng  14919  cnfldexp  14963  gsumfsum  14972  cnfldui  14973  expghmap  14991  zrhval  15001  zrhvalg  15002  znunit  15043  assalem  15052  txdis1cn  15428  cnmptcom  15448  psmettri2  15478  isxmet2d  15498  xmeteq0  15509  xmettri2  15511  elblps  15540  elbl  15541  blssps  15577  blss  15578  ssblex  15581  blin2  15582  metss2  15648  comet  15649  bdmopn  15654  txmetcnp  15668  blssioo  15703  divcnap  15715  mpomulcn  15716  expcn  15719  cncfval  15722  cncfi  15728  mulc1cncf  15739  cdivcncfap  15754  mulcncf  15758  expcncf  15759  cnopnap  15761  ellimc3apf  15810  cnlimci  15823  limccnpcntop  15825  limccnp2lem  15826  reldvg  15829  eldvap  15832  dvexp  15861  dvexp2  15862  dvrecap  15863  elplyr  15890  elplyd  15891  ply1termlem  15892  plymullem1  15898  plyadd  15901  plymul  15902  plycoeid3  15907  plycolemc  15908  plyco  15909  plycj  15911  dvply1  15915  dvply2g  15916  sin0pilem2  15933  logfac  16048  rpcxpmul2  16068  relogbcxpbap  16120  logbgcd1irr  16122  2irrexpq  16131  2irrexpqap  16133  zprmlogbaplem2  16135  zprmlogbaplem3  16136  zprmlogbap  16137  log2tlbndlog2  16139  log2ublem2  16141  ppiqval  16160  dvdsppwf1o  16184  mpodvdsmulf1o  16185  fsumdvdsmul  16186  sgmppw  16187  1sgmprm  16189  perfect  16199  bcmono  16202  bclbnd  16205  bposlem2  16210  lgsneg  16241  lgsdilem  16244  lgsdir  16252  lgsdilem2  16253  lgsdi  16254  lgsne0  16255  lgsdirnn0  16264  lgsdinn0  16265  gausslemma2dlem4  16281  lgseisenlem2  16288  lgseisenlem3  16289  lgseisenlem4  16290  lgsquadlem1  16294  lgsquadlem2  16295  lgsquad2lem2  16299  2lgs  16321  2sqlem6  16337  2sqlem8  16340  2sqlem9  16341  2sqlem10  16342  wlkeq  16693  wlkl1loop  16697  uspgr2wlkeq  16704  upgr2wlkdc  16716  clwwlknonmpo  16767  eupth2fi  16818  trilpolemclim  17183  trilpolemcl  17184  trilpolemisumle  17185  trilpolemeq1  17187  trilpolemlt1  17188  trilpo  17190  trirec0  17191  qdiff  17196  redcwlpo  17203  nconstwlpolemgt0  17212  nconstwlpo  17214  neapmkv  17216