Theorem oveq1 5882

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 3779	. . 3 |- ( A = B -> <. A , C >. = <. B , C >. )
2	1	fveq2d 5520	. 2 |- ( A = B -> ( F ` <. A , C >. ) = ( F ` <. B , C >. ) )
3		df-ov 5878	. 2 |- ( A F C ) = ( F ` <. A , C >. )
4		df-ov 5878	. 2 |- ( B F C ) = ( F ` <. B , C >. )
5	2, 3, 4	3eqtr4g 2235	1 |- ( A = B -> ( A F C ) = ( B F C ) )

Syntax hints:   -> wi 4   = wceq 1353   <.cop 3596   ` cfv 5217  (class class class)co 5875

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 709  ax-5 1447  ax-7 1448  ax-gen 1449  ax-ie1 1493  ax-ie2 1494  ax-8 1504  ax-10 1505  ax-11 1506  ax-i12 1507  ax-bndl 1509  ax-4 1510  ax-17 1526  ax-i9 1530  ax-ial 1534  ax-i5r 1535  ax-ext 2159

This theorem depends on definitions:  df-bi 117  df-3an 980  df-tru 1356  df-nf 1461  df-sb 1763  df-clab 2164  df-cleq 2170  df-clel 2173  df-nfc 2308  df-rex 2461  df-v 2740  df-un 3134  df-sn 3599  df-pr 3600  df-op 3602  df-uni 3811  df-br 4005  df-iota 5179  df-fv 5225  df-ov 5878

This theorem is referenced by:  oveq12  5884  oveq1i  5885  oveq1d  5890  ovrspc2v  5901  oveqrspc2v  5902  rspceov  5917  fovcl  5980  ovmpos  5998  ov2gf  5999  ovi3  6011  caovclg  6027  caovcomg  6030  caovassg  6033  caovcang  6036  caovcan  6039  caovordig  6040  caovordg  6042  caovord  6046  caovdig  6049  caovdirg  6052  caovimo  6068  suppssov1  6080  off  6095  omcl  6462  oeicl  6463  omv2  6466  nnm0r  6480  nnacom  6485  nndi  6487  nnmass  6488  nnmsucr  6489  nnmcom  6490  nnaword  6512  nnmord  6518  nnm00  6531  eroveu  6626  th3qlem2  6638  th3q  6640  ecovcom  6642  ecovicom  6643  ecovass  6644  ecoviass  6645  ecovdi  6646  ecovidi  6647  map0g  6688  addcmpblnq  7366  addclnq  7374  mulclnq  7375  mulidnq  7388  recexnq  7389  recmulnqg  7390  ltanqg  7399  ltmnqg  7400  ltexnqq  7407  enq0ref  7432  enq0tr  7433  addcmpblnq0  7442  mulnnnq0  7449  addclnq0  7450  mulclnq0  7451  distrnq0  7458  mulcomnq0  7459  addassnq0  7461  prarloclemlo  7493  prarloclem3  7496  prarloclem5  7499  prarloclemcalc  7501  genipv  7508  genpassl  7523  genpassu  7524  addlocprlemeq  7532  distrlem4prl  7583  distrlem4pru  7584  ltexprlemdisj  7605  ltexprlemloc  7606  ltexprlemrl  7609  ltexprlemru  7611  prplnqu  7619  cauappcvgprlemm  7644  cauappcvgprlemopl  7645  cauappcvgprlemlol  7646  cauappcvgprlemdisj  7650  cauappcvgprlemloc  7651  cauappcvgprlemladdfl  7654  cauappcvgprlemladdru  7655  cauappcvgprlemladdrl  7656  cauappcvgprlem1  7658  cauappcvgprlemlim  7660  cauappcvgpr  7661  caucvgprlemm  7667  caucvgprlemopl  7668  caucvgprlemlol  7669  caucvgprlemdisj  7673  caucvgprlemloc  7674  caucvgprlemladdrl  7677  caucvgprlem1  7678  caucvgpr  7681  caucvgprprlemell  7684  caucvgprprlemml  7693  caucvgprpr  7711  mulcmpblnrlemg  7739  addclsr  7752  mulclsr  7753  0idsr  7766  1idsr  7767  00sr  7768  ltasrg  7769  recexgt0sr  7772  mulgt0sr  7777  mulextsr1  7780  prsrriota  7787  caucvgsrlemgt1  7794  caucvgsrlemoffres  7799  pitonn  7847  peano2nnnn  7852  axaddrcl  7864  axmulrcl  7866  axaddcom  7869  ax1rid  7876  ax0id  7877  axprecex  7879  axcnre  7880  axpre-ltadd  7885  axpre-mulgt0  7886  axpre-mulext  7887  rereceu  7888  peano5nnnn  7891  axcaucvglemcau  7897  axcaucvglemres  7898  mulrid  7954  cnegexlem1  8132  cnegexlem2  8133  cnegex  8135  addcan2  8138  subval  8149  addlsub  8327  apreim  8560  recexap  8610  receuap  8626  divvalap  8631  cju  8918  peano2nn  8931  nn1m1nn  8937  nn1suc  8938  nnsub  8958  fv0p1e1  9034  nnm1nn0  9217  zdiv  9341  zneo  9354  nneoor  9355  zeo  9358  peano5uzti  9361  nn0ind-raph  9370  uzind4s  9590  uzind4s2  9591  qmulz  9623  elpq  9648  cnref1o  9650  nn0ledivnn  9767  xaddnemnf  9857  xaddnepnf  9858  xaddcom  9861  xaddid1  9862  xnn0xadd0  9867  xaddass  9869  xpncan  9871  xleadd1a  9873  xltadd1  9876  xlt2add  9880  xsubge0  9881  xposdif  9882  xlesubadd  9883  xleaddadd  9887  fzsuc2  10079  fzm1  10100  fzoval  10148  exbtwnzlemstep  10248  exbtwnzlemshrink  10249  exbtwnzlemex  10250  exbtwnz  10251  rebtwn2zlemstep  10253  rebtwn2zlemshrink  10254  rebtwn2z  10255  flqlelt  10276  flqbi  10290  fldiv4p1lem1div2  10305  modqval  10324  modqadd1  10361  modqmuladd  10366  modqmuladdnn0  10368  modqm1p1mod0  10375  modqmul1  10377  modfzo0difsn  10395  addmodlteq  10398  frec2uzzd  10400  frec2uzsucd  10401  frec2uzrand  10405  frecuzrdgrrn  10408  frec2uzrdg  10409  frecuzrdgrcl  10410  frecuzrdgsuc  10414  frecuzrdgrclt  10415  frecuzrdgg  10416  frecuzrdgdom  10418  frecuzrdgfun  10420  frecuzrdgsuctlem  10423  frecuzrdgsuct  10424  uzsinds  10442  iseqvalcbv  10457  seq3val  10458  seqvalcd  10459  seqf  10461  seq3p1  10462  seqovcd  10463  seqp1cd  10466  seq3fveq2  10469  seq3shft2  10473  monoord  10476  monoord2  10477  seq3split  10479  seq3caopr3  10481  seq3caopr2  10482  iseqf1olemqval  10487  iseqf1olemqk  10494  seq3id2  10509  seq3homo  10510  seq3z  10511  seq3distr  10513  m1expcl2  10542  mulexp  10559  expadd  10562  expmul  10565  sq0i  10612  qsqeqor  10631  sqoddm1div8  10674  facp1  10710  faclbnd  10721  faclbnd3  10723  bcval  10729  bcn1  10738  bcval5  10743  bcpasc  10746  bccl  10747  hashfz1  10763  omgadd  10782  hashfzo  10802  hashfzp1  10804  hashxp  10806  seq3coll  10822  shftlem  10825  shftfvalg  10827  shftfibg  10829  shftfval  10830  shftfib  10832  shftfn  10833  shftf  10839  2shfti  10840  shftvalg  10845  shftval4g  10846  cjval  10854  imval  10859  cjexp  10902  cnrecnv  10919  cvg1nlemcau  10993  cvg1nlemres  10994  resqrexlemcalc3  11025  resqrexlemex  11034  rsqrmo  11036  resqrtcl  11038  rersqrtthlem  11039  sqrtsq  11053  absexp  11088  recan  11118  climshft  11312  climcn1  11316  climcn2  11317  subcn2  11319  fsumshft  11452  fisum0diag2  11455  fsumiun  11485  binomlem  11491  binom  11492  bcxmas  11497  isumsplit  11499  arisum2  11507  trireciplem  11508  trirecip  11509  geolim  11519  cvgratnnlemnexp  11532  cvgratnnlemmn  11533  clim2prod  11547  prodfrecap  11554  fprodcl2lem  11613  fprodfac  11623  fprodshft  11626  ef0lem  11668  efval  11669  efne0  11686  efexp  11690  demoivreALT  11781  dvdsval2  11797  p1modz1  11801  dvds0lem  11808  dvds1lem  11809  dvds2lem  11810  dvdsmulc  11826  divconjdvds  11855  odd2np1lem  11877  odd2np1  11878  ltoddhalfle  11898  halfleoddlt  11899  nn0o1gt2  11910  nn0o  11912  divalglemnn  11923  divalglemeunn  11926  divalglemex  11927  divalglemeuneg  11928  flodddiv4  11939  gcdabs1  11990  gcddiv  12020  dvdssqim  12025  rpmulgcd  12027  bezoutr1  12034  uzwodc  12038  dvdslcm  12069  lcmeq0  12071  lcmdvds  12079  divgcdcoprm0  12101  prmind2  12120  isprm5lem  12141  isprm6  12147  rpexp  12153  sqrt2irr  12162  pw2dvdslemn  12165  pw2dvdseu  12168  oddpwdclemxy  12169  nn0gcdsq  12200  phicl2  12214  phibndlem  12216  hashdvds  12221  crth  12224  phimullem  12225  eulerthlem1  12227  eulerthlemfi  12228  eulerthlemrprm  12229  eulerthlemth  12232  eulerth  12233  hashgcdlem  12238  phisum  12240  odzval  12241  modprm0  12254  nnnn0modprm0  12255  pythagtriplem1  12265  pythagtriplem6  12270  pythagtriplem7  12271  pythagtriplem12  12275  pythagtriplem14  12277  pythagtriplem18  12281  pythagtriplem19  12282  pceulem  12294  pceu  12295  pcval  12296  pczpre  12297  pcdiv  12302  pcqmul  12303  pcqcl  12306  pcexp  12309  pcaddlem  12338  pcadd  12339  pcmpt  12341  pcprod  12344  pcfac  12348  expnprm  12351  prmpwdvds  12353  pockthi  12356  1arithlem2  12362  4sqlem2  12387  4sqlem3  12388  ennnfonelemr  12424  ctinfom  12429  infpn2  12457  ercpbl  12750  mgm1  12789  mgmidmo  12791  ismgmid  12796  mgmlrid  12798  ismgmid2  12799  lidrideqd  12800  lidrididd  12801  mgmidsssn0  12803  grpridd  12806  isnsgrp  12812  sgrpass  12814  sgrp1  12816  sgrpidmndm  12821  ismndd  12838  mndinvmod  12846  mnd1  12847  mnd1id  12848  mhmpropd  12857  insubm  12872  mhmima  12875  grppropd  12893  isgrpd2  12897  isgrpd  12899  dfgrp2  12902  grprcan  12910  grpinveu  12911  grpsubval  12919  grplinv  12922  grpinvid2  12925  isgrpinv  12926  grplrinv  12927  grpidinv2  12928  grpidinv  12929  grpidssd  12946  grpinvssd  12947  dfgrp3mlem  12968  dfgrp3m  12969  grplactfval  12971  grp1  12976  mhmmnd  12980  ghmgrp  12982  mulgnn0p1  12994  mulgnn0subcl  12996  mulgaddcom  13007  mulginvcom  13008  mulgnn0z  13010  mulgneg2  13017  mulgnnass  13018  mulgnn0ass  13019  mhmmulg  13024  issubg  13033  subgex  13036  issubg2m  13049  issubg4m  13053  isnsg2  13063  nsgbi  13064  isnsg3  13067  elnmz  13068  nmzbi  13069  srgrz  13167  srgmulgass  13172  srgpcomp  13173  srgrmhm  13177  ringid  13209  ringinvnzdiv  13227  mulgass2  13235  ring1  13236  dvdsrmuld  13265  dvdsrmul1  13271  dvdsr01  13273  dvreq1  13311  lringuplu  13337  issubrg  13342  issubrg2  13362  lmodlema  13382  islmodd  13383  lmodvsmmulgdi  13413  rmodislmodlem  13440  rmodislmod  13441  cnfldmulg  13473  cnfldexp  13474  cnmptcom  13801  psmettri2  13831  isxmet2d  13851  xmeteq0  13862  xmettri2  13864  metrest  14009  cncfval  14062  mulc1cncf  14079  addccncf  14089  mulcncf  14094  expcncf  14095  limccnp2lem  14148  dvcnp2cntop  14166  dvcoapbr  14174  dvexp  14178  dvrecap  14180  dvef  14191  sincn  14193  coscn  14194  ptolemy  14248  sincosq1eq  14263  logbgcd1irr  14388  logbgcd1irraplemexp  14389  2irrexpq  14397  2irrexpqap  14399  lgslem4  14407  lgsval  14408  lgsfvalg  14409  lgsval2lem  14414  lgsdir2lem4  14435  lgsdir  14439  lgsdilem2  14440  lgsdi  14441  lgsne0  14442  lgsmodeq  14449  lgsdirnn0  14451  lgsdinn0  14452  lgseisenlem2  14454  2lgsoddprmlem1  14456  2lgsoddprmlem3  14462  2sqlem2  14465  2sqlem6  14470  2sqlem8  14473  2sqlem9  14474  qdencn  14778  isomninn  14782  trirec0  14795  iswomninn  14801  ismkvnn  14804