Theorem oveq1 6024

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 3862	. . 3 |- ( A = B -> <. A , C >. = <. B , C >. )
2	1	fveq2d 5643	. 2 |- ( A = B -> ( F ` <. A , C >. ) = ( F ` <. B , C >. ) )
3		df-ov 6020	. 2 |- ( A F C ) = ( F ` <. A , C >. )
4		df-ov 6020	. 2 |- ( B F C ) = ( F ` <. B , C >. )
5	2, 3, 4	3eqtr4g 2289	1 |- ( A = B -> ( A F C ) = ( B F C ) )

Syntax hints:   -> wi 4   = wceq 1397   <.cop 3672   ` cfv 5326  (class class class)co 6017

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 716  ax-5 1495  ax-7 1496  ax-gen 1497  ax-ie1 1541  ax-ie2 1542  ax-8 1552  ax-10 1553  ax-11 1554  ax-i12 1555  ax-bndl 1557  ax-4 1558  ax-17 1574  ax-i9 1578  ax-ial 1582  ax-i5r 1583  ax-ext 2213

This theorem depends on definitions:  df-bi 117  df-3an 1006  df-tru 1400  df-nf 1509  df-sb 1811  df-clab 2218  df-cleq 2224  df-clel 2227  df-nfc 2363  df-rex 2516  df-v 2804  df-un 3204  df-sn 3675  df-pr 3676  df-op 3678  df-uni 3894  df-br 4089  df-iota 5286  df-fv 5334  df-ov 6020

This theorem is referenced by:  oveq12  6026  oveq1i  6027  oveq1d  6032  ovrspc2v  6043  oveqrspc2v  6044  rspceov  6060  fovcld  6125  ovmpos  6144  ov2gf  6145  ovi3  6158  caovclg  6174  caovcomg  6177  caovassg  6180  caovcang  6183  caovcan  6186  caovordig  6187  caovordg  6189  caovord  6193  caovdig  6196  caovdirg  6199  caovimo  6215  suppssov1  6231  off  6247  caofid0r  6262  caofid1  6263  caofdig  6268  omcl  6628  oeicl  6629  omv2  6632  nnm0r  6646  nnacom  6651  nndi  6653  nnmass  6654  nnmsucr  6655  nnmcom  6656  nnaword  6678  nnmord  6684  nnm00  6697  eroveu  6794  th3qlem2  6806  th3q  6808  ecovcom  6810  ecovicom  6811  ecovass  6812  ecoviass  6813  ecovdi  6814  ecovidi  6815  map0g  6856  addcmpblnq  7586  addclnq  7594  mulclnq  7595  mulidnq  7608  recexnq  7609  recmulnqg  7610  ltanqg  7619  ltmnqg  7620  ltexnqq  7627  enq0ref  7652  enq0tr  7653  addcmpblnq0  7662  mulnnnq0  7669  addclnq0  7670  mulclnq0  7671  distrnq0  7678  mulcomnq0  7679  addassnq0  7681  prarloclemlo  7713  prarloclem3  7716  prarloclem5  7719  prarloclemcalc  7721  genipv  7728  genpassl  7743  genpassu  7744  addlocprlemeq  7752  distrlem4prl  7803  distrlem4pru  7804  ltexprlemdisj  7825  ltexprlemloc  7826  ltexprlemrl  7829  ltexprlemru  7831  prplnqu  7839  cauappcvgprlemm  7864  cauappcvgprlemopl  7865  cauappcvgprlemlol  7866  cauappcvgprlemdisj  7870  cauappcvgprlemloc  7871  cauappcvgprlemladdfl  7874  cauappcvgprlemladdru  7875  cauappcvgprlemladdrl  7876  cauappcvgprlem1  7878  cauappcvgprlemlim  7880  cauappcvgpr  7881  caucvgprlemm  7887  caucvgprlemopl  7888  caucvgprlemlol  7889  caucvgprlemdisj  7893  caucvgprlemloc  7894  caucvgprlemladdrl  7897  caucvgprlem1  7898  caucvgpr  7901  caucvgprprlemell  7904  caucvgprprlemml  7913  caucvgprpr  7931  mulcmpblnrlemg  7959  addclsr  7972  mulclsr  7973  0idsr  7986  1idsr  7987  00sr  7988  ltasrg  7989  recexgt0sr  7992  mulgt0sr  7997  mulextsr1  8000  prsrriota  8007  caucvgsrlemgt1  8014  caucvgsrlemoffres  8019  pitonn  8067  peano2nnnn  8072  axaddrcl  8084  axmulrcl  8086  axaddcom  8089  ax1rid  8096  ax0id  8097  axprecex  8099  axcnre  8100  axpre-ltadd  8105  axpre-mulgt0  8106  axpre-mulext  8107  rereceu  8108  peano5nnnn  8111  axcaucvglemcau  8117  axcaucvglemres  8118  mulrid  8175  cnegexlem1  8353  cnegexlem2  8354  cnegex  8356  addcan2  8359  subval  8370  addlsub  8548  apreim  8782  recexap  8832  receuap  8848  divvalap  8853  cju  9140  peano2nn  9154  nn1m1nn  9160  nn1suc  9161  nnsub  9181  fv0p1e1  9257  nnm1nn0  9442  zdiv  9567  zneo  9580  nneoor  9581  zeo  9584  peano5uzti  9587  nn0ind-raph  9596  uzind4s  9823  uzind4s2  9824  qmulz  9856  elpq  9882  cnref1o  9884  nn0ledivnn  10001  xaddnemnf  10091  xaddnepnf  10092  xaddcom  10095  xaddid1  10096  xnn0xadd0  10101  xaddass  10103  xpncan  10105  xleadd1a  10107  xltadd1  10110  xlt2add  10114  xsubge0  10115  xposdif  10116  xlesubadd  10117  xleaddadd  10121  fzsuc2  10313  fzm1  10334  fzoval  10382  exbtwnzlemstep  10506  exbtwnzlemshrink  10507  exbtwnzlemex  10508  exbtwnz  10509  rebtwn2zlemstep  10511  rebtwn2zlemshrink  10512  rebtwn2z  10513  flqlelt  10535  flqbi  10549  fldiv4p1lem1div2  10564  fldiv4lem1div2  10566  modqval  10585  modqadd1  10622  modqmuladd  10627  modqmuladdnn0  10629  modqm1p1mod0  10636  modqmul1  10638  modfzo0difsn  10656  addmodlteq  10659  frec2uzzd  10661  frec2uzsucd  10662  frec2uzrand  10666  frecuzrdgrrn  10669  frec2uzrdg  10670  frecuzrdgrcl  10671  frecuzrdgsuc  10675  frecuzrdgrclt  10676  frecuzrdgg  10677  frecuzrdgdom  10679  frecuzrdgfun  10681  frecuzrdgsuctlem  10684  frecuzrdgsuct  10685  uzsinds  10705  iseqvalcbv  10720  seq3val  10721  seqvalcd  10722  seqf  10725  seq3p1  10726  seqovcd  10728  seqp1cd  10731  seq3fveq2  10736  seqfveq2g  10738  seq3shft2  10742  seqshft2g  10743  monoord  10746  monoord2  10747  seq3split  10749  seqsplitg  10750  seq3caopr3  10752  seqcaopr3g  10753  seq3caopr2  10754  seqcaopr2g  10755  iseqf1olemqval  10761  iseqf1olemqk  10768  seqf1oglem2a  10779  seqf1oglem2  10781  seq3id2  10787  seq3homo  10788  seq3z  10789  seqhomog  10791  seqfeq4g  10792  seq3distr  10793  m1expcl2  10822  mulexp  10839  expadd  10842  expmul  10845  sq0i  10892  qsqeqor  10911  sqoddm1div8  10954  facp1  10991  faclbnd  11002  faclbnd3  11004  bcval  11010  bcn1  11019  bcval5  11024  bcpasc  11027  bccl  11028  hashfz1  11044  omgadd  11064  hashfzo  11085  hashfzp1  11087  hashxp  11089  seq3coll  11105  lsw1  11162  ccats1val2  11216  ccatw2s1p2  11222  pfxsuff1eqwrdeq  11279  swrdswrd  11285  ccats1pfxeq  11294  ccatopth  11296  wrdind  11302  wrd2ind  11303  swrdccatin2  11309  pfxccatin12lem2  11311  swrdccat3blem  11319  ccats1pfxeqbi  11322  swrdccatin2d  11324  reuccatpfxs1  11327  shftlem  11376  shftfvalg  11378  shftfibg  11380  shftfval  11381  shftfib  11383  shftfn  11384  shftf  11390  2shfti  11391  shftvalg  11396  shftval4g  11397  cjval  11405  imval  11410  cjexp  11453  cnrecnv  11470  cvg1nlemcau  11544  cvg1nlemres  11545  resqrexlemcalc3  11576  resqrexlemex  11585  rsqrmo  11587  resqrtcl  11589  rersqrtthlem  11590  sqrtsq  11604  absexp  11639  recan  11669  climshft  11864  climcn1  11868  climcn2  11869  subcn2  11871  fsumshft  12004  fisum0diag2  12007  fsumiun  12037  binomlem  12043  binom  12044  bcxmas  12049  isumsplit  12051  arisum2  12059  trireciplem  12060  trirecip  12061  geolim  12071  cvgratnnlemnexp  12084  cvgratnnlemmn  12085  clim2prod  12099  prodfrecap  12106  fprodcl2lem  12165  fprodfac  12175  fprodshft  12178  ef0lem  12220  efval  12221  efne0  12238  efexp  12242  demoivreALT  12334  dvdsval2  12350  p1modz1  12354  dvds0lem  12361  dvds1lem  12362  dvds2lem  12363  dvdsmulc  12379  divconjdvds  12409  odd2np1lem  12432  odd2np1  12433  ltoddhalfle  12453  halfleoddlt  12454  nn0o1gt2  12465  nn0o  12467  divalglemnn  12478  divalglemeunn  12481  divalglemex  12482  divalglemeuneg  12483  flodddiv4  12496  bitsinv1  12522  gcdabs1  12559  gcddiv  12589  dvdssqim  12594  rpmulgcd  12596  bezoutr1  12603  uzwodc  12607  dvdslcm  12640  lcmeq0  12642  lcmdvds  12650  divgcdcoprm0  12672  prmind2  12691  isprm5lem  12712  isprm6  12718  rpexp  12724  sqrt2irr  12733  pw2dvdslemn  12736  pw2dvdseu  12739  oddpwdclemxy  12740  nn0gcdsq  12771  phicl2  12785  phibndlem  12787  hashdvds  12792  crth  12795  phimullem  12796  eulerthlem1  12798  eulerthlemfi  12799  eulerthlemrprm  12800  eulerthlemth  12803  eulerth  12804  hashgcdlem  12809  phisum  12812  odzval  12813  modprm0  12826  nnnn0modprm0  12827  pythagtriplem1  12837  pythagtriplem6  12842  pythagtriplem7  12843  pythagtriplem12  12847  pythagtriplem14  12849  pythagtriplem18  12853  pythagtriplem19  12854  pceulem  12866  pceu  12867  pcval  12868  pczpre  12869  pcdiv  12874  pcqmul  12875  pcqcl  12878  pcexp  12881  pcaddlem  12911  pcadd  12912  pcmpt  12915  pcprod  12918  pcfac  12922  expnprm  12925  prmpwdvds  12927  pockthi  12930  1arithlem2  12936  4sqlem2  12961  4sqlem3  12962  4sqlem11  12973  4sqlem12  12974  4sqlem13m  12975  4sqlem17  12979  4sqlem18  12980  4sqlem19  12981  ennnfonelemr  13043  ctinfom  13048  infpn2  13076  ercpbl  13413  mgm1  13452  mgmidmo  13454  ismgmid  13459  mgmlrid  13461  ismgmid2  13462  lidrideqd  13463  lidrididd  13464  mgmidsssn0  13466  grprida  13469  gsumfzval  13473  gsumress  13477  gsumval2  13479  isnsgrp  13488  sgrpass  13490  sgrp1  13493  sgrpidmndm  13502  ismndd  13519  mndinvmod  13527  imasmnd2  13534  mnd1  13537  mnd1id  13538  mhmpropd  13548  insubm  13567  mhmima  13573  gsumvallem2  13575  grppropd  13599  isgrpd2  13603  isgrpd  13605  dfgrp2  13609  grprcan  13619  grpinveu  13620  grpsubval  13628  grplinv  13632  grpinvid2  13635  isgrpinv  13636  grplrinv  13639  grpidinv2  13640  grpidinv  13641  grpidssd  13658  grpinvssd  13659  dfgrp3mlem  13680  dfgrp3m  13681  grplactfval  13683  grp1  13688  imasgrp2  13696  mhmmnd  13702  ghmgrp  13704  mulgnn0gsum  13714  mulgnn0p1  13719  mulgnn0subcl  13721  mulgaddcom  13732  mulginvcom  13733  mulgnn0z  13735  mulgneg2  13742  mulgnnass  13743  mulgnn0ass  13744  mhmmulg  13749  issubg  13759  subgex  13762  issubg2m  13775  issubg4m  13779  isnsg2  13789  nsgbi  13790  isnsg3  13793  elnmz  13794  nmzbi  13795  ghmrn  13843  ghmnsgima  13854  gsumfzconst  13927  rngdi  13952  rngdir  13953  srgrz  13996  srgmulgass  14001  srgpcomp  14002  srgrmhm  14006  ringid  14038  ringinvnzdiv  14062  mulgass2  14070  ring1  14071  ringrghm  14074  imasring  14076  dvdsrmuld  14109  dvdsrmul1  14115  dvdsr01  14117  dvreq1  14155  rhmdvdsr  14188  lringuplu  14209  issubrng  14212  issubrng2  14223  issubrg  14234  issubrg2  14254  isrrg  14276  domneq0  14285  lmodlema  14305  islmodd  14306  lmodvsmmulgdi  14336  rmodislmodlem  14363  rmodislmod  14364  lssclg  14377  lss1d  14396  lspsn  14429  sraval  14450  rnglidlmcl  14493  quscrng  14546  cnfldmulg  14589  cnfldexp  14590  gsumfzfsumlemm  14600  cnfldui  14602  expghmap  14620  mulgghm2  14621  mulgrhm  14622  zrhmulg  14633  zlmval  14640  znunit  14672  cnmptcom  15021  psmettri2  15051  isxmet2d  15071  xmeteq0  15082  xmettri2  15084  metrest  15229  mpomulcn  15289  expcn  15292  cncfval  15295  mulc1cncf  15312  addccncf  15323  mulcncf  15331  expcncf  15332  hovera  15370  hoverb  15371  hoverlt1  15372  hovergt0  15373  ivthdich  15376  limccnp2lem  15399  dvcnp2cntop  15422  dvcoapbr  15430  dvexp  15434  dvrecap  15436  dvef  15450  plyadd  15474  plymul  15475  plycoeid3  15480  plyco  15482  plycjlemc  15483  plycj  15484  plyrecj  15486  dvply1  15488  dvply2g  15489  sincn  15492  coscn  15493  ptolemy  15547  sincosq1eq  15562  rpcxpmul2  15636  logbgcd1irr  15690  logbgcd1irraplemexp  15691  2irrexpq  15699  2irrexpqap  15701  mpodvdsmulf1o  15713  fsumdvdsmul  15714  sgmppw  15715  sgmmul  15719  perfect  15724  lgslem4  15731  lgsval  15732  lgsfvalg  15733  lgsval2lem  15738  lgsdir2lem4  15759  lgsdir  15763  lgsdilem2  15764  lgsdi  15765  lgsne0  15766  lgsmodeq  15773  lgsdirnn0  15775  lgsdinn0  15776  gausslemma2dlem0i  15785  gausslemma2dlem1a  15786  gausslemma2dlem1f1o  15788  gausslemma2dlem2  15790  gausslemma2dlem3  15791  gausslemma2dlem4  15792  lgseisenlem2  15799  lgsquadlem2  15806  lgsquadlem3  15807  lgsquad  15808  lgsquad2lem2  15810  2lgslem1a  15816  2lgslem1b  15817  2lgslem1c  15818  2lgslem3a  15821  2lgslem3b  15822  2lgslem3c  15823  2lgslem3d  15824  2lgslem3a1  15825  2lgslem3b1  15826  2lgslem3c1  15827  2lgslem3d1  15828  2lgs  15832  2lgsoddprmlem1  15833  2lgsoddprmlem3  15839  2sqlem2  15843  2sqlem6  15848  2sqlem8  15851  2sqlem9  15852  wlklenvm1  16191  wlklenvm1g  16192  wlkl1loop  16208  2wlklem  16226  clwwlknnn  16262  clwwlknp  16267  clwwlkn1  16268  clwwlkn2  16271  clwwlkext2edg  16272  umgr2cwwk2dif  16274  clwwlknon  16279  clwwlk0on0  16281  clwwlknonex2lem1  16287  clwwlknonex2lem2  16288  clwwlknonex2  16289  qdencn  16631  isomninn  16635  trirec0  16648  iswomninn  16654  ismkvnn  16657  gfsumval  16680  gsumgfsumlem  16683