Theorem oveq1 5929

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 3808	. . 3 |- ( A = B -> <. A , C >. = <. B , C >. )
2	1	fveq2d 5562	. 2 |- ( A = B -> ( F ` <. A , C >. ) = ( F ` <. B , C >. ) )
3		df-ov 5925	. 2 |- ( A F C ) = ( F ` <. A , C >. )
4		df-ov 5925	. 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 3625   ` cfv 5258  (class class class)co 5922

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 3628  df-pr 3629  df-op 3631  df-uni 3840  df-br 4034  df-iota 5219  df-fv 5266  df-ov 5925

This theorem is referenced by:  oveq12  5931  oveq1i  5932  oveq1d  5937  ovrspc2v  5948  oveqrspc2v  5949  rspceov  5964  fovcld  6027  ovmpos  6046  ov2gf  6047  ovi3  6060  caovclg  6076  caovcomg  6079  caovassg  6082  caovcang  6085  caovcan  6088  caovordig  6089  caovordg  6091  caovord  6095  caovdig  6098  caovdirg  6101  caovimo  6117  suppssov1  6132  off  6148  caofdig  6164  omcl  6519  oeicl  6520  omv2  6523  nnm0r  6537  nnacom  6542  nndi  6544  nnmass  6545  nnmsucr  6546  nnmcom  6547  nnaword  6569  nnmord  6575  nnm00  6588  eroveu  6685  th3qlem2  6697  th3q  6699  ecovcom  6701  ecovicom  6702  ecovass  6703  ecoviass  6704  ecovdi  6705  ecovidi  6706  map0g  6747  addcmpblnq  7434  addclnq  7442  mulclnq  7443  mulidnq  7456  recexnq  7457  recmulnqg  7458  ltanqg  7467  ltmnqg  7468  ltexnqq  7475  enq0ref  7500  enq0tr  7501  addcmpblnq0  7510  mulnnnq0  7517  addclnq0  7518  mulclnq0  7519  distrnq0  7526  mulcomnq0  7527  addassnq0  7529  prarloclemlo  7561  prarloclem3  7564  prarloclem5  7567  prarloclemcalc  7569  genipv  7576  genpassl  7591  genpassu  7592  addlocprlemeq  7600  distrlem4prl  7651  distrlem4pru  7652  ltexprlemdisj  7673  ltexprlemloc  7674  ltexprlemrl  7677  ltexprlemru  7679  prplnqu  7687  cauappcvgprlemm  7712  cauappcvgprlemopl  7713  cauappcvgprlemlol  7714  cauappcvgprlemdisj  7718  cauappcvgprlemloc  7719  cauappcvgprlemladdfl  7722  cauappcvgprlemladdru  7723  cauappcvgprlemladdrl  7724  cauappcvgprlem1  7726  cauappcvgprlemlim  7728  cauappcvgpr  7729  caucvgprlemm  7735  caucvgprlemopl  7736  caucvgprlemlol  7737  caucvgprlemdisj  7741  caucvgprlemloc  7742  caucvgprlemladdrl  7745  caucvgprlem1  7746  caucvgpr  7749  caucvgprprlemell  7752  caucvgprprlemml  7761  caucvgprpr  7779  mulcmpblnrlemg  7807  addclsr  7820  mulclsr  7821  0idsr  7834  1idsr  7835  00sr  7836  ltasrg  7837  recexgt0sr  7840  mulgt0sr  7845  mulextsr1  7848  prsrriota  7855  caucvgsrlemgt1  7862  caucvgsrlemoffres  7867  pitonn  7915  peano2nnnn  7920  axaddrcl  7932  axmulrcl  7934  axaddcom  7937  ax1rid  7944  ax0id  7945  axprecex  7947  axcnre  7948  axpre-ltadd  7953  axpre-mulgt0  7954  axpre-mulext  7955  rereceu  7956  peano5nnnn  7959  axcaucvglemcau  7965  axcaucvglemres  7966  mulrid  8023  cnegexlem1  8201  cnegexlem2  8202  cnegex  8204  addcan2  8207  subval  8218  addlsub  8396  apreim  8630  recexap  8680  receuap  8696  divvalap  8701  cju  8988  peano2nn  9002  nn1m1nn  9008  nn1suc  9009  nnsub  9029  fv0p1e1  9105  nnm1nn0  9290  zdiv  9414  zneo  9427  nneoor  9428  zeo  9431  peano5uzti  9434  nn0ind-raph  9443  uzind4s  9664  uzind4s2  9665  qmulz  9697  elpq  9723  cnref1o  9725  nn0ledivnn  9842  xaddnemnf  9932  xaddnepnf  9933  xaddcom  9936  xaddid1  9937  xnn0xadd0  9942  xaddass  9944  xpncan  9946  xleadd1a  9948  xltadd1  9951  xlt2add  9955  xsubge0  9956  xposdif  9957  xlesubadd  9958  xleaddadd  9962  fzsuc2  10154  fzm1  10175  fzoval  10223  exbtwnzlemstep  10337  exbtwnzlemshrink  10338  exbtwnzlemex  10339  exbtwnz  10340  rebtwn2zlemstep  10342  rebtwn2zlemshrink  10343  rebtwn2z  10344  flqlelt  10366  flqbi  10380  fldiv4p1lem1div2  10395  fldiv4lem1div2  10397  modqval  10416  modqadd1  10453  modqmuladd  10458  modqmuladdnn0  10460  modqm1p1mod0  10467  modqmul1  10469  modfzo0difsn  10487  addmodlteq  10490  frec2uzzd  10492  frec2uzsucd  10493  frec2uzrand  10497  frecuzrdgrrn  10500  frec2uzrdg  10501  frecuzrdgrcl  10502  frecuzrdgsuc  10506  frecuzrdgrclt  10507  frecuzrdgg  10508  frecuzrdgdom  10510  frecuzrdgfun  10512  frecuzrdgsuctlem  10515  frecuzrdgsuct  10516  uzsinds  10536  iseqvalcbv  10551  seq3val  10552  seqvalcd  10553  seqf  10556  seq3p1  10557  seqovcd  10559  seqp1cd  10562  seq3fveq2  10567  seqfveq2g  10569  seq3shft2  10573  seqshft2g  10574  monoord  10577  monoord2  10578  seq3split  10580  seqsplitg  10581  seq3caopr3  10583  seqcaopr3g  10584  seq3caopr2  10585  seqcaopr2g  10586  iseqf1olemqval  10592  iseqf1olemqk  10599  seqf1oglem2a  10610  seqf1oglem2  10612  seq3id2  10618  seq3homo  10619  seq3z  10620  seqhomog  10622  seqfeq4g  10623  seq3distr  10624  m1expcl2  10653  mulexp  10670  expadd  10673  expmul  10676  sq0i  10723  qsqeqor  10742  sqoddm1div8  10785  facp1  10822  faclbnd  10833  faclbnd3  10835  bcval  10841  bcn1  10850  bcval5  10855  bcpasc  10858  bccl  10859  hashfz1  10875  omgadd  10894  hashfzo  10914  hashfzp1  10916  hashxp  10918  seq3coll  10934  shftlem  10981  shftfvalg  10983  shftfibg  10985  shftfval  10986  shftfib  10988  shftfn  10989  shftf  10995  2shfti  10996  shftvalg  11001  shftval4g  11002  cjval  11010  imval  11015  cjexp  11058  cnrecnv  11075  cvg1nlemcau  11149  cvg1nlemres  11150  resqrexlemcalc3  11181  resqrexlemex  11190  rsqrmo  11192  resqrtcl  11194  rersqrtthlem  11195  sqrtsq  11209  absexp  11244  recan  11274  climshft  11469  climcn1  11473  climcn2  11474  subcn2  11476  fsumshft  11609  fisum0diag2  11612  fsumiun  11642  binomlem  11648  binom  11649  bcxmas  11654  isumsplit  11656  arisum2  11664  trireciplem  11665  trirecip  11666  geolim  11676  cvgratnnlemnexp  11689  cvgratnnlemmn  11690  clim2prod  11704  prodfrecap  11711  fprodcl2lem  11770  fprodfac  11780  fprodshft  11783  ef0lem  11825  efval  11826  efne0  11843  efexp  11847  demoivreALT  11939  dvdsval2  11955  p1modz1  11959  dvds0lem  11966  dvds1lem  11967  dvds2lem  11968  dvdsmulc  11984  divconjdvds  12014  odd2np1lem  12037  odd2np1  12038  ltoddhalfle  12058  halfleoddlt  12059  nn0o1gt2  12070  nn0o  12072  divalglemnn  12083  divalglemeunn  12086  divalglemex  12087  divalglemeuneg  12088  flodddiv4  12101  gcdabs1  12156  gcddiv  12186  dvdssqim  12191  rpmulgcd  12193  bezoutr1  12200  uzwodc  12204  dvdslcm  12237  lcmeq0  12239  lcmdvds  12247  divgcdcoprm0  12269  prmind2  12288  isprm5lem  12309  isprm6  12315  rpexp  12321  sqrt2irr  12330  pw2dvdslemn  12333  pw2dvdseu  12336  oddpwdclemxy  12337  nn0gcdsq  12368  phicl2  12382  phibndlem  12384  hashdvds  12389  crth  12392  phimullem  12393  eulerthlem1  12395  eulerthlemfi  12396  eulerthlemrprm  12397  eulerthlemth  12400  eulerth  12401  hashgcdlem  12406  phisum  12409  odzval  12410  modprm0  12423  nnnn0modprm0  12424  pythagtriplem1  12434  pythagtriplem6  12439  pythagtriplem7  12440  pythagtriplem12  12444  pythagtriplem14  12446  pythagtriplem18  12450  pythagtriplem19  12451  pceulem  12463  pceu  12464  pcval  12465  pczpre  12466  pcdiv  12471  pcqmul  12472  pcqcl  12475  pcexp  12478  pcaddlem  12508  pcadd  12509  pcmpt  12512  pcprod  12515  pcfac  12519  expnprm  12522  prmpwdvds  12524  pockthi  12527  1arithlem2  12533  4sqlem2  12558  4sqlem3  12559  4sqlem11  12570  4sqlem12  12571  4sqlem13m  12572  4sqlem17  12576  4sqlem18  12577  4sqlem19  12578  ennnfonelemr  12640  ctinfom  12645  infpn2  12673  ercpbl  12974  mgm1  13013  mgmidmo  13015  ismgmid  13020  mgmlrid  13022  ismgmid2  13023  lidrideqd  13024  lidrididd  13025  mgmidsssn0  13027  grprida  13030  gsumfzval  13034  gsumress  13038  gsumval2  13040  isnsgrp  13049  sgrpass  13051  sgrp1  13054  sgrpidmndm  13061  ismndd  13078  mndinvmod  13086  mnd1  13087  mnd1id  13088  mhmpropd  13098  insubm  13117  mhmima  13123  gsumvallem2  13125  grppropd  13149  isgrpd2  13153  isgrpd  13155  dfgrp2  13159  grprcan  13169  grpinveu  13170  grpsubval  13178  grplinv  13182  grpinvid2  13185  isgrpinv  13186  grplrinv  13189  grpidinv2  13190  grpidinv  13191  grpidssd  13208  grpinvssd  13209  dfgrp3mlem  13230  dfgrp3m  13231  grplactfval  13233  grp1  13238  imasgrp2  13240  mhmmnd  13246  ghmgrp  13248  mulgnn0gsum  13258  mulgnn0p1  13263  mulgnn0subcl  13265  mulgaddcom  13276  mulginvcom  13277  mulgnn0z  13279  mulgneg2  13286  mulgnnass  13287  mulgnn0ass  13288  mhmmulg  13293  issubg  13303  subgex  13306  issubg2m  13319  issubg4m  13323  isnsg2  13333  nsgbi  13334  isnsg3  13337  elnmz  13338  nmzbi  13339  ghmrn  13387  ghmnsgima  13398  gsumfzconst  13471  rngdi  13496  rngdir  13497  srgrz  13540  srgmulgass  13545  srgpcomp  13546  srgrmhm  13550  ringid  13582  ringinvnzdiv  13606  mulgass2  13614  ring1  13615  ringrghm  13618  imasring  13620  dvdsrmuld  13652  dvdsrmul1  13658  dvdsr01  13660  dvreq1  13698  rhmdvdsr  13731  lringuplu  13752  issubrng  13755  issubrng2  13766  issubrg  13777  issubrg2  13797  isrrg  13819  domneq0  13828  lmodlema  13848  islmodd  13849  lmodvsmmulgdi  13879  rmodislmodlem  13906  rmodislmod  13907  lssclg  13920  lss1d  13939  lspsn  13972  sraval  13993  rnglidlmcl  14036  quscrng  14089  cnfldmulg  14132  cnfldexp  14133  gsumfzfsumlemm  14143  cnfldui  14145  expghmap  14163  mulgghm2  14164  mulgrhm  14165  zrhmulg  14176  zlmval  14183  znunit  14215  cnmptcom  14534  psmettri2  14564  isxmet2d  14584  xmeteq0  14595  xmettri2  14597  metrest  14742  mpomulcn  14802  expcn  14805  cncfval  14808  mulc1cncf  14825  addccncf  14836  mulcncf  14844  expcncf  14845  hovera  14883  hoverb  14884  hoverlt1  14885  hovergt0  14886  ivthdich  14889  limccnp2lem  14912  dvcnp2cntop  14935  dvcoapbr  14943  dvexp  14947  dvrecap  14949  dvef  14963  plyadd  14987  plymul  14988  plycoeid3  14993  plyco  14995  plycjlemc  14996  plycj  14997  plyrecj  14999  dvply1  15001  dvply2g  15002  sincn  15005  coscn  15006  ptolemy  15060  sincosq1eq  15075  rpcxpmul2  15149  logbgcd1irr  15203  logbgcd1irraplemexp  15204  2irrexpq  15212  2irrexpqap  15214  mpodvdsmulf1o  15226  fsumdvdsmul  15227  sgmppw  15228  sgmmul  15232  perfect  15237  lgslem4  15244  lgsval  15245  lgsfvalg  15246  lgsval2lem  15251  lgsdir2lem4  15272  lgsdir  15276  lgsdilem2  15277  lgsdi  15278  lgsne0  15279  lgsmodeq  15286  lgsdirnn0  15288  lgsdinn0  15289  gausslemma2dlem0i  15298  gausslemma2dlem1a  15299  gausslemma2dlem1f1o  15301  gausslemma2dlem2  15303  gausslemma2dlem3  15304  gausslemma2dlem4  15305  lgseisenlem2  15312  lgsquadlem2  15319  lgsquadlem3  15320  lgsquad  15321  lgsquad2lem2  15323  2lgslem1a  15329  2lgslem1b  15330  2lgslem1c  15331  2lgslem3a  15334  2lgslem3b  15335  2lgslem3c  15336  2lgslem3d  15337  2lgslem3a1  15338  2lgslem3b1  15339  2lgslem3c1  15340  2lgslem3d1  15341  2lgs  15345  2lgsoddprmlem1  15346  2lgsoddprmlem3  15352  2sqlem2  15356  2sqlem6  15361  2sqlem8  15364  2sqlem9  15365  qdencn  15671  isomninn  15675  trirec0  15688  iswomninn  15694  ismkvnn  15697