Theorem oveq2 6096

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 5702	. 2 |- ( A = B -> ( F ` <. C , A >. ) = ( F ` <. C , B >. ) )
3		df-ov 6091	. 2 |- ( C F A ) = ( F ` <. C , A >. )
4		df-ov 6091	. 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 5380  (class class class)co 6088

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 4132  df-iota 5340  df-fv 5388  df-ov 6091

This theorem is used by:  oveq12  6097  oveq2i  6099  oveq2d  6104  ovanraleqv  6112  ovrspc2v  6114  oveqrspc2v  6115  rspceov  6131  fovcld  6196  ovmpos  6215  ov2gf  6216  ovi3  6229  caovclg  6245  caovcomg  6248  caovassg  6251  caovcang  6254  caovcan  6257  caovordig  6258  caovordg  6260  caovord  6264  caovdig  6267  caovdirg  6270  caovimo  6286  suppssov1  6302  off  6319  caofid0l  6333  caofid2  6336  caofdig  6340  suppofss1dcl  6508  suppofss2dcl  6509  omv  6732  oeiv  6733  oasuc  6741  oawordriexmid  6747  omsuc  6749  nna0r  6755  nnm0r  6756  nnacl  6757  nnmcl  6758  nnacom  6761  nnaass  6762  nndi  6763  nnmass  6764  nnmsucr  6765  nnmcom  6766  nnaordi  6785  nnaord  6786  nnmordi  6793  nnmord  6794  nnaordex  6805  nnawordex  6806  nnm00  6807  eroveu  6904  ecopovtrn  6910  ecopovtrng  6913  th3qlem2  6916  th3q  6918  ecovcom  6920  ecovicom  6921  ecovass  6922  ecoviass  6923  ecovdi  6924  ecovidi  6925  exmidpw2en  7223  mapfi  7265  acneq  7564  addcanpig  7707  mulcanpig  7708  addcmpblnq  7740  addclnq  7748  mulclnq  7749  recexnq  7763  recmulnqg  7764  ltanqg  7773  ltmnqg  7774  ltexnqq  7781  enq0ref  7806  enq0tr  7807  addcmpblnq0  7816  mulnnnq0  7823  addclnq0  7824  mulclnq0  7825  distrnq0  7832  mulcomnq0  7833  addassnq0  7835  nq02m  7838  prarloclem3  7870  genipv  7882  genpassl  7897  genpassu  7898  addlocpr  7909  distrlem1prl  7955  distrlem1pru  7956  1idprl  7963  1idpru  7964  ltexprlemell  7971  ltexprlemelu  7972  ltexpri  7986  lteupri  7990  ltaprlem  7991  recexprlem1ssl  8006  recexprlem1ssu  8007  recexpr  8011  cauappcvgprlemm  8018  cauappcvgprlemdisj  8024  cauappcvgprlemloc  8025  cauappcvgprlemladdru  8029  cauappcvgprlemladdrl  8030  cauappcvgprlem1  8032  cauappcvgprlemlim  8034  cauappcvgpr  8035  mulcmpblnrlemg  8113  addclsr  8126  mulclsr  8127  ltasrg  8143  negexsr  8145  recexgt0sr  8146  mulgt0sr  8151  mulextsr1  8154  srpospr  8156  caucvgsrlemgt1  8168  map2psrprg  8178  axaddrcl  8238  axmulrcl  8240  axaddcom  8243  axrnegex  8252  axprecex  8253  axcnre  8254  axpre-ltadd  8259  axpre-mulgt0  8260  axpre-mulext  8261  rereceu  8262  recriota  8263  axcaucvglemres  8272  readdcan  8473  cnegexlem1  8508  cnegex  8511  addcan  8513  negeq  8526  subadd  8536  addid0  8706  ine0  8728  rimul  8921  cru  8938  apreim  8939  recexap  8989  mulcanapd  8997  receuap  9007  divmulap  9013  rerecapb  9181  cju  9299  nnaddcl  9333  nnmulcl  9334  nnsub  9352  nnnn0addcl  9604  zaddcllempos  9692  zaddcl  9695  zdiv  9745  deceq1  9792  deceq2  9793  uzaddcl  10002  zq  10042  qreccl  10058  cnref1o  10068  xaddnemnf  10276  xaddnepnf  10277  xaddcom  10280  xnn0xadd0  10286  xnegdi  10287  xaddass  10288  xlt2add  10299  xlesubadd  10302  xleaddadd  10306  fzsuc2  10503  fzrevral  10529  fzshftral  10532  2ffzeq  10565  exfzdc  10676  exbtwnzlemshrink  10700  rebtwn2zlemshrink  10705  modqval  10782  modqmuladd  10824  modqmuladdnn0  10826  frecuzrdgrrn  10866  frec2uzrdg  10867  frecuzrdgrcl  10868  frecuzrdgsuc  10872  frecuzrdgrclt  10873  frecuzrdgg  10874  frecuzrdgsuctlem  10881  frecfzennn  10884  uzsinds  10902  iseqvalcbv  10917  seq3val  10918  seqvalcd  10919  seqovcd  10925  seq3caopr3  10949  seq3caopr2  10951  seqcaopr2g  10952  seq3f1olemp  10973  seqf1og  10979  seq3id  10983  seq3homo  10985  seq3z  10986  seqhomog  10988  seqfeq4g  10989  seq3distr  10990  expp1  11004  expnegap0  11005  expcllem  11008  expcl2lemap  11009  m1expcl2  11019  expap0  11027  mulexp  11036  expadd  11039  expmul  11042  leexp2r  11051  leexp1a  11052  bernneq  11119  expnbnd  11122  modqexp  11125  nn0ltexp2  11169  expcan  11176  apexp1  11178  facdiv  11198  faclbnd3  11203  faclbnd6  11204  bcval  11209  bcpasc  11226  bccl  11227  fz1eqb  11251  omgadd  11264  hashunlem  11266  hashfzo  11285  hashfzp1  11287  hashmap  11290  hashfibclem  11304  hashfibc  11305  hashf1  11309  iswrdinn0  11331  wrdnval  11357  eqwrd  11367  eqs1  11418  pfxeq  11490  ccatopth  11510  wrd2ind  11517  swrdccatin1  11519  swrdccatin2  11523  pfxccatin12lem2  11525  swrdccat3blem  11533  pfxccatid  11535  swrdccatin1d  11537  swrdccatin2d  11538  s2dmg  11584  shftfvalg  11605  shftfval  11608  cjth  11633  remim  11647  reim0b  11649  cjexp  11680  cnrecnv  11698  cvg1nlemcau  11772  cvg1nlemres  11773  recvguniq  11783  resqrexlemp1rp  11794  resqrexlemfp1  11797  resqrexlemlo  11801  resqrexlemgt0  11808  resqrexlemoverl  11809  resqrexlemglsq  11810  resqrexlemsqa  11812  resqrexlemex  11813  resqrex  11814  absexp  11868  recan  11898  climcn2  12100  subcn2  12102  summodc  12175  fsum3  12179  fsum3cvg3  12188  fsumrev  12235  fisum0diag2  12239  telfsumo  12258  fsumrelem  12263  binomlem  12275  binom  12276  binom1dif  12279  bcxmaslem1  12280  bcxmas  12281  isumshft  12282  divcnv  12289  arisum  12290  trireciplem  12292  expcnvap0  12294  expcnvre  12295  expcnv  12296  explecnv  12297  geosergap  12298  geolim  12303  geolim2  12304  geo2sum  12306  geo2lim  12308  geoisum  12309  geoisumr  12310  geoisum1  12311  geoisum1c  12312  cvgratnnlemsumlt  12320  cvgratz  12324  prodmodc  12370  fprodseq  12375  fprodcl2lem  12397  fprodfac  12407  fprodabs  12408  fprodrev  12411  eftvalcn  12449  efcvgfsum  12459  ege2le3  12463  efcj  12465  efaddlem  12466  efexp  12474  eftlub  12482  efgt1p2  12487  eflegeo  12493  sinval  12494  cosval  12495  demoivreALT  12566  divides  12581  dvdscmul  12610  dvds2ln  12616  dvdstr  12620  odd2np1lem  12664  odd2np1  12665  2tp1odd  12676  opeo  12689  omeo  12690  m1expe  12691  m1expo  12692  m1exp1  12693  divalglemnn  12710  divalglemeunn  12713  divalglemeuneg  12715  divalgmod  12719  ndvdssub  12722  bitsval  12735  bitsfzolem  12746  bitsinv1lem  12753  bitsinv1  12754  gcd0id  12781  bezoutlemnewy  12798  bezoutlema  12801  bezoutlemb  12802  bezoutlemex  12803  bezoutlemaz  12805  bezoutlembz  12806  gcdmultiple  12822  gcdmultiplez  12823  dvdsmulgcd  12827  rplpwr  12829  nn0seqcvgd  12844  dvdslcm  12872  lcmeq0  12874  lcmcl  12875  lcmneg  12877  lcmgcdlem  12880  lcmdvds  12882  lcmid  12883  lcmgcdeq  12886  coprmdvds  12895  mulgcddvds  12897  qredeq  12899  cncongr1  12906  cncongr2  12907  cncongrcoprm  12909  prmind2  12923  isprm6  12951  prmdvdsexp  12952  prmdvdsexpr  12954  sqrt2irr  12966  pwbdvdslemn  12969  pwbdvdseu  12972  nnmaxpwlemxy  12973  sqpweven  12980  2sqpwodd  12981  sqne2sq  12982  nn0gcdsq  13005  qden1elz  13010  phival  13020  dfphi2  13027  eulerthlemrprm  13036  eulerthlema  13037  prmdiv  13042  prmdiveq  13043  phisum  13048  odzval  13049  odzcllem  13050  odzdvds  13053  reumodprminv  13061  pythagtriplem3  13075  pythagtriplem18  13089  pythagtriplem19  13090  pclem0  13094  pclemub  13095  pclemdc  13096  pcprecl  13097  pcprendvds  13098  pcpremul  13101  pceulem  13102  pceu  13103  pczpre  13105  pcdiv  13110  pcqmul  13111  pcqcl  13114  pcexp  13117  pcxnn0cl  13118  pcxcl  13119  pcge0  13121  pcdvdsb  13128  pcneg  13133  pcabs  13134  pcgcd1  13136  pc2dvds  13138  pc11  13139  pcz  13140  pcprmpw2  13141  pcprmpw  13142  dvdsprmpweq  13143  dvdsprmpweqnn  13144  dvdsprmpweqle  13145  pcaddlem  13147  pcadd  13148  pcfac  13158  oddprmdvds  13162  prmpwdvds  13163  pockthi  13166  infpnlem2  13168  1arithlem1  13171  4sqlemffi  13204  4sqlem12  13210  2expltfac  13248  ballotfilemfval  13287  ballotfilemfc0  13290  ballotfilemfcc  13291  ballotfilemsv  13311  ballotfilemsf1o  13315  ballotfi  13340  ennnfonelemnn0  13371  ennnfonelemr  13372  f1ovscpbl  13692  imasaddvallemg  13695  ercpbl  13711  mgm1  13749  mgmidmo  13751  mgmlrid  13758  lidrideqd  13760  lidrididd  13761  grpinvalem  13764  grpinva  13765  gzsumfzval  13770  gzsumval2  13773  isnsgrp  13780  sgrpass  13782  sgrp1  13785  mndinvmod  13817  imasmnd2  13818  mnd1  13821  mnd1id  13822  mhmpropd  13832  mhmlin  13833  insubm  13851  mhmima  13857  gzsumwsubmcl  13860  gzsumwmhm  13862  grpinvex  13874  grppropd  13881  dfgrp2  13891  grpidd2  13905  grpinvval  13907  grpinvid1  13916  grplrinv  13921  grpidinv2  13922  grpidinv  13923  grplcan  13926  grpidssd  13940  grpinvssd  13941  dfgrp3mlem  13962  dfgrp3m  13963  grplactcnv  13966  grp1  13970  imasgrp2  13972  mhmlem  13976  mulgnn0gzsum  13990  mulginvcom  14009  mulgnn0ass  14020  mulgmodid  14023  issubg  14035  issubg2m  14051  issubg4m  14055  isnsg2  14065  nsgbi  14066  isnsg3  14069  elnmz  14070  nmzbi  14071  ghmlin  14110  ghmrn  14119  ghmnsgima  14130  conjghm  14138  conjnmz  14141  elcntz  14154  cntzsnval  14156  elcntzsn  14157  cntzi  14162  cntzmhm  14173  gzsumconst  14233  gsum2dfilem2  14272  gsum2d2fi  14274  gsumcom2fi  14275  rngdi  14346  rngdir  14347  srglz  14396  srgisid  14397  srglmhm  14404  ringid  14438  ringinvnz1ne0  14461  ringinvnzdiv  14462  ring1  14471  ringlghm  14473  gsummulc2fi  14476  imasring  14478  dvdsrtr  14517  lringuplu  14612  issubrng  14616  issubrng2  14627  issubrg  14638  issubrg2  14658  rrgeq0i  14681  rrgeq0  14682  unitrrg  14685  domneq0  14690  lmodlema  14737  islmodd  14738  rmodislmodlem  14796  rmodislmod  14797  lssclg  14810  lss1d  14829  rnglidlmcl  14926  quscrng  14979  cnfldexp  15023  gsumfsum  15032  cnfldui  15033  expghmap  15051  zrhval  15061  zrhvalg  15062  znunit  15103  assalem  15112  psrlidmfi  15199  psrridmfi  15200  psrass1fi  15201  txdis1cn  15504  cnmptcom  15524  psmettri2  15554  isxmet2d  15574  xmeteq0  15585  xmettri2  15587  elblps  15616  elbl  15617  blssps  15653  blss  15654  ssblex  15657  blin2  15658  metss2  15724  comet  15725  bdmopn  15730  txmetcnp  15744  blssioo  15779  divcnap  15791  mpomulcn  15792  expcn  15795  cncfval  15798  cncfi  15804  mulc1cncf  15815  cdivcncfap  15830  mulcncf  15834  expcncf  15835  cnopnap  15837  ellimc3apf  15886  cnlimci  15899  limccnpcntop  15901  limccnp2lem  15902  reldvg  15905  eldvap  15908  dvexp  15937  dvexp2  15938  dvrecap  15939  elplyr  15966  elplyd  15967  ply1termlem  15968  plymullem1  15974  plyadd  15977  plymul  15978  plycoeid3  15983  plycolemc  15984  plyco  15985  plycj  15987  dvply1  15991  dvply2g  15992  sin0pilem2  16009  sineq0re  16076  logfac  16126  rpcxpmul2  16146  relogbcxpbap  16201  logbgcd1irr  16203  2irrexpq  16212  2irrexpqap  16214  zprmlogbaplem2  16216  zprmlogbaplem3  16217  zprmlogbap  16218  log2tlbndlog2  16220  log2ublem2  16222  chtqcl  16244  chtqval  16245  ppiqval  16248  dvdsppwf1o  16283  mpodvdsmulf1o  16284  fsumdvdsmul  16285  sgmppw  16286  1sgmprm  16288  chtublem  16295  chtqub  16296  perfect  16301  bcmono  16304  bclbnd  16307  bposlem2  16312  bposlem7  16317  bposlem8  16318  bposlem9  16319  lgsneg  16348  lgsdilem  16351  lgsdir  16359  lgsdilem2  16360  lgsdi  16361  lgsne0  16362  lgsdirnn0  16371  lgsdinn0  16372  gausslemma2dlem4  16388  lgseisenlem2  16395  lgseisenlem3  16396  lgseisenlem4  16397  lgsquadlem1  16401  lgsquadlem2  16402  lgsquad2lem2  16406  2lgs  16428  2sqlem6  16444  2sqlem8  16447  2sqlem9  16448  2sqlem10  16449  wlkeq  16800  wlkl1loop  16804  uspgr2wlkeq  16811  upgr2wlkdc  16823  clwwlknonmpo  16874  eupth2fi  16925  trilpolemclim  17292  trilpolemcl  17293  trilpolemisumle  17294  trilpolemeq1  17296  trilpolemlt1  17297  trilpo  17299  trirec0  17300  qdiff  17305  redcwlpo  17312  nconstwlpolemgt0  17321  nconstwlpo  17323  neapmkv  17325