Theorem oveq1 5872

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 3774	. . 3 |- ( A = B -> <. A , C >. = <. B , C >. )
2	1	fveq2d 5511	. 2 |- ( A = B -> ( F ` <. A , C >. ) = ( F ` <. B , C >. ) )
3		df-ov 5868	. 2 |- ( A F C ) = ( F ` <. A , C >. )
4		df-ov 5868	. 2 |- ( B F C ) = ( F ` <. B , C >. )
5	2, 3, 4	3eqtr4g 2233	1 |- ( A = B -> ( A F C ) = ( B F C ) )

Syntax hints:   -> wi 4   = wceq 1353   <.cop 3592   ` cfv 5208  (class class class)co 5865

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 1445  ax-7 1446  ax-gen 1447  ax-ie1 1491  ax-ie2 1492  ax-8 1502  ax-10 1503  ax-11 1504  ax-i12 1505  ax-bndl 1507  ax-4 1508  ax-17 1524  ax-i9 1528  ax-ial 1532  ax-i5r 1533  ax-ext 2157

This theorem depends on definitions:  df-bi 117  df-3an 980  df-tru 1356  df-nf 1459  df-sb 1761  df-clab 2162  df-cleq 2168  df-clel 2171  df-nfc 2306  df-rex 2459  df-v 2737  df-un 3131  df-sn 3595  df-pr 3596  df-op 3598  df-uni 3806  df-br 3999  df-iota 5170  df-fv 5216  df-ov 5868

This theorem is referenced by:  oveq12  5874  oveq1i  5875  oveq1d  5880  ovrspc2v  5891  oveqrspc2v  5892  rspceov  5907  fovcl  5970  ovmpos  5988  ov2gf  5989  ovi3  6001  caovclg  6017  caovcomg  6020  caovassg  6023  caovcang  6026  caovcan  6029  caovordig  6030  caovordg  6032  caovord  6036  caovdig  6039  caovdirg  6042  caovimo  6058  suppssov1  6070  off  6085  omcl  6452  oeicl  6453  omv2  6456  nnm0r  6470  nnacom  6475  nndi  6477  nnmass  6478  nnmsucr  6479  nnmcom  6480  nnaword  6502  nnmord  6508  nnm00  6521  eroveu  6616  th3qlem2  6628  th3q  6630  ecovcom  6632  ecovicom  6633  ecovass  6634  ecoviass  6635  ecovdi  6636  ecovidi  6637  map0g  6678  addcmpblnq  7341  addclnq  7349  mulclnq  7350  mulidnq  7363  recexnq  7364  recmulnqg  7365  ltanqg  7374  ltmnqg  7375  ltexnqq  7382  enq0ref  7407  enq0tr  7408  addcmpblnq0  7417  mulnnnq0  7424  addclnq0  7425  mulclnq0  7426  distrnq0  7433  mulcomnq0  7434  addassnq0  7436  prarloclemlo  7468  prarloclem3  7471  prarloclem5  7474  prarloclemcalc  7476  genipv  7483  genpassl  7498  genpassu  7499  addlocprlemeq  7507  distrlem4prl  7558  distrlem4pru  7559  ltexprlemdisj  7580  ltexprlemloc  7581  ltexprlemrl  7584  ltexprlemru  7586  prplnqu  7594  cauappcvgprlemm  7619  cauappcvgprlemopl  7620  cauappcvgprlemlol  7621  cauappcvgprlemdisj  7625  cauappcvgprlemloc  7626  cauappcvgprlemladdfl  7629  cauappcvgprlemladdru  7630  cauappcvgprlemladdrl  7631  cauappcvgprlem1  7633  cauappcvgprlemlim  7635  cauappcvgpr  7636  caucvgprlemm  7642  caucvgprlemopl  7643  caucvgprlemlol  7644  caucvgprlemdisj  7648  caucvgprlemloc  7649  caucvgprlemladdrl  7652  caucvgprlem1  7653  caucvgpr  7656  caucvgprprlemell  7659  caucvgprprlemml  7668  caucvgprpr  7686  mulcmpblnrlemg  7714  addclsr  7727  mulclsr  7728  0idsr  7741  1idsr  7742  00sr  7743  ltasrg  7744  recexgt0sr  7747  mulgt0sr  7752  mulextsr1  7755  prsrriota  7762  caucvgsrlemgt1  7769  caucvgsrlemoffres  7774  pitonn  7822  peano2nnnn  7827  axaddrcl  7839  axmulrcl  7841  axaddcom  7844  ax1rid  7851  ax0id  7852  axprecex  7854  axcnre  7855  axpre-ltadd  7860  axpre-mulgt0  7861  axpre-mulext  7862  rereceu  7863  peano5nnnn  7866  axcaucvglemcau  7872  axcaucvglemres  7873  mulid1  7929  cnegexlem1  8106  cnegexlem2  8107  cnegex  8109  addcan2  8112  subval  8123  addlsub  8301  apreim  8534  recexap  8583  receuap  8599  divvalap  8604  cju  8891  peano2nn  8904  nn1m1nn  8910  nn1suc  8911  nnsub  8931  fv0p1e1  9007  nnm1nn0  9190  zdiv  9314  zneo  9327  nneoor  9328  zeo  9331  peano5uzti  9334  nn0ind-raph  9343  uzind4s  9563  uzind4s2  9564  qmulz  9596  elpq  9621  cnref1o  9623  nn0ledivnn  9738  xaddnemnf  9828  xaddnepnf  9829  xaddcom  9832  xaddid1  9833  xnn0xadd0  9838  xaddass  9840  xpncan  9842  xleadd1a  9844  xltadd1  9847  xlt2add  9851  xsubge0  9852  xposdif  9853  xlesubadd  9854  xleaddadd  9858  fzsuc2  10049  fzm1  10070  fzoval  10118  exbtwnzlemstep  10218  exbtwnzlemshrink  10219  exbtwnzlemex  10220  exbtwnz  10221  rebtwn2zlemstep  10223  rebtwn2zlemshrink  10224  rebtwn2z  10225  flqlelt  10246  flqbi  10260  fldiv4p1lem1div2  10275  modqval  10294  modqadd1  10331  modqmuladd  10336  modqmuladdnn0  10338  modqm1p1mod0  10345  modqmul1  10347  modfzo0difsn  10365  addmodlteq  10368  frec2uzzd  10370  frec2uzsucd  10371  frec2uzrand  10375  frecuzrdgrrn  10378  frec2uzrdg  10379  frecuzrdgrcl  10380  frecuzrdgsuc  10384  frecuzrdgrclt  10385  frecuzrdgg  10386  frecuzrdgdom  10388  frecuzrdgfun  10390  frecuzrdgsuctlem  10393  frecuzrdgsuct  10394  uzsinds  10412  iseqvalcbv  10427  seq3val  10428  seqvalcd  10429  seqf  10431  seq3p1  10432  seqovcd  10433  seqp1cd  10436  seq3fveq2  10439  seq3shft2  10443  monoord  10446  monoord2  10447  seq3split  10449  seq3caopr3  10451  seq3caopr2  10452  iseqf1olemqval  10457  iseqf1olemqk  10464  seq3id2  10479  seq3homo  10480  seq3z  10481  seq3distr  10483  m1expcl2  10512  mulexp  10529  expadd  10532  expmul  10535  sq0i  10581  qsqeqor  10600  sqoddm1div8  10643  facp1  10678  faclbnd  10689  faclbnd3  10691  bcval  10697  bcn1  10706  bcval5  10711  bcpasc  10714  bccl  10715  hashfz1  10731  omgadd  10750  hashfzo  10770  hashfzp1  10772  hashxp  10774  seq3coll  10790  shftlem  10793  shftfvalg  10795  shftfibg  10797  shftfval  10798  shftfib  10800  shftfn  10801  shftf  10807  2shfti  10808  shftvalg  10813  shftval4g  10814  cjval  10822  imval  10827  cjexp  10870  cnrecnv  10887  cvg1nlemcau  10961  cvg1nlemres  10962  resqrexlemcalc3  10993  resqrexlemex  11002  rsqrmo  11004  resqrtcl  11006  rersqrtthlem  11007  sqrtsq  11021  absexp  11056  recan  11086  climshft  11280  climcn1  11284  climcn2  11285  subcn2  11287  fsumshft  11420  fisum0diag2  11423  fsumiun  11453  binomlem  11459  binom  11460  bcxmas  11465  isumsplit  11467  arisum2  11475  trireciplem  11476  trirecip  11477  geolim  11487  cvgratnnlemnexp  11500  cvgratnnlemmn  11501  clim2prod  11515  prodfrecap  11522  fprodcl2lem  11581  fprodfac  11591  fprodshft  11594  ef0lem  11636  efval  11637  efne0  11654  efexp  11658  demoivreALT  11749  dvdsval2  11765  p1modz1  11769  dvds0lem  11776  dvds1lem  11777  dvds2lem  11778  dvdsmulc  11794  divconjdvds  11822  odd2np1lem  11844  odd2np1  11845  ltoddhalfle  11865  halfleoddlt  11866  nn0o1gt2  11877  nn0o  11879  divalglemnn  11890  divalglemeunn  11893  divalglemex  11894  divalglemeuneg  11895  flodddiv4  11906  gcdabs1  11957  gcddiv  11987  dvdssqim  11992  rpmulgcd  11994  bezoutr1  12001  uzwodc  12005  dvdslcm  12036  lcmeq0  12038  lcmdvds  12046  divgcdcoprm0  12068  prmind2  12087  isprm5lem  12108  isprm6  12114  rpexp  12120  sqrt2irr  12129  pw2dvdslemn  12132  pw2dvdseu  12135  oddpwdclemxy  12136  nn0gcdsq  12167  phicl2  12181  phibndlem  12183  hashdvds  12188  crth  12191  phimullem  12192  eulerthlem1  12194  eulerthlemfi  12195  eulerthlemrprm  12196  eulerthlemth  12199  eulerth  12200  hashgcdlem  12205  phisum  12207  odzval  12208  modprm0  12221  nnnn0modprm0  12222  pythagtriplem1  12232  pythagtriplem6  12237  pythagtriplem7  12238  pythagtriplem12  12242  pythagtriplem14  12244  pythagtriplem18  12248  pythagtriplem19  12249  pceulem  12261  pceu  12262  pcval  12263  pczpre  12264  pcdiv  12269  pcqmul  12270  pcqcl  12273  pcexp  12276  pcaddlem  12305  pcadd  12306  pcmpt  12308  pcprod  12311  pcfac  12315  expnprm  12318  prmpwdvds  12320  pockthi  12323  1arithlem2  12329  4sqlem2  12354  4sqlem3  12355  ennnfonelemr  12391  ctinfom  12396  infpn2  12424  mgm1  12664  mgmidmo  12666  ismgmid  12671  mgmlrid  12673  ismgmid2  12674  lidrideqd  12675  lidrididd  12676  mgmidsssn0  12678  grpridd  12681  isnsgrp  12687  sgrpass  12689  sgrp1  12691  sgrpidmndm  12696  ismndd  12713  mndinvmod  12718  mnd1  12719  mnd1id  12720  mhmpropd  12729  insubm  12743  mhmima  12746  grppropd  12764  isgrpd2  12768  isgrpd  12770  dfgrp2  12773  grprcan  12781  grpinveu  12782  grpsubval  12790  grplinv  12793  grpinvid2  12796  isgrpinv  12797  grplrinv  12798  grpidinv2  12799  grpidinv  12800  grpidssd  12816  grpinvssd  12817  dfgrp3mlem  12838  dfgrp3m  12839  grplactfval  12841  grp1  12846  mhmmnd  12850  ghmgrp  12852  mulgnn0p1  12864  mulgnn0subcl  12866  mulgaddcom  12876  mulginvcom  12877  mulgnn0z  12879  mulgneg2  12886  mulgnnass  12887  mulgnn0ass  12888  mhmmulg  12893  srgrz  12973  srgmulgass  12978  srgpcomp  12979  srgrmhm  12983  ringid  13015  ringinvnzdiv  13032  mulgass2  13040  ring1  13041  cnmptcom  13378  psmettri2  13408  isxmet2d  13428  xmeteq0  13439  xmettri2  13441  metrest  13586  cncfval  13639  mulc1cncf  13656  addccncf  13666  mulcncf  13671  expcncf  13672  limccnp2lem  13725  dvcnp2cntop  13743  dvcoapbr  13751  dvexp  13755  dvrecap  13757  dvef  13768  sincn  13770  coscn  13771  ptolemy  13825  sincosq1eq  13840  logbgcd1irr  13965  logbgcd1irraplemexp  13966  2irrexpq  13974  2irrexpqap  13976  lgslem4  13984  lgsval  13985  lgsfvalg  13986  lgsval2lem  13991  lgsdir2lem4  14012  lgsdir  14016  lgsdilem2  14017  lgsdi  14018  lgsne0  14019  lgsmodeq  14026  lgsdirnn0  14028  lgsdinn0  14029  2sqlem2  14031  2sqlem6  14036  2sqlem8  14039  2sqlem9  14040  qdencn  14345  isomninn  14349  trirec0  14362  iswomninn  14368  ismkvnn  14371