Theorem oveq1 5932

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 3809	. . 3 |- ( A = B -> <. A , C >. = <. B , C >. )
2	1	fveq2d 5565	. 2 |- ( A = B -> ( F ` <. A , C >. ) = ( F ` <. B , C >. ) )
3		df-ov 5928	. 2 |- ( A F C ) = ( F ` <. A , C >. )
4		df-ov 5928	. 2 |- ( B F C ) = ( F ` <. B , C >. )
5	2, 3, 4	3eqtr4g 2254	1 |- ( A = B -> ( A F C ) = ( B F C ) )

Syntax hints:   -> wi 4   = wceq 1364   <.cop 3626   ` cfv 5259  (class class class)co 5925

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 1461  ax-7 1462  ax-gen 1463  ax-ie1 1507  ax-ie2 1508  ax-8 1518  ax-10 1519  ax-11 1520  ax-i12 1521  ax-bndl 1523  ax-4 1524  ax-17 1540  ax-i9 1544  ax-ial 1548  ax-i5r 1549  ax-ext 2178

This theorem depends on definitions:  df-bi 117  df-3an 982  df-tru 1367  df-nf 1475  df-sb 1777  df-clab 2183  df-cleq 2189  df-clel 2192  df-nfc 2328  df-rex 2481  df-v 2765  df-un 3161  df-sn 3629  df-pr 3630  df-op 3632  df-uni 3841  df-br 4035  df-iota 5220  df-fv 5267  df-ov 5928

This theorem is referenced by:  oveq12  5934  oveq1i  5935  oveq1d  5940  ovrspc2v  5951  oveqrspc2v  5952  rspceov  5968  fovcld  6031  ovmpos  6050  ov2gf  6051  ovi3  6064  caovclg  6080  caovcomg  6083  caovassg  6086  caovcang  6089  caovcan  6092  caovordig  6093  caovordg  6095  caovord  6099  caovdig  6102  caovdirg  6105  caovimo  6121  suppssov1  6136  off  6152  caofid0r  6167  caofid1  6168  caofdig  6173  omcl  6528  oeicl  6529  omv2  6532  nnm0r  6546  nnacom  6551  nndi  6553  nnmass  6554  nnmsucr  6555  nnmcom  6556  nnaword  6578  nnmord  6584  nnm00  6597  eroveu  6694  th3qlem2  6706  th3q  6708  ecovcom  6710  ecovicom  6711  ecovass  6712  ecoviass  6713  ecovdi  6714  ecovidi  6715  map0g  6756  addcmpblnq  7451  addclnq  7459  mulclnq  7460  mulidnq  7473  recexnq  7474  recmulnqg  7475  ltanqg  7484  ltmnqg  7485  ltexnqq  7492  enq0ref  7517  enq0tr  7518  addcmpblnq0  7527  mulnnnq0  7534  addclnq0  7535  mulclnq0  7536  distrnq0  7543  mulcomnq0  7544  addassnq0  7546  prarloclemlo  7578  prarloclem3  7581  prarloclem5  7584  prarloclemcalc  7586  genipv  7593  genpassl  7608  genpassu  7609  addlocprlemeq  7617  distrlem4prl  7668  distrlem4pru  7669  ltexprlemdisj  7690  ltexprlemloc  7691  ltexprlemrl  7694  ltexprlemru  7696  prplnqu  7704  cauappcvgprlemm  7729  cauappcvgprlemopl  7730  cauappcvgprlemlol  7731  cauappcvgprlemdisj  7735  cauappcvgprlemloc  7736  cauappcvgprlemladdfl  7739  cauappcvgprlemladdru  7740  cauappcvgprlemladdrl  7741  cauappcvgprlem1  7743  cauappcvgprlemlim  7745  cauappcvgpr  7746  caucvgprlemm  7752  caucvgprlemopl  7753  caucvgprlemlol  7754  caucvgprlemdisj  7758  caucvgprlemloc  7759  caucvgprlemladdrl  7762  caucvgprlem1  7763  caucvgpr  7766  caucvgprprlemell  7769  caucvgprprlemml  7778  caucvgprpr  7796  mulcmpblnrlemg  7824  addclsr  7837  mulclsr  7838  0idsr  7851  1idsr  7852  00sr  7853  ltasrg  7854  recexgt0sr  7857  mulgt0sr  7862  mulextsr1  7865  prsrriota  7872  caucvgsrlemgt1  7879  caucvgsrlemoffres  7884  pitonn  7932  peano2nnnn  7937  axaddrcl  7949  axmulrcl  7951  axaddcom  7954  ax1rid  7961  ax0id  7962  axprecex  7964  axcnre  7965  axpre-ltadd  7970  axpre-mulgt0  7971  axpre-mulext  7972  rereceu  7973  peano5nnnn  7976  axcaucvglemcau  7982  axcaucvglemres  7983  mulrid  8040  cnegexlem1  8218  cnegexlem2  8219  cnegex  8221  addcan2  8224  subval  8235  addlsub  8413  apreim  8647  recexap  8697  receuap  8713  divvalap  8718  cju  9005  peano2nn  9019  nn1m1nn  9025  nn1suc  9026  nnsub  9046  fv0p1e1  9122  nnm1nn0  9307  zdiv  9431  zneo  9444  nneoor  9445  zeo  9448  peano5uzti  9451  nn0ind-raph  9460  uzind4s  9681  uzind4s2  9682  qmulz  9714  elpq  9740  cnref1o  9742  nn0ledivnn  9859  xaddnemnf  9949  xaddnepnf  9950  xaddcom  9953  xaddid1  9954  xnn0xadd0  9959  xaddass  9961  xpncan  9963  xleadd1a  9965  xltadd1  9968  xlt2add  9972  xsubge0  9973  xposdif  9974  xlesubadd  9975  xleaddadd  9979  fzsuc2  10171  fzm1  10192  fzoval  10240  exbtwnzlemstep  10354  exbtwnzlemshrink  10355  exbtwnzlemex  10356  exbtwnz  10357  rebtwn2zlemstep  10359  rebtwn2zlemshrink  10360  rebtwn2z  10361  flqlelt  10383  flqbi  10397  fldiv4p1lem1div2  10412  fldiv4lem1div2  10414  modqval  10433  modqadd1  10470  modqmuladd  10475  modqmuladdnn0  10477  modqm1p1mod0  10484  modqmul1  10486  modfzo0difsn  10504  addmodlteq  10507  frec2uzzd  10509  frec2uzsucd  10510  frec2uzrand  10514  frecuzrdgrrn  10517  frec2uzrdg  10518  frecuzrdgrcl  10519  frecuzrdgsuc  10523  frecuzrdgrclt  10524  frecuzrdgg  10525  frecuzrdgdom  10527  frecuzrdgfun  10529  frecuzrdgsuctlem  10532  frecuzrdgsuct  10533  uzsinds  10553  iseqvalcbv  10568  seq3val  10569  seqvalcd  10570  seqf  10573  seq3p1  10574  seqovcd  10576  seqp1cd  10579  seq3fveq2  10584  seqfveq2g  10586  seq3shft2  10590  seqshft2g  10591  monoord  10594  monoord2  10595  seq3split  10597  seqsplitg  10598  seq3caopr3  10600  seqcaopr3g  10601  seq3caopr2  10602  seqcaopr2g  10603  iseqf1olemqval  10609  iseqf1olemqk  10616  seqf1oglem2a  10627  seqf1oglem2  10629  seq3id2  10635  seq3homo  10636  seq3z  10637  seqhomog  10639  seqfeq4g  10640  seq3distr  10641  m1expcl2  10670  mulexp  10687  expadd  10690  expmul  10693  sq0i  10740  qsqeqor  10759  sqoddm1div8  10802  facp1  10839  faclbnd  10850  faclbnd3  10852  bcval  10858  bcn1  10867  bcval5  10872  bcpasc  10875  bccl  10876  hashfz1  10892  omgadd  10911  hashfzo  10931  hashfzp1  10933  hashxp  10935  seq3coll  10951  shftlem  10998  shftfvalg  11000  shftfibg  11002  shftfval  11003  shftfib  11005  shftfn  11006  shftf  11012  2shfti  11013  shftvalg  11018  shftval4g  11019  cjval  11027  imval  11032  cjexp  11075  cnrecnv  11092  cvg1nlemcau  11166  cvg1nlemres  11167  resqrexlemcalc3  11198  resqrexlemex  11207  rsqrmo  11209  resqrtcl  11211  rersqrtthlem  11212  sqrtsq  11226  absexp  11261  recan  11291  climshft  11486  climcn1  11490  climcn2  11491  subcn2  11493  fsumshft  11626  fisum0diag2  11629  fsumiun  11659  binomlem  11665  binom  11666  bcxmas  11671  isumsplit  11673  arisum2  11681  trireciplem  11682  trirecip  11683  geolim  11693  cvgratnnlemnexp  11706  cvgratnnlemmn  11707  clim2prod  11721  prodfrecap  11728  fprodcl2lem  11787  fprodfac  11797  fprodshft  11800  ef0lem  11842  efval  11843  efne0  11860  efexp  11864  demoivreALT  11956  dvdsval2  11972  p1modz1  11976  dvds0lem  11983  dvds1lem  11984  dvds2lem  11985  dvdsmulc  12001  divconjdvds  12031  odd2np1lem  12054  odd2np1  12055  ltoddhalfle  12075  halfleoddlt  12076  nn0o1gt2  12087  nn0o  12089  divalglemnn  12100  divalglemeunn  12103  divalglemex  12104  divalglemeuneg  12105  flodddiv4  12118  bitsinv1  12144  gcdabs1  12181  gcddiv  12211  dvdssqim  12216  rpmulgcd  12218  bezoutr1  12225  uzwodc  12229  dvdslcm  12262  lcmeq0  12264  lcmdvds  12272  divgcdcoprm0  12294  prmind2  12313  isprm5lem  12334  isprm6  12340  rpexp  12346  sqrt2irr  12355  pw2dvdslemn  12358  pw2dvdseu  12361  oddpwdclemxy  12362  nn0gcdsq  12393  phicl2  12407  phibndlem  12409  hashdvds  12414  crth  12417  phimullem  12418  eulerthlem1  12420  eulerthlemfi  12421  eulerthlemrprm  12422  eulerthlemth  12425  eulerth  12426  hashgcdlem  12431  phisum  12434  odzval  12435  modprm0  12448  nnnn0modprm0  12449  pythagtriplem1  12459  pythagtriplem6  12464  pythagtriplem7  12465  pythagtriplem12  12469  pythagtriplem14  12471  pythagtriplem18  12475  pythagtriplem19  12476  pceulem  12488  pceu  12489  pcval  12490  pczpre  12491  pcdiv  12496  pcqmul  12497  pcqcl  12500  pcexp  12503  pcaddlem  12533  pcadd  12534  pcmpt  12537  pcprod  12540  pcfac  12544  expnprm  12547  prmpwdvds  12549  pockthi  12552  1arithlem2  12558  4sqlem2  12583  4sqlem3  12584  4sqlem11  12595  4sqlem12  12596  4sqlem13m  12597  4sqlem17  12601  4sqlem18  12602  4sqlem19  12603  ennnfonelemr  12665  ctinfom  12670  infpn2  12698  ercpbl  13033  mgm1  13072  mgmidmo  13074  ismgmid  13079  mgmlrid  13081  ismgmid2  13082  lidrideqd  13083  lidrididd  13084  mgmidsssn0  13086  grprida  13089  gsumfzval  13093  gsumress  13097  gsumval2  13099  isnsgrp  13108  sgrpass  13110  sgrp1  13113  sgrpidmndm  13122  ismndd  13139  mndinvmod  13147  imasmnd2  13154  mnd1  13157  mnd1id  13158  mhmpropd  13168  insubm  13187  mhmima  13193  gsumvallem2  13195  grppropd  13219  isgrpd2  13223  isgrpd  13225  dfgrp2  13229  grprcan  13239  grpinveu  13240  grpsubval  13248  grplinv  13252  grpinvid2  13255  isgrpinv  13256  grplrinv  13259  grpidinv2  13260  grpidinv  13261  grpidssd  13278  grpinvssd  13279  dfgrp3mlem  13300  dfgrp3m  13301  grplactfval  13303  grp1  13308  imasgrp2  13316  mhmmnd  13322  ghmgrp  13324  mulgnn0gsum  13334  mulgnn0p1  13339  mulgnn0subcl  13341  mulgaddcom  13352  mulginvcom  13353  mulgnn0z  13355  mulgneg2  13362  mulgnnass  13363  mulgnn0ass  13364  mhmmulg  13369  issubg  13379  subgex  13382  issubg2m  13395  issubg4m  13399  isnsg2  13409  nsgbi  13410  isnsg3  13413  elnmz  13414  nmzbi  13415  ghmrn  13463  ghmnsgima  13474  gsumfzconst  13547  rngdi  13572  rngdir  13573  srgrz  13616  srgmulgass  13621  srgpcomp  13622  srgrmhm  13626  ringid  13658  ringinvnzdiv  13682  mulgass2  13690  ring1  13691  ringrghm  13694  imasring  13696  dvdsrmuld  13728  dvdsrmul1  13734  dvdsr01  13736  dvreq1  13774  rhmdvdsr  13807  lringuplu  13828  issubrng  13831  issubrng2  13842  issubrg  13853  issubrg2  13873  isrrg  13895  domneq0  13904  lmodlema  13924  islmodd  13925  lmodvsmmulgdi  13955  rmodislmodlem  13982  rmodislmod  13983  lssclg  13996  lss1d  14015  lspsn  14048  sraval  14069  rnglidlmcl  14112  quscrng  14165  cnfldmulg  14208  cnfldexp  14209  gsumfzfsumlemm  14219  cnfldui  14221  expghmap  14239  mulgghm2  14240  mulgrhm  14241  zrhmulg  14252  zlmval  14259  znunit  14291  cnmptcom  14618  psmettri2  14648  isxmet2d  14668  xmeteq0  14679  xmettri2  14681  metrest  14826  mpomulcn  14886  expcn  14889  cncfval  14892  mulc1cncf  14909  addccncf  14920  mulcncf  14928  expcncf  14929  hovera  14967  hoverb  14968  hoverlt1  14969  hovergt0  14970  ivthdich  14973  limccnp2lem  14996  dvcnp2cntop  15019  dvcoapbr  15027  dvexp  15031  dvrecap  15033  dvef  15047  plyadd  15071  plymul  15072  plycoeid3  15077  plyco  15079  plycjlemc  15080  plycj  15081  plyrecj  15083  dvply1  15085  dvply2g  15086  sincn  15089  coscn  15090  ptolemy  15144  sincosq1eq  15159  rpcxpmul2  15233  logbgcd1irr  15287  logbgcd1irraplemexp  15288  2irrexpq  15296  2irrexpqap  15298  mpodvdsmulf1o  15310  fsumdvdsmul  15311  sgmppw  15312  sgmmul  15316  perfect  15321  lgslem4  15328  lgsval  15329  lgsfvalg  15330  lgsval2lem  15335  lgsdir2lem4  15356  lgsdir  15360  lgsdilem2  15361  lgsdi  15362  lgsne0  15363  lgsmodeq  15370  lgsdirnn0  15372  lgsdinn0  15373  gausslemma2dlem0i  15382  gausslemma2dlem1a  15383  gausslemma2dlem1f1o  15385  gausslemma2dlem2  15387  gausslemma2dlem3  15388  gausslemma2dlem4  15389  lgseisenlem2  15396  lgsquadlem2  15403  lgsquadlem3  15404  lgsquad  15405  lgsquad2lem2  15407  2lgslem1a  15413  2lgslem1b  15414  2lgslem1c  15415  2lgslem3a  15418  2lgslem3b  15419  2lgslem3c  15420  2lgslem3d  15421  2lgslem3a1  15422  2lgslem3b1  15423  2lgslem3c1  15424  2lgslem3d1  15425  2lgs  15429  2lgsoddprmlem1  15430  2lgsoddprmlem3  15436  2sqlem2  15440  2sqlem6  15445  2sqlem8  15448  2sqlem9  15449  qdencn  15758  isomninn  15762  trirec0  15775  iswomninn  15781  ismkvnn  15784