Theorem oveq1 6059

Description: Equality theorem for operation value. (Contributed by NM, 28-Feb-1995.)

Assertion

Ref	Expression
oveq1	|- ( A = B -> ( A F C ) = ( B F C ) )

Proof of Theorem oveq1

Step	Hyp	Ref	Expression
1		opeq1 3885	. . 3 |- ( A = B -> <. A , C >. = <. B , C >. )
2	1	fveq2d 5676	. 2 |- ( A = B -> ( F ` <. A , C >. ) = ( F ` <. B , C >. ) )
3		df-ov 6055	. 2 |- ( A F C ) = ( F ` <. A , C >. )
4		df-ov 6055	. 2 |- ( B F C ) = ( F ` <. B , C >. )
5	2, 3, 4	3eqtr4g 2292	1 |- ( A = B -> ( A F C ) = ( B F C ) )

Syntax hints:   -> wi 4   = wceq 1398   <.cop 3694   ` cfv 5354  (class class class)co 6052

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 717  ax-5 1496  ax-7 1497  ax-gen 1498  ax-ie1 1542  ax-ie2 1543  ax-8 1553  ax-10 1554  ax-11 1555  ax-i12 1556  ax-bndl 1558  ax-4 1559  ax-17 1575  ax-i9 1579  ax-ial 1583  ax-i5r 1584  ax-ext 2216

This theorem depends on definitions:  df-bi 117  df-3an 1007  df-tru 1401  df-nf 1510  df-sb 1812  df-clab 2221  df-cleq 2227  df-clel 2230  df-nfc 2375  df-rex 2528  df-v 2817  df-un 3217  df-sn 3697  df-pr 3698  df-op 3700  df-uni 3917  df-br 4112  df-iota 5314  df-fv 5362  df-ov 6055

This theorem is referenced by:  oveq12  6061  oveq1i  6062  oveq1d  6067  ovrspc2v  6078  oveqrspc2v  6079  rspceov  6095  fovcld  6160  ovmpos  6179  ov2gf  6180  ovi3  6193  caovclg  6209  caovcomg  6212  caovassg  6215  caovcang  6218  caovcan  6221  caovordig  6222  caovordg  6224  caovord  6228  caovdig  6231  caovdirg  6234  caovimo  6250  suppssov1  6265  off  6281  caofid0r  6296  caofid1  6297  caofdig  6302  suppofss1dcl  6466  suppofss2dcl  6467  omcl  6696  oeicl  6697  omv2  6700  nnm0r  6714  nnacom  6719  nndi  6721  nnmass  6722  nnmsucr  6723  nnmcom  6724  nnaword  6746  nnmord  6752  nnm00  6765  eroveu  6862  th3qlem2  6874  th3q  6876  ecovcom  6878  ecovicom  6879  ecovass  6880  ecoviass  6881  ecovdi  6882  ecovidi  6883  map0g  6924  addcmpblnq  7684  addclnq  7692  mulclnq  7693  mulidnq  7706  recexnq  7707  recmulnqg  7708  ltanqg  7717  ltmnqg  7718  ltexnqq  7725  enq0ref  7750  enq0tr  7751  addcmpblnq0  7760  mulnnnq0  7767  addclnq0  7768  mulclnq0  7769  distrnq0  7776  mulcomnq0  7777  addassnq0  7779  prarloclemlo  7811  prarloclem3  7814  prarloclem5  7817  prarloclemcalc  7819  genipv  7826  genpassl  7841  genpassu  7842  addlocprlemeq  7850  distrlem4prl  7901  distrlem4pru  7902  ltexprlemdisj  7923  ltexprlemloc  7924  ltexprlemrl  7927  ltexprlemru  7929  prplnqu  7937  cauappcvgprlemm  7962  cauappcvgprlemopl  7963  cauappcvgprlemlol  7964  cauappcvgprlemdisj  7968  cauappcvgprlemloc  7969  cauappcvgprlemladdfl  7972  cauappcvgprlemladdru  7973  cauappcvgprlemladdrl  7974  cauappcvgprlem1  7976  cauappcvgprlemlim  7978  cauappcvgpr  7979  caucvgprlemm  7985  caucvgprlemopl  7986  caucvgprlemlol  7987  caucvgprlemdisj  7991  caucvgprlemloc  7992  caucvgprlemladdrl  7995  caucvgprlem1  7996  caucvgpr  7999  caucvgprprlemell  8002  caucvgprprlemml  8011  caucvgprpr  8029  mulcmpblnrlemg  8057  addclsr  8070  mulclsr  8071  0idsr  8084  1idsr  8085  00sr  8086  ltasrg  8087  recexgt0sr  8090  mulgt0sr  8095  mulextsr1  8098  prsrriota  8105  caucvgsrlemgt1  8112  caucvgsrlemoffres  8117  pitonn  8165  peano2nnnn  8170  axaddrcl  8182  axmulrcl  8184  axaddcom  8187  ax1rid  8194  ax0id  8195  axprecex  8197  axcnre  8198  axpre-ltadd  8203  axpre-mulgt0  8204  axpre-mulext  8205  rereceu  8206  peano5nnnn  8209  axcaucvglemcau  8215  axcaucvglemres  8216  mulrid  8273  cnegexlem1  8450  cnegexlem2  8451  cnegex  8453  addcan2  8456  subval  8467  addlsub  8645  apreim  8879  recexap  8929  receuap  8945  divvalap  8950  cju  9237  peano2nn  9251  nn1m1nn  9257  nn1suc  9258  nnsub  9278  fv0p1e1  9354  nnm1nn0  9539  zdiv  9669  zneo  9682  nneoor  9683  zeo  9686  peano5uzti  9689  nn0ind-raph  9698  uzind4s  9925  uzind4s2  9926  qmulz  9958  elpq  9984  cnref1o  9986  nn0ledivnn  10103  xaddnemnf  10193  xaddnepnf  10194  xaddcom  10197  xaddid1  10198  xnn0xadd0  10203  xaddass  10205  xpncan  10207  xleadd1a  10209  xltadd1  10212  xlt2add  10216  xsubge0  10217  xposdif  10218  xlesubadd  10219  xleaddadd  10223  fzsuc2  10417  fzm1  10438  fzoval  10486  exbtwnzlemstep  10611  exbtwnzlemshrink  10612  exbtwnzlemex  10613  exbtwnz  10614  rebtwn2zlemstep  10616  rebtwn2zlemshrink  10617  rebtwn2z  10618  flqlelt  10640  flqbi  10654  fldiv4p1lem1div2  10669  fldiv4lem1div2  10671  modqval  10690  modqadd1  10727  modqmuladd  10732  modqmuladdnn0  10734  modqm1p1mod0  10741  modqmul1  10743  modfzo0difsn  10761  addmodlteq  10764  frec2uzzd  10766  frec2uzsucd  10767  frec2uzrand  10771  frecuzrdgrrn  10774  frec2uzrdg  10775  frecuzrdgrcl  10776  frecuzrdgsuc  10780  frecuzrdgrclt  10781  frecuzrdgg  10782  frecuzrdgdom  10784  frecuzrdgfun  10786  frecuzrdgsuctlem  10789  frecuzrdgsuct  10790  uzsinds  10810  iseqvalcbv  10825  seq3val  10826  seqvalcd  10827  seqf  10830  seq3p1  10831  seqovcd  10833  seqp1cd  10836  seq3fveq2  10841  seqfveq2g  10843  seq3shft2  10847  seqshft2g  10848  monoord  10851  monoord2  10852  seq3split  10854  seqsplitg  10855  seq3caopr3  10857  seqcaopr3g  10858  seq3caopr2  10859  seqcaopr2g  10860  iseqf1olemqval  10866  iseqf1olemqk  10873  seqf1oglem2a  10884  seqf1oglem2  10886  seq3id2  10892  seq3homo  10893  seq3z  10894  seqhomog  10896  seqfeq4g  10897  seq3distr  10898  m1expcl2  10927  mulexp  10944  expadd  10947  expmul  10950  sq0i  10997  qsqeqor  11016  sqoddm1div8  11059  facp1  11096  faclbnd  11107  faclbnd3  11109  bcval  11115  bcn1  11124  bcval5  11129  bcpasc  11132  bccl  11133  hashfz1  11150  omgadd  11170  hashfzo  11191  hashfzp1  11193  hashxp  11195  hashmap  11196  seq3coll  11218  lsw1  11278  ccats1val2  11332  ccatw2s1p2  11338  pfxsuff1eqwrdeq  11395  swrdswrd  11401  ccats1pfxeq  11410  ccatopth  11412  wrdind  11418  wrd2ind  11419  swrdccatin2  11425  pfxccatin12lem2  11427  swrdccat3blem  11435  ccats1pfxeqbi  11438  swrdccatin2d  11440  reuccatpfxs1  11443  shftlem  11505  shftfvalg  11507  shftfibg  11509  shftfval  11510  shftfib  11512  shftfn  11513  shftf  11519  2shfti  11520  shftvalg  11525  shftval4g  11526  cjval  11534  imval  11539  cjexp  11582  cnrecnv  11599  cvg1nlemcau  11673  cvg1nlemres  11674  resqrexlemcalc3  11705  resqrexlemex  11714  rsqrmo  11716  resqrtcl  11718  rersqrtthlem  11719  sqrtsq  11733  absexp  11768  recan  11798  climshft  11993  climcn1  11997  climcn2  11998  subcn2  12000  fsumshft  12134  fisum0diag2  12137  fsumiun  12167  binomlem  12173  binom  12174  bcxmas  12179  isumsplit  12181  arisum2  12189  trireciplem  12190  trirecip  12191  geolim  12201  cvgratnnlemnexp  12214  cvgratnnlemmn  12215  clim2prod  12229  prodfrecap  12236  fprodcl2lem  12295  fprodfac  12305  fprodshft  12308  ef0lem  12350  efval  12351  efne0  12368  efexp  12372  demoivreALT  12464  dvdsval2  12480  p1modz1  12484  dvds0lem  12491  dvds1lem  12492  dvds2lem  12493  dvdsmulc  12509  divconjdvds  12539  odd2np1lem  12562  odd2np1  12563  ltoddhalfle  12583  halfleoddlt  12584  nn0o1gt2  12595  nn0o  12597  divalglemnn  12608  divalglemeunn  12611  divalglemex  12612  divalglemeuneg  12613  flodddiv4  12626  bitsinv1  12652  gcdabs1  12689  gcddiv  12719  dvdssqim  12724  rpmulgcd  12726  bezoutr1  12733  uzwodc  12737  dvdslcm  12770  lcmeq0  12772  lcmdvds  12780  divgcdcoprm0  12802  prmind2  12821  isprm5lem  12842  isprm6  12848  rpexp  12854  sqrt2irr  12863  pw2dvdslemn  12866  pw2dvdseu  12869  oddpwdclemxy  12870  nn0gcdsq  12901  phicl2  12915  phibndlem  12917  hashdvds  12922  crth  12925  phimullem  12926  eulerthlem1  12928  eulerthlemfi  12929  eulerthlemrprm  12930  eulerthlemth  12933  eulerth  12934  hashgcdlem  12939  phisum  12942  odzval  12943  modprm0  12956  nnnn0modprm0  12957  pythagtriplem1  12967  pythagtriplem6  12972  pythagtriplem7  12973  pythagtriplem12  12977  pythagtriplem14  12979  pythagtriplem18  12983  pythagtriplem19  12984  pceulem  12996  pceu  12997  pcval  12998  pczpre  12999  pcdiv  13004  pcqmul  13005  pcqcl  13008  pcexp  13011  pcaddlem  13041  pcadd  13042  pcmpt  13045  pcprod  13048  pcfac  13052  expnprm  13055  prmpwdvds  13057  pockthi  13060  1arithlem2  13066  4sqlem2  13091  4sqlem3  13092  4sqlem11  13103  4sqlem12  13104  4sqlem13m  13105  4sqlem17  13109  4sqlem18  13110  4sqlem19  13111  ballotfilemfc0  13153  ballotfilemfcc  13154  ennnfonelemr  13191  ctinfom  13196  infpn2  13224  ercpbl  13561  mgm1  13600  mgmidmo  13602  ismgmid  13607  mgmlrid  13609  ismgmid2  13610  lidrideqd  13611  lidrididd  13612  mgmidsssn0  13614  grprida  13617  gsumfzval  13621  gsumress  13625  gsumval2  13627  isnsgrp  13636  sgrpass  13638  sgrp1  13641  sgrpidmndm  13650  ismndd  13667  mndinvmod  13675  imasmnd2  13682  mnd1  13685  mnd1id  13686  mhmpropd  13696  insubm  13715  mhmima  13721  gsumvallem2  13723  grppropd  13747  isgrpd2  13751  isgrpd  13753  dfgrp2  13757  grprcan  13767  grpinveu  13768  grpsubval  13776  grplinv  13780  grpinvid2  13783  isgrpinv  13784  grplrinv  13787  grpidinv2  13788  grpidinv  13789  grpidssd  13806  grpinvssd  13807  dfgrp3mlem  13828  dfgrp3m  13829  grplactfval  13831  grp1  13836  imasgrp2  13844  mhmmnd  13850  ghmgrp  13852  mulgnn0gsum  13862  mulgnn0p1  13867  mulgnn0subcl  13869  mulgaddcom  13880  mulginvcom  13881  mulgnn0z  13883  mulgneg2  13890  mulgnnass  13891  mulgnn0ass  13892  mhmmulg  13897  issubg  13907  subgex  13910  issubg2m  13923  issubg4m  13927  isnsg2  13937  nsgbi  13938  isnsg3  13941  elnmz  13942  nmzbi  13943  ghmrn  13991  ghmnsgima  14002  gsumfzconst  14075  rngdi  14101  rngdir  14102  srgrz  14145  srgmulgass  14150  srgpcomp  14151  srgrmhm  14155  ringid  14187  ringinvnzdiv  14211  mulgass2  14219  ring1  14220  ringrghm  14223  imasring  14225  dvdsrmuld  14258  dvdsrmul1  14264  dvdsr01  14266  dvreq1  14304  rhmdvdsr  14337  lringuplu  14358  issubrng  14361  issubrng2  14372  issubrg  14383  issubrg2  14403  isrrg  14425  domneq0  14435  lmodlema  14457  islmodd  14458  lmodvsmmulgdi  14488  rmodislmodlem  14515  rmodislmod  14516  lssclg  14529  lss1d  14548  lspsn  14581  sraval  14602  rnglidlmcl  14645  quscrng  14698  cnfldmulg  14741  cnfldexp  14742  gsumfzfsumlemm  14752  cnfldui  14754  expghmap  14772  mulgghm2  14773  mulgrhm  14774  zrhmulg  14785  zlmval  14792  znunit  14824  cnmptcom  15180  psmettri2  15210  isxmet2d  15230  xmeteq0  15241  xmettri2  15243  metrest  15388  mpomulcn  15448  expcn  15451  cncfval  15454  mulc1cncf  15471  addccncf  15482  mulcncf  15490  expcncf  15491  hovera  15529  hoverb  15530  hoverlt1  15531  hovergt0  15532  ivthdich  15535  limccnp2lem  15558  dvcnp2cntop  15581  dvcoapbr  15589  dvexp  15593  dvrecap  15595  dvef  15609  plyadd  15633  plymul  15634  plycoeid3  15639  plyco  15641  plycjlemc  15642  plycj  15643  plyrecj  15645  dvply1  15647  dvply2g  15648  sincn  15651  coscn  15652  ptolemy  15706  sincosq1eq  15721  rpcxpmul2  15795  logbgcd1irr  15849  logbgcd1irraplemexp  15850  2irrexpq  15858  2irrexpqap  15860  pellexlem3  15864  mpodvdsmulf1o  15875  fsumdvdsmul  15876  sgmppw  15877  sgmmul  15881  perfect  15886  lgslem4  15893  lgsval  15894  lgsfvalg  15895  lgsval2lem  15900  lgsdir2lem4  15921  lgsdir  15925  lgsdilem2  15926  lgsdi  15927  lgsne0  15928  lgsmodeq  15935  lgsdirnn0  15937  lgsdinn0  15938  gausslemma2dlem0i  15947  gausslemma2dlem1a  15948  gausslemma2dlem1f1o  15950  gausslemma2dlem2  15952  gausslemma2dlem3  15953  gausslemma2dlem4  15954  lgseisenlem2  15961  lgsquadlem2  15968  lgsquadlem3  15969  lgsquad  15970  lgsquad2lem2  15972  2lgslem1a  15978  2lgslem1b  15979  2lgslem1c  15980  2lgslem3a  15983  2lgslem3b  15984  2lgslem3c  15985  2lgslem3d  15986  2lgslem3a1  15987  2lgslem3b1  15988  2lgslem3c1  15989  2lgslem3d1  15990  2lgs  15994  2lgsoddprmlem1  15995  2lgsoddprmlem3  16001  2sqlem2  16005  2sqlem6  16010  2sqlem8  16013  2sqlem9  16014  wlklenvm1  16353  wlklenvm1g  16354  wlkl1loop  16370  2wlklem  16388  clwwlknnn  16424  clwwlknp  16429  clwwlkn1  16430  clwwlkn2  16433  clwwlkext2edg  16434  umgr2cwwk2dif  16436  clwwlknon  16441  clwwlk0on0  16443  clwwlknonex2lem1  16449  clwwlknonex2lem2  16450  clwwlknonex2  16451  qdencn  16824  isomninn  16832  trirec0  16845  iswomninn  16852  ismkvnn  16855  gfsumval  16879  gsumgfsumlem  16882