Theorem oveq1 5848

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 3757	. . 3 |- ( A = B -> <. A , C >. = <. B , C >. )
2	1	fveq2d 5489	. 2 |- ( A = B -> ( F ` <. A , C >. ) = ( F ` <. B , C >. ) )
3		df-ov 5844	. 2 |- ( A F C ) = ( F ` <. A , C >. )
4		df-ov 5844	. 2 |- ( B F C ) = ( F ` <. B , C >. )
5	2, 3, 4	3eqtr4g 2223	1 |- ( A = B -> ( A F C ) = ( B F C ) )

Syntax hints:   -> wi 4   = wceq 1343   <.cop 3578   ` cfv 5187  (class class class)co 5841

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 1435  ax-7 1436  ax-gen 1437  ax-ie1 1481  ax-ie2 1482  ax-8 1492  ax-10 1493  ax-11 1494  ax-i12 1495  ax-bndl 1497  ax-4 1498  ax-17 1514  ax-i9 1518  ax-ial 1522  ax-i5r 1523  ax-ext 2147

This theorem depends on definitions:  df-bi 116  df-3an 970  df-tru 1346  df-nf 1449  df-sb 1751  df-clab 2152  df-cleq 2158  df-clel 2161  df-nfc 2296  df-rex 2449  df-v 2727  df-un 3119  df-sn 3581  df-pr 3582  df-op 3584  df-uni 3789  df-br 3982  df-iota 5152  df-fv 5195  df-ov 5844

This theorem is referenced by:  oveq12  5850  oveq1i  5851  oveq1d  5856  rspceov  5880  fovcl  5943  ovmpos  5961  ov2gf  5962  ovi3  5974  caovclg  5990  caovcomg  5993  caovassg  5996  caovcang  5999  caovcan  6002  caovordig  6003  caovordg  6005  caovord  6009  caovdig  6012  caovdirg  6015  caovimo  6031  grpridd  6034  suppssov1  6046  off  6061  omcl  6425  oeicl  6426  omv2  6429  nnm0r  6443  nnacom  6448  nndi  6450  nnmass  6451  nnmsucr  6452  nnmcom  6453  nnaword  6475  nnmord  6481  nnm00  6493  eroveu  6588  th3qlem2  6600  th3q  6602  ecovcom  6604  ecovicom  6605  ecovass  6606  ecoviass  6607  ecovdi  6608  ecovidi  6609  map0g  6650  addcmpblnq  7304  addclnq  7312  mulclnq  7313  mulidnq  7326  recexnq  7327  recmulnqg  7328  ltanqg  7337  ltmnqg  7338  ltexnqq  7345  enq0ref  7370  enq0tr  7371  addcmpblnq0  7380  mulnnnq0  7387  addclnq0  7388  mulclnq0  7389  distrnq0  7396  mulcomnq0  7397  addassnq0  7399  prarloclemlo  7431  prarloclem3  7434  prarloclem5  7437  prarloclemcalc  7439  genipv  7446  genpassl  7461  genpassu  7462  addlocprlemeq  7470  distrlem4prl  7521  distrlem4pru  7522  ltexprlemdisj  7543  ltexprlemloc  7544  ltexprlemrl  7547  ltexprlemru  7549  prplnqu  7557  cauappcvgprlemm  7582  cauappcvgprlemopl  7583  cauappcvgprlemlol  7584  cauappcvgprlemdisj  7588  cauappcvgprlemloc  7589  cauappcvgprlemladdfl  7592  cauappcvgprlemladdru  7593  cauappcvgprlemladdrl  7594  cauappcvgprlem1  7596  cauappcvgprlemlim  7598  cauappcvgpr  7599  caucvgprlemm  7605  caucvgprlemopl  7606  caucvgprlemlol  7607  caucvgprlemdisj  7611  caucvgprlemloc  7612  caucvgprlemladdrl  7615  caucvgprlem1  7616  caucvgpr  7619  caucvgprprlemell  7622  caucvgprprlemml  7631  caucvgprpr  7649  mulcmpblnrlemg  7677  addclsr  7690  mulclsr  7691  0idsr  7704  1idsr  7705  00sr  7706  ltasrg  7707  recexgt0sr  7710  mulgt0sr  7715  mulextsr1  7718  prsrriota  7725  caucvgsrlemgt1  7732  caucvgsrlemoffres  7737  pitonn  7785  peano2nnnn  7790  axaddrcl  7802  axmulrcl  7804  axaddcom  7807  ax1rid  7814  ax0id  7815  axprecex  7817  axcnre  7818  axpre-ltadd  7823  axpre-mulgt0  7824  axpre-mulext  7825  rereceu  7826  peano5nnnn  7829  axcaucvglemcau  7835  axcaucvglemres  7836  mulid1  7892  cnegexlem1  8069  cnegexlem2  8070  cnegex  8072  addcan2  8075  subval  8086  addlsub  8264  apreim  8497  recexap  8546  receuap  8562  divvalap  8566  cju  8852  peano2nn  8865  nn1m1nn  8871  nn1suc  8872  nnsub  8892  fv0p1e1  8968  nnm1nn0  9151  zdiv  9275  zneo  9288  nneoor  9289  zeo  9292  peano5uzti  9295  nn0ind-raph  9304  uzind4s  9524  uzind4s2  9525  qmulz  9557  elpq  9582  cnref1o  9584  nn0ledivnn  9699  xaddnemnf  9789  xaddnepnf  9790  xaddcom  9793  xaddid1  9794  xnn0xadd0  9799  xaddass  9801  xpncan  9803  xleadd1a  9805  xltadd1  9808  xlt2add  9812  xsubge0  9813  xposdif  9814  xlesubadd  9815  xleaddadd  9819  fzsuc2  10010  fzm1  10031  fzoval  10079  exbtwnzlemstep  10179  exbtwnzlemshrink  10180  exbtwnzlemex  10181  exbtwnz  10182  rebtwn2zlemstep  10184  rebtwn2zlemshrink  10185  rebtwn2z  10186  flqlelt  10207  flqbi  10221  fldiv4p1lem1div2  10236  modqval  10255  modqadd1  10292  modqmuladd  10297  modqmuladdnn0  10299  modqm1p1mod0  10306  modqmul1  10308  modfzo0difsn  10326  addmodlteq  10329  frec2uzzd  10331  frec2uzsucd  10332  frec2uzrand  10336  frecuzrdgrrn  10339  frec2uzrdg  10340  frecuzrdgrcl  10341  frecuzrdgsuc  10345  frecuzrdgrclt  10346  frecuzrdgg  10347  frecuzrdgdom  10349  frecuzrdgfun  10351  frecuzrdgsuctlem  10354  frecuzrdgsuct  10355  uzsinds  10373  iseqvalcbv  10388  seq3val  10389  seqvalcd  10390  seqf  10392  seq3p1  10393  seqovcd  10394  seqp1cd  10397  seq3fveq2  10400  seq3shft2  10404  monoord  10407  monoord2  10408  seq3split  10410  seq3caopr3  10412  seq3caopr2  10413  iseqf1olemqval  10418  iseqf1olemqk  10425  seq3id2  10440  seq3homo  10441  seq3z  10442  seq3distr  10444  m1expcl2  10473  mulexp  10490  expadd  10493  expmul  10496  sq0i  10542  qsqeqor  10561  sqoddm1div8  10604  facp1  10639  faclbnd  10650  faclbnd3  10652  bcval  10658  bcn1  10667  bcval5  10672  bcpasc  10675  bccl  10676  hashfz1  10692  omgadd  10711  hashfzo  10731  hashfzp1  10733  hashxp  10735  seq3coll  10751  shftlem  10754  shftfvalg  10756  shftfibg  10758  shftfval  10759  shftfib  10761  shftfn  10762  shftf  10768  2shfti  10769  shftvalg  10774  shftval4g  10775  cjval  10783  imval  10788  cjexp  10831  cnrecnv  10848  cvg1nlemcau  10922  cvg1nlemres  10923  resqrexlemcalc3  10954  resqrexlemex  10963  rsqrmo  10965  resqrtcl  10967  rersqrtthlem  10968  sqrtsq  10982  absexp  11017  recan  11047  climshft  11241  climcn1  11245  climcn2  11246  subcn2  11248  fsumshft  11381  fisum0diag2  11384  fsumiun  11414  binomlem  11420  binom  11421  bcxmas  11426  isumsplit  11428  arisum2  11436  trireciplem  11437  trirecip  11438  geolim  11448  cvgratnnlemnexp  11461  cvgratnnlemmn  11462  clim2prod  11476  prodfrecap  11483  fprodcl2lem  11542  fprodfac  11552  fprodshft  11555  ef0lem  11597  efval  11598  efne0  11615  efexp  11619  demoivreALT  11710  dvdsval2  11726  p1modz1  11730  dvds0lem  11737  dvds1lem  11738  dvds2lem  11739  dvdsmulc  11755  divconjdvds  11783  odd2np1lem  11805  odd2np1  11806  ltoddhalfle  11826  halfleoddlt  11827  nn0o1gt2  11838  nn0o  11840  divalglemnn  11851  divalglemeunn  11854  divalglemex  11855  divalglemeuneg  11856  flodddiv4  11867  gcdabs1  11918  gcddiv  11948  dvdssqim  11953  rpmulgcd  11955  bezoutr1  11962  uzwodc  11966  dvdslcm  11997  lcmeq0  11999  lcmdvds  12007  divgcdcoprm0  12029  prmind2  12048  isprm5lem  12069  isprm6  12075  rpexp  12081  sqrt2irr  12090  pw2dvdslemn  12093  pw2dvdseu  12096  oddpwdclemxy  12097  nn0gcdsq  12128  phicl2  12142  phibndlem  12144  hashdvds  12149  crth  12152  phimullem  12153  eulerthlem1  12155  eulerthlemfi  12156  eulerthlemrprm  12157  eulerthlemth  12160  eulerth  12161  hashgcdlem  12166  phisum  12168  odzval  12169  modprm0  12182  nnnn0modprm0  12183  pythagtriplem1  12193  pythagtriplem6  12198  pythagtriplem7  12199  pythagtriplem12  12203  pythagtriplem14  12205  pythagtriplem18  12209  pythagtriplem19  12210  pceulem  12222  pceu  12223  pcval  12224  pczpre  12225  pcdiv  12230  pcqmul  12231  pcqcl  12234  pcexp  12237  pcaddlem  12266  pcadd  12267  pcmpt  12269  pcprod  12272  pcfac  12276  expnprm  12279  prmpwdvds  12281  pockthi  12284  1arithlem2  12290  4sqlem2  12315  4sqlem3  12316  ennnfonelemr  12352  ctinfom  12357  infpn2  12385  cnmptcom  12898  psmettri2  12928  isxmet2d  12948  xmeteq0  12959  xmettri2  12961  metrest  13106  cncfval  13159  mulc1cncf  13176  addccncf  13186  mulcncf  13191  expcncf  13192  limccnp2lem  13245  dvcnp2cntop  13263  dvcoapbr  13271  dvexp  13275  dvrecap  13277  dvef  13288  sincn  13290  coscn  13291  ptolemy  13345  sincosq1eq  13360  logbgcd1irr  13485  logbgcd1irraplemexp  13486  2irrexpq  13494  2irrexpqap  13496  lgslem4  13504  lgsval  13505  lgsfvalg  13506  lgsval2lem  13511  lgsdir2lem4  13532  lgsdir  13536  lgsdilem2  13537  lgsdi  13538  lgsne0  13539  lgsmodeq  13546  lgsdirnn0  13548  lgsdinn0  13549  2sqlem2  13551  2sqlem6  13556  2sqlem8  13559  2sqlem9  13560  qdencn  13866  isomninn  13870  trirec0  13883  iswomninn  13889  ismkvnn  13892