Theorem oveq1 5789

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 3713	. . 3 |- ( A = B -> <. A , C >. = <. B , C >. )
2	1	fveq2d 5433	. 2 |- ( A = B -> ( F ` <. A , C >. ) = ( F ` <. B , C >. ) )
3		df-ov 5785	. 2 |- ( A F C ) = ( F ` <. A , C >. )
4		df-ov 5785	. 2 |- ( B F C ) = ( F ` <. B , C >. )
5	2, 3, 4	3eqtr4g 2198	1 |- ( A = B -> ( A F C ) = ( B F C ) )

Syntax hints:   -> wi 4   = wceq 1332   <.cop 3535   ` cfv 5131  (class class class)co 5782

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 699  ax-5 1424  ax-7 1425  ax-gen 1426  ax-ie1 1470  ax-ie2 1471  ax-8 1483  ax-10 1484  ax-11 1485  ax-i12 1486  ax-bndl 1487  ax-4 1488  ax-17 1507  ax-i9 1511  ax-ial 1515  ax-i5r 1516  ax-ext 2122

This theorem depends on definitions:  df-bi 116  df-3an 965  df-tru 1335  df-nf 1438  df-sb 1737  df-clab 2127  df-cleq 2133  df-clel 2136  df-nfc 2271  df-rex 2423  df-v 2691  df-un 3080  df-sn 3538  df-pr 3539  df-op 3541  df-uni 3745  df-br 3938  df-iota 5096  df-fv 5139  df-ov 5785

This theorem is referenced by:  oveq12  5791  oveq1i  5792  oveq1d  5797  rspceov  5821  fovcl  5884  ovmpos  5902  ov2gf  5903  ovi3  5915  caovclg  5931  caovcomg  5934  caovassg  5937  caovcang  5940  caovcan  5943  caovordig  5944  caovordg  5946  caovord  5950  caovdig  5953  caovdirg  5956  caovimo  5972  grpridd  5975  suppssov1  5987  off  6002  omcl  6365  oeicl  6366  omv2  6369  nnm0r  6383  nnacom  6388  nndi  6390  nnmass  6391  nnmsucr  6392  nnmcom  6393  nnaword  6415  nnmord  6421  nnm00  6433  eroveu  6528  th3qlem2  6540  th3q  6542  ecovcom  6544  ecovicom  6545  ecovass  6546  ecoviass  6547  ecovdi  6548  ecovidi  6549  map0g  6590  addcmpblnq  7199  addclnq  7207  mulclnq  7208  mulidnq  7221  recexnq  7222  recmulnqg  7223  ltanqg  7232  ltmnqg  7233  ltexnqq  7240  enq0ref  7265  enq0tr  7266  addcmpblnq0  7275  mulnnnq0  7282  addclnq0  7283  mulclnq0  7284  distrnq0  7291  mulcomnq0  7292  addassnq0  7294  prarloclemlo  7326  prarloclem3  7329  prarloclem5  7332  prarloclemcalc  7334  genipv  7341  genpassl  7356  genpassu  7357  addlocprlemeq  7365  distrlem4prl  7416  distrlem4pru  7417  ltexprlemdisj  7438  ltexprlemloc  7439  ltexprlemrl  7442  ltexprlemru  7444  prplnqu  7452  cauappcvgprlemm  7477  cauappcvgprlemopl  7478  cauappcvgprlemlol  7479  cauappcvgprlemdisj  7483  cauappcvgprlemloc  7484  cauappcvgprlemladdfl  7487  cauappcvgprlemladdru  7488  cauappcvgprlemladdrl  7489  cauappcvgprlem1  7491  cauappcvgprlemlim  7493  cauappcvgpr  7494  caucvgprlemm  7500  caucvgprlemopl  7501  caucvgprlemlol  7502  caucvgprlemdisj  7506  caucvgprlemloc  7507  caucvgprlemladdrl  7510  caucvgprlem1  7511  caucvgpr  7514  caucvgprprlemell  7517  caucvgprprlemml  7526  caucvgprpr  7544  mulcmpblnrlemg  7572  addclsr  7585  mulclsr  7586  0idsr  7599  1idsr  7600  00sr  7601  ltasrg  7602  recexgt0sr  7605  mulgt0sr  7610  mulextsr1  7613  prsrriota  7620  caucvgsrlemgt1  7627  caucvgsrlemoffres  7632  pitonn  7680  peano2nnnn  7685  axaddrcl  7697  axmulrcl  7699  axaddcom  7702  ax1rid  7709  ax0id  7710  axprecex  7712  axcnre  7713  axpre-ltadd  7718  axpre-mulgt0  7719  axpre-mulext  7720  rereceu  7721  peano5nnnn  7724  axcaucvglemcau  7730  axcaucvglemres  7731  mulid1  7787  cnegexlem1  7961  cnegexlem2  7962  cnegex  7964  addcan2  7967  subval  7978  addlsub  8156  apreim  8389  recexap  8438  receuap  8454  divvalap  8458  cju  8743  peano2nn  8756  nn1m1nn  8762  nn1suc  8763  nnsub  8783  fv0p1e1  8859  nnm1nn0  9042  zdiv  9163  zneo  9176  nneoor  9177  zeo  9180  peano5uzti  9183  nn0ind-raph  9192  uzind4s  9412  uzind4s2  9413  qmulz  9442  elpq  9467  cnref1o  9469  nn0ledivnn  9584  xaddnemnf  9670  xaddnepnf  9671  xaddcom  9674  xaddid1  9675  xnn0xadd0  9680  xaddass  9682  xpncan  9684  xleadd1a  9686  xltadd1  9689  xlt2add  9693  xsubge0  9694  xposdif  9695  xlesubadd  9696  xleaddadd  9700  fzsuc2  9890  fzm1  9911  fzoval  9956  exbtwnzlemstep  10056  exbtwnzlemshrink  10057  exbtwnzlemex  10058  exbtwnz  10059  rebtwn2zlemstep  10061  rebtwn2zlemshrink  10062  rebtwn2z  10063  flqlelt  10080  flqbi  10094  fldiv4p1lem1div2  10109  modqval  10128  modqadd1  10165  modqmuladd  10170  modqmuladdnn0  10172  modqm1p1mod0  10179  modqmul1  10181  modfzo0difsn  10199  addmodlteq  10202  frec2uzzd  10204  frec2uzsucd  10205  frec2uzrand  10209  frecuzrdgrrn  10212  frec2uzrdg  10213  frecuzrdgrcl  10214  frecuzrdgsuc  10218  frecuzrdgrclt  10219  frecuzrdgg  10220  frecuzrdgdom  10222  frecuzrdgfun  10224  frecuzrdgsuctlem  10227  frecuzrdgsuct  10228  uzsinds  10246  iseqvalcbv  10261  seq3val  10262  seqvalcd  10263  seqf  10265  seq3p1  10266  seqovcd  10267  seqp1cd  10270  seq3fveq2  10273  seq3shft2  10277  monoord  10280  monoord2  10281  seq3split  10283  seq3caopr3  10285  seq3caopr2  10286  iseqf1olemqval  10291  iseqf1olemqk  10298  seq3id2  10313  seq3homo  10314  seq3z  10315  seq3distr  10317  m1expcl2  10346  mulexp  10363  expadd  10366  expmul  10369  sq0i  10415  sqoddm1div8  10475  facp1  10508  faclbnd  10519  faclbnd3  10521  bcval  10527  bcn1  10536  bcval5  10541  bcpasc  10544  bccl  10545  hashfz1  10561  omgadd  10580  hashfzo  10600  hashfzp1  10602  hashxp  10604  seq3coll  10617  shftlem  10620  shftfvalg  10622  shftfibg  10624  shftfval  10625  shftfib  10627  shftfn  10628  shftf  10634  2shfti  10635  shftvalg  10640  shftval4g  10641  cjval  10649  imval  10654  cjexp  10697  cnrecnv  10714  cvg1nlemcau  10788  cvg1nlemres  10789  resqrexlemcalc3  10820  resqrexlemex  10829  rsqrmo  10831  resqrtcl  10833  rersqrtthlem  10834  sqrtsq  10848  absexp  10883  recan  10913  climshft  11105  climcn1  11109  climcn2  11110  subcn2  11112  fsumshft  11245  fisum0diag2  11248  fsumiun  11278  binomlem  11284  binom  11285  bcxmas  11290  isumsplit  11292  arisum2  11300  trireciplem  11301  trirecip  11302  geolim  11312  cvgratnnlemnexp  11325  cvgratnnlemmn  11326  clim2prod  11340  prodfrecap  11347  ef0lem  11403  efval  11404  efne0  11421  efexp  11425  demoivreALT  11516  dvdsval2  11532  dvds0lem  11539  dvds1lem  11540  dvds2lem  11541  dvdsmulc  11557  divconjdvds  11583  odd2np1lem  11605  odd2np1  11606  ltoddhalfle  11626  halfleoddlt  11627  nn0o1gt2  11638  nn0o  11640  divalglemnn  11651  divalglemeunn  11654  divalglemex  11655  divalglemeuneg  11656  flodddiv4  11667  gcdabs1  11713  gcddiv  11743  dvdssqim  11748  rpmulgcd  11750  bezoutr1  11757  dvdslcm  11786  lcmeq0  11788  lcmdvds  11796  divgcdcoprm0  11818  prmind2  11837  isprm6  11861  rpexp  11867  sqrt2irr  11876  pw2dvdslemn  11879  pw2dvdseu  11882  oddpwdclemxy  11883  nn0gcdsq  11914  phicl2  11926  phibndlem  11928  hashdvds  11933  crth  11936  phimullem  11937  hashgcdlem  11939  ennnfonelemr  11972  ctinfom  11977  cnmptcom  12506  psmettri2  12536  isxmet2d  12556  xmeteq0  12567  xmettri2  12569  metrest  12714  cncfval  12767  mulc1cncf  12784  addccncf  12794  mulcncf  12799  expcncf  12800  limccnp2lem  12853  dvcnp2cntop  12871  dvcoapbr  12879  dvexp  12883  dvrecap  12885  dvef  12896  sincn  12898  coscn  12899  ptolemy  12953  sincosq1eq  12968  logbgcd1irr  13092  logbgcd1irraplemexp  13093  2irrexpq  13101  2irrexpqap  13103  qdencn  13397  isomninn  13401  trirec0  13412  iswomninn  13418  ismkvnn  13420