Theorem oveq1 5926

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 3805	. . 3 |- ( A = B -> <. A , C >. = <. B , C >. )
2	1	fveq2d 5559	. 2 |- ( A = B -> ( F ` <. A , C >. ) = ( F ` <. B , C >. ) )
3		df-ov 5922	. 2 |- ( A F C ) = ( F ` <. A , C >. )
4		df-ov 5922	. 2 |- ( B F C ) = ( F ` <. B , C >. )
5	2, 3, 4	3eqtr4g 2251	1 |- ( A = B -> ( A F C ) = ( B F C ) )

Syntax hints:   -> wi 4   = wceq 1364   <.cop 3622   ` cfv 5255  (class class class)co 5919

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 710  ax-5 1458  ax-7 1459  ax-gen 1460  ax-ie1 1504  ax-ie2 1505  ax-8 1515  ax-10 1516  ax-11 1517  ax-i12 1518  ax-bndl 1520  ax-4 1521  ax-17 1537  ax-i9 1541  ax-ial 1545  ax-i5r 1546  ax-ext 2175

This theorem depends on definitions:  df-bi 117  df-3an 982  df-tru 1367  df-nf 1472  df-sb 1774  df-clab 2180  df-cleq 2186  df-clel 2189  df-nfc 2325  df-rex 2478  df-v 2762  df-un 3158  df-sn 3625  df-pr 3626  df-op 3628  df-uni 3837  df-br 4031  df-iota 5216  df-fv 5263  df-ov 5922

This theorem is referenced by:  oveq12  5928  oveq1i  5929  oveq1d  5934  ovrspc2v  5945  oveqrspc2v  5946  rspceov  5961  fovcld  6024  ovmpos  6043  ov2gf  6044  ovi3  6057  caovclg  6073  caovcomg  6076  caovassg  6079  caovcang  6082  caovcan  6085  caovordig  6086  caovordg  6088  caovord  6092  caovdig  6095  caovdirg  6098  caovimo  6114  suppssov1  6129  off  6145  caofdig  6161  omcl  6516  oeicl  6517  omv2  6520  nnm0r  6534  nnacom  6539  nndi  6541  nnmass  6542  nnmsucr  6543  nnmcom  6544  nnaword  6566  nnmord  6572  nnm00  6585  eroveu  6682  th3qlem2  6694  th3q  6696  ecovcom  6698  ecovicom  6699  ecovass  6700  ecoviass  6701  ecovdi  6702  ecovidi  6703  map0g  6744  addcmpblnq  7429  addclnq  7437  mulclnq  7438  mulidnq  7451  recexnq  7452  recmulnqg  7453  ltanqg  7462  ltmnqg  7463  ltexnqq  7470  enq0ref  7495  enq0tr  7496  addcmpblnq0  7505  mulnnnq0  7512  addclnq0  7513  mulclnq0  7514  distrnq0  7521  mulcomnq0  7522  addassnq0  7524  prarloclemlo  7556  prarloclem3  7559  prarloclem5  7562  prarloclemcalc  7564  genipv  7571  genpassl  7586  genpassu  7587  addlocprlemeq  7595  distrlem4prl  7646  distrlem4pru  7647  ltexprlemdisj  7668  ltexprlemloc  7669  ltexprlemrl  7672  ltexprlemru  7674  prplnqu  7682  cauappcvgprlemm  7707  cauappcvgprlemopl  7708  cauappcvgprlemlol  7709  cauappcvgprlemdisj  7713  cauappcvgprlemloc  7714  cauappcvgprlemladdfl  7717  cauappcvgprlemladdru  7718  cauappcvgprlemladdrl  7719  cauappcvgprlem1  7721  cauappcvgprlemlim  7723  cauappcvgpr  7724  caucvgprlemm  7730  caucvgprlemopl  7731  caucvgprlemlol  7732  caucvgprlemdisj  7736  caucvgprlemloc  7737  caucvgprlemladdrl  7740  caucvgprlem1  7741  caucvgpr  7744  caucvgprprlemell  7747  caucvgprprlemml  7756  caucvgprpr  7774  mulcmpblnrlemg  7802  addclsr  7815  mulclsr  7816  0idsr  7829  1idsr  7830  00sr  7831  ltasrg  7832  recexgt0sr  7835  mulgt0sr  7840  mulextsr1  7843  prsrriota  7850  caucvgsrlemgt1  7857  caucvgsrlemoffres  7862  pitonn  7910  peano2nnnn  7915  axaddrcl  7927  axmulrcl  7929  axaddcom  7932  ax1rid  7939  ax0id  7940  axprecex  7942  axcnre  7943  axpre-ltadd  7948  axpre-mulgt0  7949  axpre-mulext  7950  rereceu  7951  peano5nnnn  7954  axcaucvglemcau  7960  axcaucvglemres  7961  mulrid  8018  cnegexlem1  8196  cnegexlem2  8197  cnegex  8199  addcan2  8202  subval  8213  addlsub  8391  apreim  8624  recexap  8674  receuap  8690  divvalap  8695  cju  8982  peano2nn  8996  nn1m1nn  9002  nn1suc  9003  nnsub  9023  fv0p1e1  9099  nnm1nn0  9284  zdiv  9408  zneo  9421  nneoor  9422  zeo  9425  peano5uzti  9428  nn0ind-raph  9437  uzind4s  9658  uzind4s2  9659  qmulz  9691  elpq  9717  cnref1o  9719  nn0ledivnn  9836  xaddnemnf  9926  xaddnepnf  9927  xaddcom  9930  xaddid1  9931  xnn0xadd0  9936  xaddass  9938  xpncan  9940  xleadd1a  9942  xltadd1  9945  xlt2add  9949  xsubge0  9950  xposdif  9951  xlesubadd  9952  xleaddadd  9956  fzsuc2  10148  fzm1  10169  fzoval  10217  exbtwnzlemstep  10319  exbtwnzlemshrink  10320  exbtwnzlemex  10321  exbtwnz  10322  rebtwn2zlemstep  10324  rebtwn2zlemshrink  10325  rebtwn2z  10326  flqlelt  10348  flqbi  10362  fldiv4p1lem1div2  10377  fldiv4lem1div2  10379  modqval  10398  modqadd1  10435  modqmuladd  10440  modqmuladdnn0  10442  modqm1p1mod0  10449  modqmul1  10451  modfzo0difsn  10469  addmodlteq  10472  frec2uzzd  10474  frec2uzsucd  10475  frec2uzrand  10479  frecuzrdgrrn  10482  frec2uzrdg  10483  frecuzrdgrcl  10484  frecuzrdgsuc  10488  frecuzrdgrclt  10489  frecuzrdgg  10490  frecuzrdgdom  10492  frecuzrdgfun  10494  frecuzrdgsuctlem  10497  frecuzrdgsuct  10498  uzsinds  10518  iseqvalcbv  10533  seq3val  10534  seqvalcd  10535  seqf  10538  seq3p1  10539  seqovcd  10541  seqp1cd  10544  seq3fveq2  10549  seqfveq2g  10551  seq3shft2  10555  seqshft2g  10556  monoord  10559  monoord2  10560  seq3split  10562  seqsplitg  10563  seq3caopr3  10565  seqcaopr3g  10566  seq3caopr2  10567  seqcaopr2g  10568  iseqf1olemqval  10574  iseqf1olemqk  10581  seqf1oglem2a  10592  seqf1oglem2  10594  seq3id2  10600  seq3homo  10601  seq3z  10602  seqhomog  10604  seqfeq4g  10605  seq3distr  10606  m1expcl2  10635  mulexp  10652  expadd  10655  expmul  10658  sq0i  10705  qsqeqor  10724  sqoddm1div8  10767  facp1  10804  faclbnd  10815  faclbnd3  10817  bcval  10823  bcn1  10832  bcval5  10837  bcpasc  10840  bccl  10841  hashfz1  10857  omgadd  10876  hashfzo  10896  hashfzp1  10898  hashxp  10900  seq3coll  10916  shftlem  10963  shftfvalg  10965  shftfibg  10967  shftfval  10968  shftfib  10970  shftfn  10971  shftf  10977  2shfti  10978  shftvalg  10983  shftval4g  10984  cjval  10992  imval  10997  cjexp  11040  cnrecnv  11057  cvg1nlemcau  11131  cvg1nlemres  11132  resqrexlemcalc3  11163  resqrexlemex  11172  rsqrmo  11174  resqrtcl  11176  rersqrtthlem  11177  sqrtsq  11191  absexp  11226  recan  11256  climshft  11450  climcn1  11454  climcn2  11455  subcn2  11457  fsumshft  11590  fisum0diag2  11593  fsumiun  11623  binomlem  11629  binom  11630  bcxmas  11635  isumsplit  11637  arisum2  11645  trireciplem  11646  trirecip  11647  geolim  11657  cvgratnnlemnexp  11670  cvgratnnlemmn  11671  clim2prod  11685  prodfrecap  11692  fprodcl2lem  11751  fprodfac  11761  fprodshft  11764  ef0lem  11806  efval  11807  efne0  11824  efexp  11828  demoivreALT  11920  dvdsval2  11936  p1modz1  11940  dvds0lem  11947  dvds1lem  11948  dvds2lem  11949  dvdsmulc  11965  divconjdvds  11994  odd2np1lem  12016  odd2np1  12017  ltoddhalfle  12037  halfleoddlt  12038  nn0o1gt2  12049  nn0o  12051  divalglemnn  12062  divalglemeunn  12065  divalglemex  12066  divalglemeuneg  12067  flodddiv4  12078  gcdabs1  12129  gcddiv  12159  dvdssqim  12164  rpmulgcd  12166  bezoutr1  12173  uzwodc  12177  dvdslcm  12210  lcmeq0  12212  lcmdvds  12220  divgcdcoprm0  12242  prmind2  12261  isprm5lem  12282  isprm6  12288  rpexp  12294  sqrt2irr  12303  pw2dvdslemn  12306  pw2dvdseu  12309  oddpwdclemxy  12310  nn0gcdsq  12341  phicl2  12355  phibndlem  12357  hashdvds  12362  crth  12365  phimullem  12366  eulerthlem1  12368  eulerthlemfi  12369  eulerthlemrprm  12370  eulerthlemth  12373  eulerth  12374  hashgcdlem  12379  phisum  12381  odzval  12382  modprm0  12395  nnnn0modprm0  12396  pythagtriplem1  12406  pythagtriplem6  12411  pythagtriplem7  12412  pythagtriplem12  12416  pythagtriplem14  12418  pythagtriplem18  12422  pythagtriplem19  12423  pceulem  12435  pceu  12436  pcval  12437  pczpre  12438  pcdiv  12443  pcqmul  12444  pcqcl  12447  pcexp  12450  pcaddlem  12480  pcadd  12481  pcmpt  12484  pcprod  12487  pcfac  12491  expnprm  12494  prmpwdvds  12496  pockthi  12499  1arithlem2  12505  4sqlem2  12530  4sqlem3  12531  4sqlem11  12542  4sqlem12  12543  4sqlem13m  12544  4sqlem17  12548  4sqlem18  12549  4sqlem19  12550  ennnfonelemr  12583  ctinfom  12588  infpn2  12616  ercpbl  12917  mgm1  12956  mgmidmo  12958  ismgmid  12963  mgmlrid  12965  ismgmid2  12966  lidrideqd  12967  lidrididd  12968  mgmidsssn0  12970  grprida  12973  gsumfzval  12977  gsumress  12981  gsumval2  12983  isnsgrp  12992  sgrpass  12994  sgrp1  12997  sgrpidmndm  13004  ismndd  13021  mndinvmod  13029  mnd1  13030  mnd1id  13031  mhmpropd  13041  insubm  13060  mhmima  13066  gsumvallem2  13068  grppropd  13092  isgrpd2  13096  isgrpd  13098  dfgrp2  13102  grprcan  13112  grpinveu  13113  grpsubval  13121  grplinv  13125  grpinvid2  13128  isgrpinv  13129  grplrinv  13132  grpidinv2  13133  grpidinv  13134  grpidssd  13151  grpinvssd  13152  dfgrp3mlem  13173  dfgrp3m  13174  grplactfval  13176  grp1  13181  imasgrp2  13183  mhmmnd  13189  ghmgrp  13191  mulgnn0gsum  13201  mulgnn0p1  13206  mulgnn0subcl  13208  mulgaddcom  13219  mulginvcom  13220  mulgnn0z  13222  mulgneg2  13229  mulgnnass  13230  mulgnn0ass  13231  mhmmulg  13236  issubg  13246  subgex  13249  issubg2m  13262  issubg4m  13266  isnsg2  13276  nsgbi  13277  isnsg3  13280  elnmz  13281  nmzbi  13282  ghmrn  13330  ghmnsgima  13341  gsumfzconst  13414  rngdi  13439  rngdir  13440  srgrz  13483  srgmulgass  13488  srgpcomp  13489  srgrmhm  13493  ringid  13525  ringinvnzdiv  13549  mulgass2  13557  ring1  13558  ringrghm  13561  imasring  13563  dvdsrmuld  13595  dvdsrmul1  13601  dvdsr01  13603  dvreq1  13641  rhmdvdsr  13674  lringuplu  13695  issubrng  13698  issubrng2  13709  issubrg  13720  issubrg2  13740  isrrg  13762  domneq0  13771  lmodlema  13791  islmodd  13792  lmodvsmmulgdi  13822  rmodislmodlem  13849  rmodislmod  13850  lssclg  13863  lss1d  13882  lspsn  13915  sraval  13936  rnglidlmcl  13979  quscrng  14032  cnfldmulg  14075  cnfldexp  14076  gsumfzfsumlemm  14086  cnfldui  14088  expghmap  14106  mulgghm2  14107  mulgrhm  14108  zrhmulg  14119  zlmval  14126  znunit  14158  cnmptcom  14477  psmettri2  14507  isxmet2d  14527  xmeteq0  14538  xmettri2  14540  metrest  14685  mpomulcn  14745  expcn  14748  cncfval  14751  mulc1cncf  14768  addccncf  14779  mulcncf  14787  expcncf  14788  hovera  14826  hoverb  14827  hoverlt1  14828  hovergt0  14829  ivthdich  14832  limccnp2lem  14855  dvcnp2cntop  14878  dvcoapbr  14886  dvexp  14890  dvrecap  14892  dvef  14906  plyadd  14930  plymul  14931  plyco  14937  plycjlemc  14938  plycj  14939  plyrecj  14941  dvply1  14943  sincn  14945  coscn  14946  ptolemy  15000  sincosq1eq  15015  logbgcd1irr  15140  logbgcd1irraplemexp  15141  2irrexpq  15149  2irrexpqap  15151  lgslem4  15160  lgsval  15161  lgsfvalg  15162  lgsval2lem  15167  lgsdir2lem4  15188  lgsdir  15192  lgsdilem2  15193  lgsdi  15194  lgsne0  15195  lgsmodeq  15202  lgsdirnn0  15204  lgsdinn0  15205  gausslemma2dlem0i  15214  gausslemma2dlem1a  15215  gausslemma2dlem1f1o  15217  gausslemma2dlem2  15219  gausslemma2dlem3  15220  gausslemma2dlem4  15221  lgseisenlem2  15228  lgsquadlem2  15235  lgsquadlem3  15236  lgsquad  15237  lgsquad2lem2  15239  2lgslem1a  15245  2lgslem1b  15246  2lgslem1c  15247  2lgslem3a  15250  2lgslem3b  15251  2lgslem3c  15252  2lgslem3d  15253  2lgslem3a1  15254  2lgslem3b1  15255  2lgslem3c1  15256  2lgslem3d1  15257  2lgs  15261  2lgsoddprmlem1  15262  2lgsoddprmlem3  15268  2sqlem2  15272  2sqlem6  15277  2sqlem8  15280  2sqlem9  15281  qdencn  15587  isomninn  15591  trirec0  15604  iswomninn  15610  ismkvnn  15613