Theorem oveq1 5781

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 3705	. . 3 |- ( A = B -> <. A , C >. = <. B , C >. )
2	1	fveq2d 5425	. 2 |- ( A = B -> ( F ` <. A , C >. ) = ( F ` <. B , C >. ) )
3		df-ov 5777	. 2 |- ( A F C ) = ( F ` <. A , C >. )
4		df-ov 5777	. 2 |- ( B F C ) = ( F ` <. B , C >. )
5	2, 3, 4	3eqtr4g 2197	1 |- ( A = B -> ( A F C ) = ( B F C ) )

Syntax hints:   -> wi 4   = wceq 1331   <.cop 3530   ` cfv 5123  (class class class)co 5774

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-ia1 105  ax-ia2 106  ax-ia3 107  ax-io 698  ax-5 1423  ax-7 1424  ax-gen 1425  ax-ie1 1469  ax-ie2 1470  ax-8 1482  ax-10 1483  ax-11 1484  ax-i12 1485  ax-bndl 1486  ax-4 1487  ax-17 1506  ax-i9 1510  ax-ial 1514  ax-i5r 1515  ax-ext 2121

This theorem depends on definitions:  df-bi 116  df-3an 964  df-tru 1334  df-nf 1437  df-sb 1736  df-clab 2126  df-cleq 2132  df-clel 2135  df-nfc 2270  df-rex 2422  df-v 2688  df-un 3075  df-sn 3533  df-pr 3534  df-op 3536  df-uni 3737  df-br 3930  df-iota 5088  df-fv 5131  df-ov 5777

This theorem is referenced by:  oveq12  5783  oveq1i  5784  oveq1d  5789  rspceov  5813  fovcl  5876  ovmpos  5894  ov2gf  5895  ovi3  5907  caovclg  5923  caovcomg  5926  caovassg  5929  caovcang  5932  caovcan  5935  caovordig  5936  caovordg  5938  caovord  5942  caovdig  5945  caovdirg  5948  caovimo  5964  grpridd  5967  suppssov1  5979  off  5994  omcl  6357  oeicl  6358  omv2  6361  nnm0r  6375  nnacom  6380  nndi  6382  nnmass  6383  nnmsucr  6384  nnmcom  6385  nnaword  6407  nnmord  6413  nnm00  6425  eroveu  6520  th3qlem2  6532  th3q  6534  ecovcom  6536  ecovicom  6537  ecovass  6538  ecoviass  6539  ecovdi  6540  ecovidi  6541  map0g  6582  addcmpblnq  7182  addclnq  7190  mulclnq  7191  mulidnq  7204  recexnq  7205  recmulnqg  7206  ltanqg  7215  ltmnqg  7216  ltexnqq  7223  enq0ref  7248  enq0tr  7249  addcmpblnq0  7258  mulnnnq0  7265  addclnq0  7266  mulclnq0  7267  distrnq0  7274  mulcomnq0  7275  addassnq0  7277  prarloclemlo  7309  prarloclem3  7312  prarloclem5  7315  prarloclemcalc  7317  genipv  7324  genpassl  7339  genpassu  7340  addlocprlemeq  7348  distrlem4prl  7399  distrlem4pru  7400  ltexprlemdisj  7421  ltexprlemloc  7422  ltexprlemrl  7425  ltexprlemru  7427  prplnqu  7435  cauappcvgprlemm  7460  cauappcvgprlemopl  7461  cauappcvgprlemlol  7462  cauappcvgprlemdisj  7466  cauappcvgprlemloc  7467  cauappcvgprlemladdfl  7470  cauappcvgprlemladdru  7471  cauappcvgprlemladdrl  7472  cauappcvgprlem1  7474  cauappcvgprlemlim  7476  cauappcvgpr  7477  caucvgprlemm  7483  caucvgprlemopl  7484  caucvgprlemlol  7485  caucvgprlemdisj  7489  caucvgprlemloc  7490  caucvgprlemladdrl  7493  caucvgprlem1  7494  caucvgpr  7497  caucvgprprlemell  7500  caucvgprprlemml  7509  caucvgprpr  7527  mulcmpblnrlemg  7555  addclsr  7568  mulclsr  7569  0idsr  7582  1idsr  7583  00sr  7584  ltasrg  7585  recexgt0sr  7588  mulgt0sr  7593  mulextsr1  7596  prsrriota  7603  caucvgsrlemgt1  7610  caucvgsrlemoffres  7615  pitonn  7663  peano2nnnn  7668  axaddrcl  7680  axmulrcl  7682  axaddcom  7685  ax1rid  7692  ax0id  7693  axprecex  7695  axcnre  7696  axpre-ltadd  7701  axpre-mulgt0  7702  axpre-mulext  7703  rereceu  7704  peano5nnnn  7707  axcaucvglemcau  7713  axcaucvglemres  7714  mulid1  7770  cnegexlem1  7944  cnegexlem2  7945  cnegex  7947  addcan2  7950  subval  7961  addlsub  8139  apreim  8372  recexap  8421  receuap  8437  divvalap  8441  cju  8726  peano2nn  8739  nn1m1nn  8745  nn1suc  8746  nnsub  8766  fv0p1e1  8842  nnm1nn0  9025  zdiv  9146  zneo  9159  nneoor  9160  zeo  9163  peano5uzti  9166  nn0ind-raph  9175  uzind4s  9392  uzind4s2  9393  qmulz  9422  cnref1o  9447  nn0ledivnn  9561  xaddnemnf  9647  xaddnepnf  9648  xaddcom  9651  xaddid1  9652  xnn0xadd0  9657  xaddass  9659  xpncan  9661  xleadd1a  9663  xltadd1  9666  xlt2add  9670  xsubge0  9671  xposdif  9672  xlesubadd  9673  xleaddadd  9677  fzsuc2  9866  fzm1  9887  fzoval  9932  exbtwnzlemstep  10032  exbtwnzlemshrink  10033  exbtwnzlemex  10034  exbtwnz  10035  rebtwn2zlemstep  10037  rebtwn2zlemshrink  10038  rebtwn2z  10039  flqlelt  10056  flqbi  10070  fldiv4p1lem1div2  10085  modqval  10104  modqadd1  10141  modqmuladd  10146  modqmuladdnn0  10148  modqm1p1mod0  10155  modqmul1  10157  modfzo0difsn  10175  addmodlteq  10178  frec2uzzd  10180  frec2uzsucd  10181  frec2uzrand  10185  frecuzrdgrrn  10188  frec2uzrdg  10189  frecuzrdgrcl  10190  frecuzrdgsuc  10194  frecuzrdgrclt  10195  frecuzrdgg  10196  frecuzrdgdom  10198  frecuzrdgfun  10200  frecuzrdgsuctlem  10203  frecuzrdgsuct  10204  uzsinds  10222  iseqvalcbv  10237  seq3val  10238  seqvalcd  10239  seqf  10241  seq3p1  10242  seqovcd  10243  seqp1cd  10246  seq3fveq2  10249  seq3shft2  10253  monoord  10256  monoord2  10257  seq3split  10259  seq3caopr3  10261  seq3caopr2  10262  iseqf1olemqval  10267  iseqf1olemqk  10274  seq3id2  10289  seq3homo  10290  seq3z  10291  seq3distr  10293  m1expcl2  10322  mulexp  10339  expadd  10342  expmul  10345  sq0i  10391  sqoddm1div8  10451  facp1  10483  faclbnd  10494  faclbnd3  10496  bcval  10502  bcn1  10511  bcval5  10516  bcpasc  10519  bccl  10520  hashfz1  10536  omgadd  10555  hashfzo  10575  hashfzp1  10577  hashxp  10579  seq3coll  10592  shftlem  10595  shftfvalg  10597  shftfibg  10599  shftfval  10600  shftfib  10602  shftfn  10603  shftf  10609  2shfti  10610  shftvalg  10615  shftval4g  10616  cjval  10624  imval  10629  cjexp  10672  cnrecnv  10689  cvg1nlemcau  10763  cvg1nlemres  10764  resqrexlemcalc3  10795  resqrexlemex  10804  rsqrmo  10806  resqrtcl  10808  rersqrtthlem  10809  sqrtsq  10823  absexp  10858  recan  10888  climshft  11080  climcn1  11084  climcn2  11085  subcn2  11087  fsumshft  11220  fisum0diag2  11223  fsumiun  11253  binomlem  11259  binom  11260  bcxmas  11265  isumsplit  11267  arisum2  11275  trireciplem  11276  trirecip  11277  geolim  11287  cvgratnnlemnexp  11300  cvgratnnlemmn  11301  clim2prod  11315  prodfrecap  11322  ef0lem  11373  efval  11374  efne0  11391  efexp  11395  demoivreALT  11487  dvdsval2  11503  dvds0lem  11510  dvds1lem  11511  dvds2lem  11512  dvdsmulc  11528  divconjdvds  11554  odd2np1lem  11576  odd2np1  11577  ltoddhalfle  11597  halfleoddlt  11598  nn0o1gt2  11609  nn0o  11611  divalglemnn  11622  divalglemeunn  11625  divalglemex  11626  divalglemeuneg  11627  flodddiv4  11638  gcdabs1  11684  gcddiv  11714  dvdssqim  11719  rpmulgcd  11721  bezoutr1  11728  dvdslcm  11757  lcmeq0  11759  lcmdvds  11767  divgcdcoprm0  11789  prmind2  11808  isprm6  11832  rpexp  11838  sqrt2irr  11847  pw2dvdslemn  11850  pw2dvdseu  11853  oddpwdclemxy  11854  nn0gcdsq  11885  phicl2  11897  phibndlem  11899  hashdvds  11904  crth  11907  phimullem  11908  hashgcdlem  11910  ennnfonelemr  11943  ctinfom  11948  cnmptcom  12477  psmettri2  12507  isxmet2d  12527  xmeteq0  12538  xmettri2  12540  metrest  12685  cncfval  12738  mulc1cncf  12755  addccncf  12765  mulcncf  12770  expcncf  12771  limccnp2lem  12824  dvcnp2cntop  12842  dvcoapbr  12850  dvexp  12854  dvrecap  12856  dvef  12866  sincn  12868  coscn  12869  ptolemy  12915  sincosq1eq  12930  qdencn  13232  isomninn  13236