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  7175  addclnq  7183  mulclnq  7184  mulidnq  7197  recexnq  7198  recmulnqg  7199  ltanqg  7208  ltmnqg  7209  ltexnqq  7216  enq0ref  7241  enq0tr  7242  addcmpblnq0  7251  mulnnnq0  7258  addclnq0  7259  mulclnq0  7260  distrnq0  7267  mulcomnq0  7268  addassnq0  7270  prarloclemlo  7302  prarloclem3  7305  prarloclem5  7308  prarloclemcalc  7310  genipv  7317  genpassl  7332  genpassu  7333  addlocprlemeq  7341  distrlem4prl  7392  distrlem4pru  7393  ltexprlemdisj  7414  ltexprlemloc  7415  ltexprlemrl  7418  ltexprlemru  7420  prplnqu  7428  cauappcvgprlemm  7453  cauappcvgprlemopl  7454  cauappcvgprlemlol  7455  cauappcvgprlemdisj  7459  cauappcvgprlemloc  7460  cauappcvgprlemladdfl  7463  cauappcvgprlemladdru  7464  cauappcvgprlemladdrl  7465  cauappcvgprlem1  7467  cauappcvgprlemlim  7469  cauappcvgpr  7470  caucvgprlemm  7476  caucvgprlemopl  7477  caucvgprlemlol  7478  caucvgprlemdisj  7482  caucvgprlemloc  7483  caucvgprlemladdrl  7486  caucvgprlem1  7487  caucvgpr  7490  caucvgprprlemell  7493  caucvgprprlemml  7502  caucvgprpr  7520  mulcmpblnrlemg  7548  addclsr  7561  mulclsr  7562  0idsr  7575  1idsr  7576  00sr  7577  ltasrg  7578  recexgt0sr  7581  mulgt0sr  7586  mulextsr1  7589  prsrriota  7596  caucvgsrlemgt1  7603  caucvgsrlemoffres  7608  pitonn  7656  peano2nnnn  7661  axaddrcl  7673  axmulrcl  7675  axaddcom  7678  ax1rid  7685  ax0id  7686  axprecex  7688  axcnre  7689  axpre-ltadd  7694  axpre-mulgt0  7695  axpre-mulext  7696  rereceu  7697  peano5nnnn  7700  axcaucvglemcau  7706  axcaucvglemres  7707  mulid1  7763  cnegexlem1  7937  cnegexlem2  7938  cnegex  7940  addcan2  7943  subval  7954  addlsub  8132  apreim  8365  recexap  8414  receuap  8430  divvalap  8434  cju  8719  peano2nn  8732  nn1m1nn  8738  nn1suc  8739  nnsub  8759  fv0p1e1  8835  nnm1nn0  9018  zdiv  9139  zneo  9152  nneoor  9153  zeo  9156  peano5uzti  9159  nn0ind-raph  9168  uzind4s  9385  uzind4s2  9386  qmulz  9415  cnref1o  9440  nn0ledivnn  9554  xaddnemnf  9640  xaddnepnf  9641  xaddcom  9644  xaddid1  9645  xnn0xadd0  9650  xaddass  9652  xpncan  9654  xleadd1a  9656  xltadd1  9659  xlt2add  9663  xsubge0  9664  xposdif  9665  xlesubadd  9666  xleaddadd  9670  fzsuc2  9859  fzm1  9880  fzoval  9925  exbtwnzlemstep  10025  exbtwnzlemshrink  10026  exbtwnzlemex  10027  exbtwnz  10028  rebtwn2zlemstep  10030  rebtwn2zlemshrink  10031  rebtwn2z  10032  flqlelt  10049  flqbi  10063  fldiv4p1lem1div2  10078  modqval  10097  modqadd1  10134  modqmuladd  10139  modqmuladdnn0  10141  modqm1p1mod0  10148  modqmul1  10150  modfzo0difsn  10168  addmodlteq  10171  frec2uzzd  10173  frec2uzsucd  10174  frec2uzrand  10178  frecuzrdgrrn  10181  frec2uzrdg  10182  frecuzrdgrcl  10183  frecuzrdgsuc  10187  frecuzrdgrclt  10188  frecuzrdgg  10189  frecuzrdgdom  10191  frecuzrdgfun  10193  frecuzrdgsuctlem  10196  frecuzrdgsuct  10197  uzsinds  10215  iseqvalcbv  10230  seq3val  10231  seqvalcd  10232  seqf  10234  seq3p1  10235  seqovcd  10236  seqp1cd  10239  seq3fveq2  10242  seq3shft2  10246  monoord  10249  monoord2  10250  seq3split  10252  seq3caopr3  10254  seq3caopr2  10255  iseqf1olemqval  10260  iseqf1olemqk  10267  seq3id2  10282  seq3homo  10283  seq3z  10284  seq3distr  10286  m1expcl2  10315  mulexp  10332  expadd  10335  expmul  10338  sq0i  10384  sqoddm1div8  10444  facp1  10476  faclbnd  10487  faclbnd3  10489  bcval  10495  bcn1  10504  bcval5  10509  bcpasc  10512  bccl  10513  hashfz1  10529  omgadd  10548  hashfzo  10568  hashfzp1  10570  hashxp  10572  seq3coll  10585  shftlem  10588  shftfvalg  10590  shftfibg  10592  shftfval  10593  shftfib  10595  shftfn  10596  shftf  10602  2shfti  10603  shftvalg  10608  shftval4g  10609  cjval  10617  imval  10622  cjexp  10665  cnrecnv  10682  cvg1nlemcau  10756  cvg1nlemres  10757  resqrexlemcalc3  10788  resqrexlemex  10797  rsqrmo  10799  resqrtcl  10801  rersqrtthlem  10802  sqrtsq  10816  absexp  10851  recan  10881  climshft  11073  climcn1  11077  climcn2  11078  subcn2  11080  fsumshft  11213  fisum0diag2  11216  fsumiun  11246  binomlem  11252  binom  11253  bcxmas  11258  isumsplit  11260  arisum2  11268  trireciplem  11269  trirecip  11270  geolim  11280  cvgratnnlemnexp  11293  cvgratnnlemmn  11294  clim2prod  11308  prodfrecap  11315  ef0lem  11366  efval  11367  efne0  11384  efexp  11388  demoivreALT  11480  dvdsval2  11496  dvds0lem  11503  dvds1lem  11504  dvds2lem  11505  dvdsmulc  11521  divconjdvds  11547  odd2np1lem  11569  odd2np1  11570  ltoddhalfle  11590  halfleoddlt  11591  nn0o1gt2  11602  nn0o  11604  divalglemnn  11615  divalglemeunn  11618  divalglemex  11619  divalglemeuneg  11620  flodddiv4  11631  gcdabs1  11677  gcddiv  11707  dvdssqim  11712  rpmulgcd  11714  bezoutr1  11721  dvdslcm  11750  lcmeq0  11752  lcmdvds  11760  divgcdcoprm0  11782  prmind2  11801  isprm6  11825  rpexp  11831  sqrt2irr  11840  pw2dvdslemn  11843  pw2dvdseu  11846  oddpwdclemxy  11847  nn0gcdsq  11878  phicl2  11890  phibndlem  11892  hashdvds  11897  crth  11900  phimullem  11901  hashgcdlem  11903  ennnfonelemr  11936  ctinfom  11941  cnmptcom  12467  psmettri2  12497  isxmet2d  12517  xmeteq0  12528  xmettri2  12530  metrest  12675  cncfval  12728  mulc1cncf  12745  addccncf  12755  mulcncf  12760  expcncf  12761  limccnp2lem  12814  dvcnp2cntop  12832  dvcoapbr  12840  dvexp  12844  dvrecap  12846  dvef  12856  sincn  12858  coscn  12859  ptolemy  12905  sincosq1eq  12920  qdencn  13222  isomninn  13226