Theorem oveq1 5925

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 3804	. . 3 |- ( A = B -> <. A , C >. = <. B , C >. )
2	1	fveq2d 5558	. 2 |- ( A = B -> ( F ` <. A , C >. ) = ( F ` <. B , C >. ) )
3		df-ov 5921	. 2 |- ( A F C ) = ( F ` <. A , C >. )
4		df-ov 5921	. 2 |- ( B F C ) = ( F ` <. B , C >. )
5	2, 3, 4	3eqtr4g 2251	1 |- ( A = B -> ( A F C ) = ( B F C ) )

Syntax hints:   -> wi 4   = wceq 1364   <.cop 3621   ` cfv 5254  (class class class)co 5918

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 710  ax-5 1458  ax-7 1459  ax-gen 1460  ax-ie1 1504  ax-ie2 1505  ax-8 1515  ax-10 1516  ax-11 1517  ax-i12 1518  ax-bndl 1520  ax-4 1521  ax-17 1537  ax-i9 1541  ax-ial 1545  ax-i5r 1546  ax-ext 2175

This theorem depends on definitions:  df-bi 117  df-3an 982  df-tru 1367  df-nf 1472  df-sb 1774  df-clab 2180  df-cleq 2186  df-clel 2189  df-nfc 2325  df-rex 2478  df-v 2762  df-un 3157  df-sn 3624  df-pr 3625  df-op 3627  df-uni 3836  df-br 4030  df-iota 5215  df-fv 5262  df-ov 5921

This theorem is referenced by:  oveq12  5927  oveq1i  5928  oveq1d  5933  ovrspc2v  5944  oveqrspc2v  5945  rspceov  5960  fovcld  6023  ovmpos  6042  ov2gf  6043  ovi3  6055  caovclg  6071  caovcomg  6074  caovassg  6077  caovcang  6080  caovcan  6083  caovordig  6084  caovordg  6086  caovord  6090  caovdig  6093  caovdirg  6096  caovimo  6112  suppssov1  6127  off  6143  caofdig  6159  omcl  6514  oeicl  6515  omv2  6518  nnm0r  6532  nnacom  6537  nndi  6539  nnmass  6540  nnmsucr  6541  nnmcom  6542  nnaword  6564  nnmord  6570  nnm00  6583  eroveu  6680  th3qlem2  6692  th3q  6694  ecovcom  6696  ecovicom  6697  ecovass  6698  ecoviass  6699  ecovdi  6700  ecovidi  6701  map0g  6742  addcmpblnq  7427  addclnq  7435  mulclnq  7436  mulidnq  7449  recexnq  7450  recmulnqg  7451  ltanqg  7460  ltmnqg  7461  ltexnqq  7468  enq0ref  7493  enq0tr  7494  addcmpblnq0  7503  mulnnnq0  7510  addclnq0  7511  mulclnq0  7512  distrnq0  7519  mulcomnq0  7520  addassnq0  7522  prarloclemlo  7554  prarloclem3  7557  prarloclem5  7560  prarloclemcalc  7562  genipv  7569  genpassl  7584  genpassu  7585  addlocprlemeq  7593  distrlem4prl  7644  distrlem4pru  7645  ltexprlemdisj  7666  ltexprlemloc  7667  ltexprlemrl  7670  ltexprlemru  7672  prplnqu  7680  cauappcvgprlemm  7705  cauappcvgprlemopl  7706  cauappcvgprlemlol  7707  cauappcvgprlemdisj  7711  cauappcvgprlemloc  7712  cauappcvgprlemladdfl  7715  cauappcvgprlemladdru  7716  cauappcvgprlemladdrl  7717  cauappcvgprlem1  7719  cauappcvgprlemlim  7721  cauappcvgpr  7722  caucvgprlemm  7728  caucvgprlemopl  7729  caucvgprlemlol  7730  caucvgprlemdisj  7734  caucvgprlemloc  7735  caucvgprlemladdrl  7738  caucvgprlem1  7739  caucvgpr  7742  caucvgprprlemell  7745  caucvgprprlemml  7754  caucvgprpr  7772  mulcmpblnrlemg  7800  addclsr  7813  mulclsr  7814  0idsr  7827  1idsr  7828  00sr  7829  ltasrg  7830  recexgt0sr  7833  mulgt0sr  7838  mulextsr1  7841  prsrriota  7848  caucvgsrlemgt1  7855  caucvgsrlemoffres  7860  pitonn  7908  peano2nnnn  7913  axaddrcl  7925  axmulrcl  7927  axaddcom  7930  ax1rid  7937  ax0id  7938  axprecex  7940  axcnre  7941  axpre-ltadd  7946  axpre-mulgt0  7947  axpre-mulext  7948  rereceu  7949  peano5nnnn  7952  axcaucvglemcau  7958  axcaucvglemres  7959  mulrid  8016  cnegexlem1  8194  cnegexlem2  8195  cnegex  8197  addcan2  8200  subval  8211  addlsub  8389  apreim  8622  recexap  8672  receuap  8688  divvalap  8693  cju  8980  peano2nn  8994  nn1m1nn  9000  nn1suc  9001  nnsub  9021  fv0p1e1  9097  nnm1nn0  9281  zdiv  9405  zneo  9418  nneoor  9419  zeo  9422  peano5uzti  9425  nn0ind-raph  9434  uzind4s  9655  uzind4s2  9656  qmulz  9688  elpq  9714  cnref1o  9716  nn0ledivnn  9833  xaddnemnf  9923  xaddnepnf  9924  xaddcom  9927  xaddid1  9928  xnn0xadd0  9933  xaddass  9935  xpncan  9937  xleadd1a  9939  xltadd1  9942  xlt2add  9946  xsubge0  9947  xposdif  9948  xlesubadd  9949  xleaddadd  9953  fzsuc2  10145  fzm1  10166  fzoval  10214  exbtwnzlemstep  10316  exbtwnzlemshrink  10317  exbtwnzlemex  10318  exbtwnz  10319  rebtwn2zlemstep  10321  rebtwn2zlemshrink  10322  rebtwn2z  10323  flqlelt  10345  flqbi  10359  fldiv4p1lem1div2  10374  fldiv4lem1div2  10376  modqval  10395  modqadd1  10432  modqmuladd  10437  modqmuladdnn0  10439  modqm1p1mod0  10446  modqmul1  10448  modfzo0difsn  10466  addmodlteq  10469  frec2uzzd  10471  frec2uzsucd  10472  frec2uzrand  10476  frecuzrdgrrn  10479  frec2uzrdg  10480  frecuzrdgrcl  10481  frecuzrdgsuc  10485  frecuzrdgrclt  10486  frecuzrdgg  10487  frecuzrdgdom  10489  frecuzrdgfun  10491  frecuzrdgsuctlem  10494  frecuzrdgsuct  10495  uzsinds  10515  iseqvalcbv  10530  seq3val  10531  seqvalcd  10532  seqf  10535  seq3p1  10536  seqovcd  10538  seqp1cd  10541  seq3fveq2  10546  seqfveq2g  10548  seq3shft2  10552  seqshft2g  10553  monoord  10556  monoord2  10557  seq3split  10559  seqsplitg  10560  seq3caopr3  10562  seqcaopr3g  10563  seq3caopr2  10564  seqcaopr2g  10565  iseqf1olemqval  10571  iseqf1olemqk  10578  seqf1oglem2a  10589  seqf1oglem2  10591  seq3id2  10597  seq3homo  10598  seq3z  10599  seqhomog  10601  seqfeq4g  10602  seq3distr  10603  m1expcl2  10632  mulexp  10649  expadd  10652  expmul  10655  sq0i  10702  qsqeqor  10721  sqoddm1div8  10764  facp1  10801  faclbnd  10812  faclbnd3  10814  bcval  10820  bcn1  10829  bcval5  10834  bcpasc  10837  bccl  10838  hashfz1  10854  omgadd  10873  hashfzo  10893  hashfzp1  10895  hashxp  10897  seq3coll  10913  shftlem  10960  shftfvalg  10962  shftfibg  10964  shftfval  10965  shftfib  10967  shftfn  10968  shftf  10974  2shfti  10975  shftvalg  10980  shftval4g  10981  cjval  10989  imval  10994  cjexp  11037  cnrecnv  11054  cvg1nlemcau  11128  cvg1nlemres  11129  resqrexlemcalc3  11160  resqrexlemex  11169  rsqrmo  11171  resqrtcl  11173  rersqrtthlem  11174  sqrtsq  11188  absexp  11223  recan  11253  climshft  11447  climcn1  11451  climcn2  11452  subcn2  11454  fsumshft  11587  fisum0diag2  11590  fsumiun  11620  binomlem  11626  binom  11627  bcxmas  11632  isumsplit  11634  arisum2  11642  trireciplem  11643  trirecip  11644  geolim  11654  cvgratnnlemnexp  11667  cvgratnnlemmn  11668  clim2prod  11682  prodfrecap  11689  fprodcl2lem  11748  fprodfac  11758  fprodshft  11761  ef0lem  11803  efval  11804  efne0  11821  efexp  11825  demoivreALT  11917  dvdsval2  11933  p1modz1  11937  dvds0lem  11944  dvds1lem  11945  dvds2lem  11946  dvdsmulc  11962  divconjdvds  11991  odd2np1lem  12013  odd2np1  12014  ltoddhalfle  12034  halfleoddlt  12035  nn0o1gt2  12046  nn0o  12048  divalglemnn  12059  divalglemeunn  12062  divalglemex  12063  divalglemeuneg  12064  flodddiv4  12075  gcdabs1  12126  gcddiv  12156  dvdssqim  12161  rpmulgcd  12163  bezoutr1  12170  uzwodc  12174  dvdslcm  12207  lcmeq0  12209  lcmdvds  12217  divgcdcoprm0  12239  prmind2  12258  isprm5lem  12279  isprm6  12285  rpexp  12291  sqrt2irr  12300  pw2dvdslemn  12303  pw2dvdseu  12306  oddpwdclemxy  12307  nn0gcdsq  12338  phicl2  12352  phibndlem  12354  hashdvds  12359  crth  12362  phimullem  12363  eulerthlem1  12365  eulerthlemfi  12366  eulerthlemrprm  12367  eulerthlemth  12370  eulerth  12371  hashgcdlem  12376  phisum  12378  odzval  12379  modprm0  12392  nnnn0modprm0  12393  pythagtriplem1  12403  pythagtriplem6  12408  pythagtriplem7  12409  pythagtriplem12  12413  pythagtriplem14  12415  pythagtriplem18  12419  pythagtriplem19  12420  pceulem  12432  pceu  12433  pcval  12434  pczpre  12435  pcdiv  12440  pcqmul  12441  pcqcl  12444  pcexp  12447  pcaddlem  12477  pcadd  12478  pcmpt  12481  pcprod  12484  pcfac  12488  expnprm  12491  prmpwdvds  12493  pockthi  12496  1arithlem2  12502  4sqlem2  12527  4sqlem3  12528  4sqlem11  12539  4sqlem12  12540  4sqlem13m  12541  4sqlem17  12545  4sqlem18  12546  4sqlem19  12547  ennnfonelemr  12580  ctinfom  12585  infpn2  12613  ercpbl  12914  mgm1  12953  mgmidmo  12955  ismgmid  12960  mgmlrid  12962  ismgmid2  12963  lidrideqd  12964  lidrididd  12965  mgmidsssn0  12967  grprida  12970  gsumfzval  12974  gsumress  12978  gsumval2  12980  isnsgrp  12989  sgrpass  12991  sgrp1  12994  sgrpidmndm  13001  ismndd  13018  mndinvmod  13026  mnd1  13027  mnd1id  13028  mhmpropd  13038  insubm  13057  mhmima  13063  gsumvallem2  13065  grppropd  13089  isgrpd2  13093  isgrpd  13095  dfgrp2  13099  grprcan  13109  grpinveu  13110  grpsubval  13118  grplinv  13122  grpinvid2  13125  isgrpinv  13126  grplrinv  13129  grpidinv2  13130  grpidinv  13131  grpidssd  13148  grpinvssd  13149  dfgrp3mlem  13170  dfgrp3m  13171  grplactfval  13173  grp1  13178  imasgrp2  13180  mhmmnd  13186  ghmgrp  13188  mulgnn0gsum  13198  mulgnn0p1  13203  mulgnn0subcl  13205  mulgaddcom  13216  mulginvcom  13217  mulgnn0z  13219  mulgneg2  13226  mulgnnass  13227  mulgnn0ass  13228  mhmmulg  13233  issubg  13243  subgex  13246  issubg2m  13259  issubg4m  13263  isnsg2  13273  nsgbi  13274  isnsg3  13277  elnmz  13278  nmzbi  13279  ghmrn  13327  ghmnsgima  13338  gsumfzconst  13411  rngdi  13436  rngdir  13437  srgrz  13480  srgmulgass  13485  srgpcomp  13486  srgrmhm  13490  ringid  13522  ringinvnzdiv  13546  mulgass2  13554  ring1  13555  ringrghm  13558  imasring  13560  dvdsrmuld  13592  dvdsrmul1  13598  dvdsr01  13600  dvreq1  13638  rhmdvdsr  13671  lringuplu  13692  issubrng  13695  issubrng2  13706  issubrg  13717  issubrg2  13737  isrrg  13759  domneq0  13768  lmodlema  13788  islmodd  13789  lmodvsmmulgdi  13819  rmodislmodlem  13846  rmodislmod  13847  lssclg  13860  lss1d  13879  lspsn  13912  sraval  13933  rnglidlmcl  13976  quscrng  14029  cnfldmulg  14064  cnfldexp  14065  gsumfzfsumlemm  14075  cnfldui  14077  expghmap  14095  mulgghm2  14096  mulgrhm  14097  zrhmulg  14108  zlmval  14115  znunit  14147  cnmptcom  14466  psmettri2  14496  isxmet2d  14516  xmeteq0  14527  xmettri2  14529  metrest  14674  cncfval  14727  mulc1cncf  14744  addccncf  14754  mulcncf  14762  expcncf  14763  hovera  14801  hoverb  14802  hoverlt1  14803  hovergt0  14804  ivthdich  14807  limccnp2lem  14830  dvcnp2cntop  14848  dvcoapbr  14856  dvexp  14860  dvrecap  14862  dvef  14873  plyadd  14897  plymul  14898  sincn  14904  coscn  14905  ptolemy  14959  sincosq1eq  14974  logbgcd1irr  15099  logbgcd1irraplemexp  15100  2irrexpq  15108  2irrexpqap  15110  lgslem4  15119  lgsval  15120  lgsfvalg  15121  lgsval2lem  15126  lgsdir2lem4  15147  lgsdir  15151  lgsdilem2  15152  lgsdi  15153  lgsne0  15154  lgsmodeq  15161  lgsdirnn0  15163  lgsdinn0  15164  gausslemma2dlem0i  15173  gausslemma2dlem1a  15174  gausslemma2dlem1f1o  15176  gausslemma2dlem2  15178  gausslemma2dlem3  15179  gausslemma2dlem4  15180  lgseisenlem2  15187  2lgsoddprmlem1  15193  2lgsoddprmlem3  15199  2sqlem2  15202  2sqlem6  15207  2sqlem8  15210  2sqlem9  15211  qdencn  15517  isomninn  15521  trirec0  15534  iswomninn  15540  ismkvnn  15543