Theorem oveq1 5904

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 3793	. . 3 |- ( A = B -> <. A , C >. = <. B , C >. )
2	1	fveq2d 5538	. 2 |- ( A = B -> ( F ` <. A , C >. ) = ( F ` <. B , C >. ) )
3		df-ov 5900	. 2 |- ( A F C ) = ( F ` <. A , C >. )
4		df-ov 5900	. 2 |- ( B F C ) = ( F ` <. B , C >. )
5	2, 3, 4	3eqtr4g 2247	1 |- ( A = B -> ( A F C ) = ( B F C ) )

Syntax hints:   -> wi 4   = wceq 1364   <.cop 3610   ` cfv 5235  (class class class)co 5897

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 2171

This theorem depends on definitions:  df-bi 117  df-3an 982  df-tru 1367  df-nf 1472  df-sb 1774  df-clab 2176  df-cleq 2182  df-clel 2185  df-nfc 2321  df-rex 2474  df-v 2754  df-un 3148  df-sn 3613  df-pr 3614  df-op 3616  df-uni 3825  df-br 4019  df-iota 5196  df-fv 5243  df-ov 5900

This theorem is referenced by:  oveq12  5906  oveq1i  5907  oveq1d  5912  ovrspc2v  5923  oveqrspc2v  5924  rspceov  5939  fovcld  6002  ovmpos  6021  ov2gf  6022  ovi3  6034  caovclg  6050  caovcomg  6053  caovassg  6056  caovcang  6059  caovcan  6062  caovordig  6063  caovordg  6065  caovord  6069  caovdig  6072  caovdirg  6075  caovimo  6091  suppssov1  6104  off  6120  omcl  6487  oeicl  6488  omv2  6491  nnm0r  6505  nnacom  6510  nndi  6512  nnmass  6513  nnmsucr  6514  nnmcom  6515  nnaword  6537  nnmord  6543  nnm00  6556  eroveu  6653  th3qlem2  6665  th3q  6667  ecovcom  6669  ecovicom  6670  ecovass  6671  ecoviass  6672  ecovdi  6673  ecovidi  6674  map0g  6715  addcmpblnq  7397  addclnq  7405  mulclnq  7406  mulidnq  7419  recexnq  7420  recmulnqg  7421  ltanqg  7430  ltmnqg  7431  ltexnqq  7438  enq0ref  7463  enq0tr  7464  addcmpblnq0  7473  mulnnnq0  7480  addclnq0  7481  mulclnq0  7482  distrnq0  7489  mulcomnq0  7490  addassnq0  7492  prarloclemlo  7524  prarloclem3  7527  prarloclem5  7530  prarloclemcalc  7532  genipv  7539  genpassl  7554  genpassu  7555  addlocprlemeq  7563  distrlem4prl  7614  distrlem4pru  7615  ltexprlemdisj  7636  ltexprlemloc  7637  ltexprlemrl  7640  ltexprlemru  7642  prplnqu  7650  cauappcvgprlemm  7675  cauappcvgprlemopl  7676  cauappcvgprlemlol  7677  cauappcvgprlemdisj  7681  cauappcvgprlemloc  7682  cauappcvgprlemladdfl  7685  cauappcvgprlemladdru  7686  cauappcvgprlemladdrl  7687  cauappcvgprlem1  7689  cauappcvgprlemlim  7691  cauappcvgpr  7692  caucvgprlemm  7698  caucvgprlemopl  7699  caucvgprlemlol  7700  caucvgprlemdisj  7704  caucvgprlemloc  7705  caucvgprlemladdrl  7708  caucvgprlem1  7709  caucvgpr  7712  caucvgprprlemell  7715  caucvgprprlemml  7724  caucvgprpr  7742  mulcmpblnrlemg  7770  addclsr  7783  mulclsr  7784  0idsr  7797  1idsr  7798  00sr  7799  ltasrg  7800  recexgt0sr  7803  mulgt0sr  7808  mulextsr1  7811  prsrriota  7818  caucvgsrlemgt1  7825  caucvgsrlemoffres  7830  pitonn  7878  peano2nnnn  7883  axaddrcl  7895  axmulrcl  7897  axaddcom  7900  ax1rid  7907  ax0id  7908  axprecex  7910  axcnre  7911  axpre-ltadd  7916  axpre-mulgt0  7917  axpre-mulext  7918  rereceu  7919  peano5nnnn  7922  axcaucvglemcau  7928  axcaucvglemres  7929  mulrid  7985  cnegexlem1  8163  cnegexlem2  8164  cnegex  8166  addcan2  8169  subval  8180  addlsub  8358  apreim  8591  recexap  8641  receuap  8657  divvalap  8662  cju  8949  peano2nn  8962  nn1m1nn  8968  nn1suc  8969  nnsub  8989  fv0p1e1  9065  nnm1nn0  9248  zdiv  9372  zneo  9385  nneoor  9386  zeo  9389  peano5uzti  9392  nn0ind-raph  9401  uzind4s  9622  uzind4s2  9623  qmulz  9655  elpq  9680  cnref1o  9682  nn0ledivnn  9799  xaddnemnf  9889  xaddnepnf  9890  xaddcom  9893  xaddid1  9894  xnn0xadd0  9899  xaddass  9901  xpncan  9903  xleadd1a  9905  xltadd1  9908  xlt2add  9912  xsubge0  9913  xposdif  9914  xlesubadd  9915  xleaddadd  9919  fzsuc2  10111  fzm1  10132  fzoval  10180  exbtwnzlemstep  10280  exbtwnzlemshrink  10281  exbtwnzlemex  10282  exbtwnz  10283  rebtwn2zlemstep  10285  rebtwn2zlemshrink  10286  rebtwn2z  10287  flqlelt  10309  flqbi  10323  fldiv4p1lem1div2  10338  modqval  10357  modqadd1  10394  modqmuladd  10399  modqmuladdnn0  10401  modqm1p1mod0  10408  modqmul1  10410  modfzo0difsn  10428  addmodlteq  10431  frec2uzzd  10433  frec2uzsucd  10434  frec2uzrand  10438  frecuzrdgrrn  10441  frec2uzrdg  10442  frecuzrdgrcl  10443  frecuzrdgsuc  10447  frecuzrdgrclt  10448  frecuzrdgg  10449  frecuzrdgdom  10451  frecuzrdgfun  10453  frecuzrdgsuctlem  10456  frecuzrdgsuct  10457  uzsinds  10475  iseqvalcbv  10490  seq3val  10491  seqvalcd  10492  seqf  10494  seq3p1  10495  seqovcd  10496  seqp1cd  10499  seq3fveq2  10502  seq3shft2  10506  monoord  10509  monoord2  10510  seq3split  10512  seq3caopr3  10514  seq3caopr2  10515  iseqf1olemqval  10520  iseqf1olemqk  10527  seq3id2  10542  seq3homo  10543  seq3z  10544  seqfeq4g  10546  seq3distr  10547  m1expcl2  10576  mulexp  10593  expadd  10596  expmul  10599  sq0i  10646  qsqeqor  10665  sqoddm1div8  10708  facp1  10745  faclbnd  10756  faclbnd3  10758  bcval  10764  bcn1  10773  bcval5  10778  bcpasc  10781  bccl  10782  hashfz1  10798  omgadd  10817  hashfzo  10837  hashfzp1  10839  hashxp  10841  seq3coll  10857  shftlem  10860  shftfvalg  10862  shftfibg  10864  shftfval  10865  shftfib  10867  shftfn  10868  shftf  10874  2shfti  10875  shftvalg  10880  shftval4g  10881  cjval  10889  imval  10894  cjexp  10937  cnrecnv  10954  cvg1nlemcau  11028  cvg1nlemres  11029  resqrexlemcalc3  11060  resqrexlemex  11069  rsqrmo  11071  resqrtcl  11073  rersqrtthlem  11074  sqrtsq  11088  absexp  11123  recan  11153  climshft  11347  climcn1  11351  climcn2  11352  subcn2  11354  fsumshft  11487  fisum0diag2  11490  fsumiun  11520  binomlem  11526  binom  11527  bcxmas  11532  isumsplit  11534  arisum2  11542  trireciplem  11543  trirecip  11544  geolim  11554  cvgratnnlemnexp  11567  cvgratnnlemmn  11568  clim2prod  11582  prodfrecap  11589  fprodcl2lem  11648  fprodfac  11658  fprodshft  11661  ef0lem  11703  efval  11704  efne0  11721  efexp  11725  demoivreALT  11816  dvdsval2  11832  p1modz1  11836  dvds0lem  11843  dvds1lem  11844  dvds2lem  11845  dvdsmulc  11861  divconjdvds  11890  odd2np1lem  11912  odd2np1  11913  ltoddhalfle  11933  halfleoddlt  11934  nn0o1gt2  11945  nn0o  11947  divalglemnn  11958  divalglemeunn  11961  divalglemex  11962  divalglemeuneg  11963  flodddiv4  11974  gcdabs1  12025  gcddiv  12055  dvdssqim  12060  rpmulgcd  12062  bezoutr1  12069  uzwodc  12073  dvdslcm  12104  lcmeq0  12106  lcmdvds  12114  divgcdcoprm0  12136  prmind2  12155  isprm5lem  12176  isprm6  12182  rpexp  12188  sqrt2irr  12197  pw2dvdslemn  12200  pw2dvdseu  12203  oddpwdclemxy  12204  nn0gcdsq  12235  phicl2  12249  phibndlem  12251  hashdvds  12256  crth  12259  phimullem  12260  eulerthlem1  12262  eulerthlemfi  12263  eulerthlemrprm  12264  eulerthlemth  12267  eulerth  12268  hashgcdlem  12273  phisum  12275  odzval  12276  modprm0  12289  nnnn0modprm0  12290  pythagtriplem1  12300  pythagtriplem6  12305  pythagtriplem7  12306  pythagtriplem12  12310  pythagtriplem14  12312  pythagtriplem18  12316  pythagtriplem19  12317  pceulem  12329  pceu  12330  pcval  12331  pczpre  12332  pcdiv  12337  pcqmul  12338  pcqcl  12341  pcexp  12344  pcaddlem  12374  pcadd  12375  pcmpt  12378  pcprod  12381  pcfac  12385  expnprm  12388  prmpwdvds  12390  pockthi  12393  1arithlem2  12399  4sqlem2  12424  4sqlem3  12425  4sqlem11  12436  4sqlem12  12437  4sqlem13m  12438  4sqlem17  12442  4sqlem18  12443  4sqlem19  12444  ennnfonelemr  12477  ctinfom  12482  infpn2  12510  ercpbl  12810  mgm1  12849  mgmidmo  12851  ismgmid  12856  mgmlrid  12858  ismgmid2  12859  lidrideqd  12860  lidrididd  12861  mgmidsssn0  12863  grprida  12866  gsumress  12873  gsumval2  12875  isnsgrp  12884  sgrpass  12886  sgrp1  12889  sgrpidmndm  12896  ismndd  12913  mndinvmod  12921  mnd1  12922  mnd1id  12923  mhmpropd  12933  insubm  12952  mhmima  12958  grppropd  12977  isgrpd2  12981  isgrpd  12983  dfgrp2  12986  grprcan  12996  grpinveu  12997  grpsubval  13005  grplinv  13009  grpinvid2  13012  isgrpinv  13013  grplrinv  13016  grpidinv2  13017  grpidinv  13018  grpidssd  13035  grpinvssd  13036  dfgrp3mlem  13057  dfgrp3m  13058  grplactfval  13060  grp1  13065  imasgrp2  13067  mhmmnd  13073  ghmgrp  13075  mulgnn0gsum  13085  mulgnn0p1  13090  mulgnn0subcl  13092  mulgaddcom  13103  mulginvcom  13104  mulgnn0z  13106  mulgneg2  13113  mulgnnass  13114  mulgnn0ass  13115  mhmmulg  13120  issubg  13129  subgex  13132  issubg2m  13145  issubg4m  13149  isnsg2  13159  nsgbi  13160  isnsg3  13163  elnmz  13164  nmzbi  13165  ghmrn  13213  ghmnsgima  13224  rngdi  13311  rngdir  13312  srgrz  13355  srgmulgass  13360  srgpcomp  13361  srgrmhm  13365  ringid  13397  ringinvnzdiv  13419  mulgass2  13427  ring1  13428  imasring  13431  dvdsrmuld  13463  dvdsrmul1  13469  dvdsr01  13471  dvreq1  13509  rhmdvdsr  13542  lringuplu  13560  issubrng  13563  issubrng2  13574  issubrg  13585  issubrg2  13605  lmodlema  13625  islmodd  13626  lmodvsmmulgdi  13656  rmodislmodlem  13683  rmodislmod  13684  lssclg  13697  lss1d  13716  lspsn  13749  sraval  13770  rnglidlmcl  13813  quscrng  13864  cnfldmulg  13896  cnfldexp  13897  mulgghm2  13923  mulgrhm  13924  zrhmulg  13934  zlmval  13940  cnmptcom  14275  psmettri2  14305  isxmet2d  14325  xmeteq0  14336  xmettri2  14338  metrest  14483  cncfval  14536  mulc1cncf  14553  addccncf  14563  mulcncf  14568  expcncf  14569  limccnp2lem  14622  dvcnp2cntop  14640  dvcoapbr  14648  dvexp  14652  dvrecap  14654  dvef  14665  sincn  14667  coscn  14668  ptolemy  14722  sincosq1eq  14737  logbgcd1irr  14862  logbgcd1irraplemexp  14863  2irrexpq  14871  2irrexpqap  14873  lgslem4  14882  lgsval  14883  lgsfvalg  14884  lgsval2lem  14889  lgsdir2lem4  14910  lgsdir  14914  lgsdilem2  14915  lgsdi  14916  lgsne0  14917  lgsmodeq  14924  lgsdirnn0  14926  lgsdinn0  14927  lgseisenlem2  14929  2lgsoddprmlem1  14931  2lgsoddprmlem3  14937  2sqlem2  14940  2sqlem6  14945  2sqlem8  14948  2sqlem9  14949  qdencn  15254  isomninn  15258  trirec0  15271  iswomninn  15277  ismkvnn  15280