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  6733  oeiv  6734  oasuc  6742  oawordriexmid  6748  omsuc  6750  nna0r  6756  nnm0r  6757  nnacl  6758  nnmcl  6759  nnacom  6762  nnaass  6763  nndi  6764  nnmass  6765  nnmsucr  6766  nnmcom  6767  nnaordi  6786  nnaord  6787  nnmordi  6794  nnmord  6795  nnaordex  6806  nnawordex  6807  nnm00  6808  eroveu  6905  ecopovtrn  6911  ecopovtrng  6914  th3qlem2  6917  th3q  6919  ecovcom  6921  ecovicom  6922  ecovass  6923  ecoviass  6924  ecovdi  6925  ecovidi  6926  exmidpw2en  7225  mapfi  7267  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  9690  zaddcl  9693  zdiv  9744  deceq1  9791  deceq2  9792  uzaddcl  10001  zq  10041  qreccl  10057  cnref1o  10067  xaddnemnf  10275  xaddnepnf  10276  xaddcom  10279  xnn0xadd0  10285  xnegdi  10286  xaddass  10287  xlt2add  10298  xlesubadd  10301  xleaddadd  10305  fzsuc2  10502  fzrevral  10528  fzshftral  10531  2ffzeq  10564  exfzdc  10675  exbtwnzlemshrink  10699  rebtwn2zlemshrink  10704  modqval  10781  modqmuladd  10823  modqmuladdnn0  10825  frecuzrdgrrn  10865  frec2uzrdg  10866  frecuzrdgrcl  10867  frecuzrdgsuc  10871  frecuzrdgrclt  10872  frecuzrdgg  10873  frecuzrdgsuctlem  10880  frecfzennn  10883  uzsinds  10901  iseqvalcbv  10916  seq3val  10917  seqvalcd  10918  seqovcd  10924  seq3caopr3  10948  seq3caopr2  10950  seqcaopr2g  10951  seq3f1olemp  10972  seqf1og  10978  seq3id  10982  seq3homo  10984  seq3z  10985  seqhomog  10987  seqfeq4g  10988  seq3distr  10989  expp1  11003  expnegap0  11004  expcllem  11007  expcl2lemap  11008  m1expcl2  11018  expap0  11026  mulexp  11035  expadd  11038  expmul  11041  leexp2r  11050  leexp1a  11051  bernneq  11118  expnbnd  11121  modqexp  11124  nn0ltexp2  11168  expcan  11175  apexp1  11177  facdiv  11197  faclbnd3  11202  faclbnd6  11203  bcval  11208  bcpasc  11225  bccl  11226  fz1eqb  11250  omgadd  11263  hashunlem  11265  hashfzo  11284  hashfzp1  11286  hashmap  11289  hashfibclem  11303  hashfibc  11304  hashf1  11308  iswrdinn0  11330  wrdnval  11356  eqwrd  11366  eqs1  11417  pfxeq  11489  ccatopth  11509  wrd2ind  11516  swrdccatin1  11518  swrdccatin2  11522  pfxccatin12lem2  11524  swrdccat3blem  11532  pfxccatid  11534  swrdccatin1d  11536  swrdccatin2d  11537  s2dmg  11583  shftfvalg  11604  shftfval  11607  cjth  11632  remim  11646  reim0b  11648  cjexp  11679  cnrecnv  11697  cvg1nlemcau  11771  cvg1nlemres  11772  recvguniq  11782  resqrexlemp1rp  11793  resqrexlemfp1  11796  resqrexlemlo  11800  resqrexlemgt0  11807  resqrexlemoverl  11808  resqrexlemglsq  11809  resqrexlemsqa  11811  resqrexlemex  11812  resqrex  11813  absexp  11867  recan  11897  climcn2  12099  subcn2  12101  summodc  12174  fsum3  12178  fsum3cvg3  12187  fsumrev  12234  fisum0diag2  12238  telfsumo  12257  fsumrelem  12262  binomlem  12274  binom  12275  binom1dif  12278  bcxmaslem1  12279  bcxmas  12280  isumshft  12281  divcnv  12288  arisum  12289  trireciplem  12291  expcnvap0  12293  expcnvre  12294  expcnv  12295  explecnv  12296  geosergap  12297  geolim  12302  geolim2  12303  geo2sum  12305  geo2lim  12307  geoisum  12308  geoisumr  12309  geoisum1  12310  geoisum1c  12311  cvgratnnlemsumlt  12319  cvgratz  12323  prodmodc  12369  fprodseq  12374  fprodcl2lem  12396  fprodfac  12406  fprodabs  12407  fprodrev  12410  eftvalcn  12448  efcvgfsum  12458  ege2le3  12462  efcj  12464  efaddlem  12465  efexp  12473  eftlub  12481  efgt1p2  12486  eflegeo  12492  sinval  12493  cosval  12494  demoivreALT  12565  divides  12580  dvdscmul  12609  dvds2ln  12615  dvdstr  12619  odd2np1lem  12663  odd2np1  12664  2tp1odd  12675  opeo  12688  omeo  12689  m1expe  12690  m1expo  12691  m1exp1  12692  divalglemnn  12709  divalglemeunn  12712  divalglemeuneg  12714  divalgmod  12718  ndvdssub  12721  bitsval  12734  bitsfzolem  12745  bitsinv1lem  12752  bitsinv1  12753  gcd0id  12780  bezoutlemnewy  12797  bezoutlema  12800  bezoutlemb  12801  bezoutlemex  12802  bezoutlemaz  12804  bezoutlembz  12805  gcdmultiple  12821  gcdmultiplez  12822  dvdsmulgcd  12826  rplpwr  12828  nn0seqcvgd  12843  dvdslcm  12871  lcmeq0  12873  lcmcl  12874  lcmneg  12876  lcmgcdlem  12879  lcmdvds  12881  lcmid  12882  lcmgcdeq  12885  coprmdvds  12894  mulgcddvds  12896  qredeq  12898  cncongr1  12905  cncongr2  12906  cncongrcoprm  12908  prmind2  12922  isprm6  12950  prmdvdsexp  12951  prmdvdsexpr  12953  sqrt2irr  12965  pwbdvdslemn  12968  pwbdvdseu  12971  nnmaxpwlemxy  12972  sqpweven  12979  2sqpwodd  12980  sqne2sq  12981  nn0gcdsq  13004  qden1elz  13009  phival  13019  dfphi2  13026  eulerthlemrprm  13035  eulerthlema  13036  prmdiv  13041  prmdiveq  13042  phisum  13047  odzval  13048  odzcllem  13049  odzdvds  13052  reumodprminv  13060  pythagtriplem3  13074  pythagtriplem18  13088  pythagtriplem19  13089  pclem0  13093  pclemub  13094  pclemdc  13095  pcprecl  13096  pcprendvds  13097  pcpremul  13100  pceulem  13101  pceu  13102  pczpre  13104  pcdiv  13109  pcqmul  13110  pcqcl  13113  pcexp  13116  pcxnn0cl  13117  pcxcl  13118  pcge0  13120  pcdvdsb  13127  pcneg  13132  pcabs  13133  pcgcd1  13135  pc2dvds  13137  pc11  13138  pcz  13139  pcprmpw2  13140  pcprmpw  13141  dvdsprmpweq  13142  dvdsprmpweqnn  13143  dvdsprmpweqle  13144  pcaddlem  13146  pcadd  13147  pcfac  13157  oddprmdvds  13161  prmpwdvds  13162  pockthi  13165  infpnlem2  13167  1arithlem1  13170  4sqlemffi  13203  4sqlem12  13209  2expltfac  13247  ballotfilemfval  13286  ballotfilemfc0  13289  ballotfilemfcc  13290  ballotfilemsv  13310  ballotfilemsf1o  13314  ballotfi  13339  ennnfonelemnn0  13370  ennnfonelemr  13371  f1ovscpbl  13691  imasaddvallemg  13694  ercpbl  13710  mgm1  13748  mgmidmo  13750  mgmlrid  13757  lidrideqd  13759  lidrididd  13760  grpinvalem  13763  grpinva  13764  gzsumfzval  13769  gzsumval2  13772  isnsgrp  13779  sgrpass  13781  sgrp1  13784  mndinvmod  13816  imasmnd2  13817  mnd1  13820  mnd1id  13821  mhmpropd  13831  mhmlin  13832  insubm  13850  mhmima  13856  gzsumwsubmcl  13859  gzsumwmhm  13861  grpinvex  13873  grppropd  13880  dfgrp2  13890  grpidd2  13904  grpinvval  13906  grpinvid1  13915  grplrinv  13920  grpidinv2  13921  grpidinv  13922  grplcan  13925  grpidssd  13939  grpinvssd  13940  dfgrp3mlem  13961  dfgrp3m  13962  grplactcnv  13965  grp1  13969  imasgrp2  13971  mhmlem  13975  mulgnn0gzsum  13989  mulginvcom  14008  mulgnn0ass  14019  mulgmodid  14022  issubg  14034  issubg2m  14050  issubg4m  14054  isnsg2  14064  nsgbi  14065  isnsg3  14068  elnmz  14069  nmzbi  14070  ghmlin  14109  ghmrn  14118  ghmnsgima  14129  conjghm  14137  conjnmz  14140  elcntz  14153  cntzsnval  14155  elcntzsn  14156  cntzi  14161  cntzmhm  14172  gzsumconst  14232  gsum2dfilem2  14271  gsum2d2fi  14273  gsumcom2fi  14274  rngdi  14345  rngdir  14346  srglz  14395  srgisid  14396  srglmhm  14403  ringid  14437  ringinvnz1ne0  14460  ringinvnzdiv  14461  ring1  14470  ringlghm  14472  gsummulc2fi  14475  imasring  14477  dvdsrtr  14516  lringuplu  14611  issubrng  14615  issubrng2  14626  issubrg  14637  issubrg2  14657  rrgeq0i  14680  rrgeq0  14681  unitrrg  14684  domneq0  14689  lmodlema  14736  islmodd  14737  rmodislmodlem  14795  rmodislmod  14796  lssclg  14809  lss1d  14828  rnglidlmcl  14925  quscrng  14978  cnfldexp  15022  gsumfsum  15031  cnfldui  15032  expghmap  15050  zrhval  15060  zrhvalg  15061  znunit  15102  assalem  15111  psrlidmfi  15208  psrridmfi  15209  psrass1fi  15210  txdis1cn  15521  cnmptcom  15541  psmettri2  15571  isxmet2d  15591  xmeteq0  15602  xmettri2  15604  elblps  15633  elbl  15634  blssps  15670  blss  15671  ssblex  15674  blin2  15675  metss2  15741  comet  15742  bdmopn  15747  txmetcnp  15761  blssioo  15796  divcnap  15808  mpomulcn  15809  expcn  15812  cncfval  15815  cncfi  15821  mulc1cncf  15832  cdivcncfap  15847  mulcncf  15851  expcncf  15852  cnopnap  15854  ellimc3apf  15903  cnlimci  15916  limccnpcntop  15918  limccnp2lem  15919  reldvg  15922  eldvap  15925  dvexp  15954  dvexp2  15955  dvrecap  15956  elplyr  15983  elplyd  15984  ply1termlem  15985  plymullem1  15991  plyadd  15994  plymul  15995  plycoeid3  16000  plycolemc  16001  plyco  16002  plycj  16004  dvply1  16008  dvply2g  16009  sin0pilem2  16026  sineq0re  16093  logfac  16143  rpcxpmul2  16163  relogbcxpbap  16218  logbgcd1irr  16220  2irrexpq  16229  2irrexpqap  16231  zprmlogbaplem2  16233  zprmlogbaplem3  16234  zprmlogbap  16235  log2tlbndlog2  16237  log2ublem2  16239  chtqcl  16261  chtqval  16262  ppiqval  16265  dvdsppwf1o  16300  mpodvdsmulf1o  16301  fsumdvdsmul  16302  sgmppw  16303  1sgmprm  16305  chtublem  16312  chtqub  16313  perfect  16318  bcmono  16321  bclbnd  16324  bposlem2  16329  bposlem7  16334  bposlem8  16335  bposlem9  16336  lgsneg  16365  lgsdilem  16368  lgsdir  16376  lgsdilem2  16377  lgsdi  16378  lgsne0  16379  lgsdirnn0  16388  lgsdinn0  16389  gausslemma2dlem4  16405  lgseisenlem2  16412  lgseisenlem3  16413  lgseisenlem4  16414  lgsquadlem1  16418  lgsquadlem2  16419  lgsquad2lem2  16423  2lgs  16445  2sqlem6  16461  2sqlem8  16464  2sqlem9  16465  2sqlem10  16466  wlkeq  16817  wlkl1loop  16821  uspgr2wlkeq  16828  upgr2wlkdc  16840  clwwlknonmpo  16891  eupth2fi  16942  trilpolemclim  17309  trilpolemcl  17310  trilpolemisumle  17311  trilpolemeq1  17313  trilpolemlt1  17314  trilpo  17316  trirec0  17317  qdiff  17322  redcwlpo  17329  nconstwlpolemgt0  17338  nconstwlpo  17340  neapmkv  17342