Theorem oveq1 6092

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 3904	. . 3 |- ( A = B -> <. A , C >. = <. B , C >. )
2	1	fveq2d 5699	. 2 |- ( A = B -> ( F ` <. A , C >. ) = ( F ` <. B , C >. ) )
3		df-ov 6088	. 2 |- ( A F C ) = ( F ` <. A , C >. )
4		df-ov 6088	. 2 |- ( B F C ) = ( F ` <. B , C >. )
5	2, 3, 4	3eqtr4g 2296	1 |- ( A = B -> ( A F C ) = ( B F C ) )

This proof depends on syntax axioms:   -> wi 4   = wceq 1402   <.cop 3712   ` cfv 5377  (class class class)co 6085

This proof depends on axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-ia1 106  ax-ia2 107  ax-ia3 108  ax-io 721  ax-5 1500  ax-7 1501  ax-gen 1502  ax-ie1 1546  ax-ie2 1547  ax-8 1557  ax-10 1558  ax-11 1559  ax-i12 1560  ax-bndl 1562  ax-4 1563  ax-17 1579  ax-i9 1583  ax-ial 1587  ax-i5r 1588  ax-ext 2220

This proof depends on definitions:  df-bi 117  df-3an 1011  df-tru 1405  df-nf 1514  df-sb 1816  df-clab 2225  df-cleq 2231  df-clel 2234  df-nfc 2381  df-rex 2534  df-v 2823  df-un 3224  df-sn 3715  df-pr 3716  df-op 3718  df-uni 3936  df-br 4131  df-iota 5337  df-fv 5385  df-ov 6088

This theorem is used by:  oveq12  6094  oveq1i  6095  oveq1d  6100  ovrspc2v  6111  oveqrspc2v  6112  rspceov  6128  fovcld  6193  ovmpos  6212  ov2gf  6213  ovi3  6226  caovclg  6242  caovcomg  6245  caovassg  6248  caovcang  6251  caovcan  6254  caovordig  6255  caovordg  6257  caovord  6261  caovdig  6264  caovdirg  6267  caovimo  6283  suppssov1  6299  off  6315  caofid0r  6330  caofid1  6331  caofdig  6336  suppofss1dcl  6504  suppofss2dcl  6505  omcl  6734  oeicl  6735  omv2  6738  nnm0r  6752  nnacom  6757  nndi  6759  nnmass  6760  nnmsucr  6761  nnmcom  6762  nnaword  6784  nnmord  6790  nnm00  6803  eroveu  6900  th3qlem2  6912  th3q  6914  ecovcom  6916  ecovicom  6917  ecovass  6918  ecoviass  6919  ecovdi  6920  ecovidi  6921  map0g  6969  addcmpblnq  7734  addclnq  7742  mulclnq  7743  mulidnq  7756  recexnq  7757  recmulnqg  7758  ltanqg  7767  ltmnqg  7768  ltexnqq  7775  enq0ref  7800  enq0tr  7801  addcmpblnq0  7810  mulnnnq0  7817  addclnq0  7818  mulclnq0  7819  distrnq0  7826  mulcomnq0  7827  addassnq0  7829  prarloclemlo  7861  prarloclem3  7864  prarloclem5  7867  prarloclemcalc  7869  genipv  7876  genpassl  7891  genpassu  7892  addlocprlemeq  7900  distrlem4prl  7951  distrlem4pru  7952  ltexprlemdisj  7973  ltexprlemloc  7974  ltexprlemrl  7977  ltexprlemru  7979  prplnqu  7987  cauappcvgprlemm  8012  cauappcvgprlemopl  8013  cauappcvgprlemlol  8014  cauappcvgprlemdisj  8018  cauappcvgprlemloc  8019  cauappcvgprlemladdfl  8022  cauappcvgprlemladdru  8023  cauappcvgprlemladdrl  8024  cauappcvgprlem1  8026  cauappcvgprlemlim  8028  cauappcvgpr  8029  caucvgprlemm  8035  caucvgprlemopl  8036  caucvgprlemlol  8037  caucvgprlemdisj  8041  caucvgprlemloc  8042  caucvgprlemladdrl  8045  caucvgprlem1  8046  caucvgpr  8049  caucvgprprlemell  8052  caucvgprprlemml  8061  caucvgprpr  8079  mulcmpblnrlemg  8107  addclsr  8120  mulclsr  8121  0idsr  8134  1idsr  8135  00sr  8136  ltasrg  8137  recexgt0sr  8140  mulgt0sr  8145  mulextsr1  8148  prsrriota  8155  caucvgsrlemgt1  8162  caucvgsrlemoffres  8167  pitonn  8215  peano2nnnn  8220  axaddrcl  8232  axmulrcl  8234  axaddcom  8237  ax1rid  8244  ax0id  8245  axprecex  8247  axcnre  8248  axpre-ltadd  8253  axpre-mulgt0  8254  axpre-mulext  8255  rereceu  8256  peano5nnnn  8259  axcaucvglemcau  8265  axcaucvglemres  8266  mulrid  8323  cnegexlem1  8502  cnegexlem2  8503  cnegex  8505  addcan2  8508  subval  8519  addlsub  8697  apreim  8933  recexap  8983  receuap  9001  divvalap  9006  cju  9293  peano2nn  9318  nn1m1nn  9324  nn1suc  9325  nnsub  9345  fv0p1e1  9421  nnm1nn0  9608  zdiv  9738  zneo  9751  nneoor  9752  zeo  9755  peano5uzti  9758  nn0ind-raph  9767  uzind4s  9999  uzind4s2  10000  qmulz  10032  elpq  10059  cnref1o  10061  nn0ledivnn  10178  xaddnemnf  10269  xaddnepnf  10270  xaddcom  10273  xaddid1  10274  xnn0xadd0  10279  xaddass  10281  xpncan  10283  xleadd1a  10285  xltadd1  10288  xlt2add  10292  xsubge0  10293  xposdif  10294  xlesubadd  10295  xleaddadd  10299  fzsuc2  10496  fzm1  10517  fzoval  10565  exbtwnzlemstep  10692  exbtwnzlemshrink  10693  exbtwnzlemex  10694  exbtwnz  10695  rebtwn2zlemstep  10697  rebtwn2zlemshrink  10698  rebtwn2z  10699  flqlelt  10722  flaplelt  10723  flqbi  10738  fldiv4p1lem1div2  10753  fldiv4lem1div2  10755  modqval  10774  modqadd1  10811  modqmuladd  10816  modqmuladdnn0  10818  modqm1p1mod0  10825  modqmul1  10827  modfzo0difsn  10845  addmodlteq  10848  frec2uzzd  10850  frec2uzsucd  10851  frec2uzrand  10855  frecuzrdgrrn  10858  frec2uzrdg  10859  frecuzrdgrcl  10860  frecuzrdgsuc  10864  frecuzrdgrclt  10865  frecuzrdgg  10866  frecuzrdgdom  10868  frecuzrdgfun  10870  frecuzrdgsuctlem  10873  frecuzrdgsuct  10874  uzsinds  10894  iseqvalcbv  10909  seq3val  10910  seqvalcd  10911  seqf  10914  seq3p1  10915  seqovcd  10917  seqp1cd  10920  seq3fveq2  10925  seqfveq2g  10927  seq3shft2  10931  seqshft2g  10932  monoord  10935  monoord2  10936  seq3split  10938  seqsplitg  10939  seq3caopr3  10941  seqcaopr3g  10942  seq3caopr2  10943  seqcaopr2g  10944  iseqf1olemqval  10950  iseqf1olemqk  10957  seqf1oglem2a  10968  seqf1oglem2  10970  seq3id2  10976  seq3homo  10977  seq3z  10978  seqhomog  10980  seqfeq4g  10981  seq3distr  10982  m1expcl2  11011  mulexp  11028  expadd  11031  expmul  11034  sq0i  11081  qsqeqor  11100  resq01  11108  sqoddm1div8  11144  facp1  11182  faclbnd  11193  faclbnd3  11195  bcval  11201  bcn1  11210  bcval5  11215  bcpasc  11218  bccl  11219  hashfz1  11236  omgadd  11256  hashfzo  11277  hashfzp1  11279  hashxp  11281  hashmap  11282  hashf1lem2  11300  seq3coll  11308  lsw1  11368  ccats1val2  11422  ccatw2s1p2  11428  pfxsuff1eqwrdeq  11485  swrdswrd  11491  ccats1pfxeq  11500  ccatopth  11502  wrdind  11508  wrd2ind  11509  swrdccatin2  11515  pfxccatin12lem2  11517  swrdccat3blem  11525  ccats1pfxeqbi  11528  swrdccatin2d  11530  reuccatpfxs1  11533  shftlem  11595  shftfvalg  11597  shftfibg  11599  shftfval  11600  shftfib  11602  shftfn  11603  shftf  11609  2shfti  11610  shftvalg  11615  shftval4g  11616  cjval  11624  imval  11629  cjexp  11672  sq01  11674  cnrecnv  11690  cvg1nlemcau  11764  cvg1nlemres  11765  resqrexlemcalc3  11796  resqrexlemex  11805  rsqrmo  11807  resqrtcl  11809  rersqrtthlem  11810  sqrtsq  11824  absexp  11860  recan  11890  climshft  12086  climcn1  12090  climcn2  12091  subcn2  12093  fsumshft  12227  fisum0diag2  12230  fsumiun  12260  binomlem  12266  binom  12267  bcxmas  12272  isumsplit  12274  arisum2  12282  trireciplem  12283  trirecip  12284  geolim  12294  cvgratnnlemnexp  12307  cvgratnnlemmn  12308  clim2prod  12322  prodfrecap  12329  fprodcl2lem  12388  fprodfac  12398  fprodshft  12401  ef0lem  12443  efval  12444  efne0  12461  efexp  12465  demoivreALT  12557  dvdsval2  12573  p1modz1  12577  dvds0lem  12584  dvds1lem  12585  dvds2lem  12586  dvdsmulc  12602  divconjdvds  12632  odd2np1lem  12655  odd2np1  12656  ltoddhalfle  12676  halfleoddlt  12677  nn0o1gt2  12688  nn0o  12690  divalglemnn  12701  divalglemeunn  12704  divalglemex  12705  divalglemeuneg  12706  flodddiv4  12719  bitsinv1  12745  gcdabs1  12782  gcddiv  12812  dvdssqim  12817  rpmulgcd  12819  bezoutr1  12826  uzwodc  12830  dvdslcm  12863  lcmeq0  12865  lcmdvds  12873  divgcdcoprm0  12895  prmind2  12914  isprm5lem  12936  isprm6  12942  rpexp  12948  sqrt2irr  12957  pwbdvdslemn  12960  pwbdvdseu  12963  nnmaxpwlemxy  12964  nn0gcdsq  12996  nn0sqdcq  13004  phicl2  13012  phibndlem  13014  hashdvds  13019  crth  13022  phimullem  13023  eulerthlem1  13025  eulerthlemfi  13026  eulerthlemrprm  13027  eulerthlemth  13030  eulerth  13031  hashgcdlem  13036  phisum  13039  odzval  13040  modprm0  13053  nnnn0modprm0  13054  pythagtriplem1  13064  pythagtriplem6  13069  pythagtriplem7  13070  pythagtriplem12  13074  pythagtriplem14  13076  pythagtriplem18  13080  pythagtriplem19  13081  pceulem  13093  pceu  13094  pcval  13095  pczpre  13096  pcdiv  13101  pcqmul  13102  pcqcl  13105  pcexp  13108  pcaddlem  13138  pcadd  13139  pcmpt  13142  pcprod  13145  pcfac  13149  expnprm  13152  prmpwdvds  13154  pockthi  13157  1arithlem2  13163  4sqlem2  13188  4sqlem3  13189  4sqlem11  13200  4sqlem12  13201  4sqlem13m  13202  4sqlem17  13206  4sqlem18  13207  4sqlem19  13208  ballotfilemfc0  13281  ballotfilemfcc  13282  ennnfonelemr  13363  ctinfom  13368  infpn2  13396  ercpbl  13701  mgm1  13739  mgmidmo  13741  ismgmid  13746  mgmlrid  13748  ismgmid2  13749  lidrideqd  13750  lidrididd  13751  mgmidsssn0  13753  grprida  13756  gzsumfzval  13760  gzsumress  13761  gzsumval2  13763  isnsgrp  13770  sgrpass  13772  sgrp1  13775  sgrpidmndm  13782  ismndd  13799  mndinvmod  13807  imasmnd2  13808  mnd1  13811  mnd1id  13812  mhmpropd  13822  insubm  13841  mhmima  13847  gsumvallem2  13849  grppropd  13871  isgrpd2  13875  isgrpd  13877  dfgrp2  13881  grprcan  13891  grpinveu  13892  grpsubval  13900  grplinv  13904  grpinvid2  13907  isgrpinv  13908  grplrinv  13911  grpidinv2  13912  grpidinv  13913  grpidssd  13930  grpinvssd  13931  dfgrp3mlem  13952  dfgrp3m  13953  grplactfval  13955  grp1  13960  imasgrp2  13962  mhmmnd  13968  ghmgrp  13970  mulgnn0gzsum  13980  mulgnn0p1  13985  mulgnn0subcl  13987  mulgaddcom  13998  mulginvcom  13999  mulgnn0z  14001  mulgneg2  14008  mulgnnass  14009  mulgnn0ass  14010  mhmmulg  14015  issubg  14025  subgex  14028  issubg2m  14041  issubg4m  14045  isnsg2  14055  nsgbi  14056  isnsg3  14059  elnmz  14060  nmzbi  14061  ghmrn  14109  ghmnsgima  14120  gzsumconst  14192  gzsumshift  14198  gsumvalfi  14201  rngdi  14288  rngdir  14289  srgrz  14337  srgmulgass  14342  srgpcomp  14343  srgrmhm  14347  ringid  14380  ringinvnzdiv  14404  mulgass2  14412  ring1  14413  ringrghm  14416  imasring  14418  dvdsrmuld  14452  dvdsrmul1  14458  dvdsr01  14460  dvreq1  14498  rhmdvdsr  14531  lringuplu  14552  issubrng  14556  issubrng2  14567  issubrg  14578  issubrg2  14598  isrrg  14620  domneq0  14630  lmodlema  14677  islmodd  14678  lmodvsmmulgdi  14709  rmodislmodlem  14736  rmodislmod  14737  lssclg  14750  lss1d  14769  lspsn  14802  sraval  14823  rnglidlmcl  14866  quscrng  14919  cnfldmulg  14962  cnfldexp  14963  gsumfsum  14972  cnfldui  14973  expghmap  14991  mulgghm2  14992  mulgrhm  14993  zrhmulg  15004  zlmval  15011  znunit  15043  assalem  15052  asclvald  15071  assamulgscmlem2  15091  assamulgscm  15092  cnmptcom  15448  psmettri2  15478  isxmet2d  15498  xmeteq0  15509  xmettri2  15511  metrest  15656  mpomulcn  15716  expcn  15719  cncfval  15722  mulc1cncf  15739  addccncf  15750  mulcncf  15758  expcncf  15759  hovera  15797  hoverb  15798  hoverlt1  15799  hovergt0  15800  ivthdich  15803  limccnp2lem  15826  dvcnp2cntop  15849  dvcoapbr  15857  dvexp  15861  dvrecap  15863  dvef  15877  plyadd  15901  plymul  15902  plycoeid3  15907  plyco  15909  plycjlemc  15910  plycj  15911  plyrecj  15913  dvply1  15915  dvply2g  15916  sincn  15919  coscn  15920  ptolemy  15975  sincosq1eq  15990  rpcxpmul2  16068  logbgcd1irr  16122  logbgcd1irraplemexp  16123  2irrexpq  16131  2irrexpqap  16133  pellexlem3  16150  mpodvdsmulf1o  16185  fsumdvdsmul  16186  sgmppw  16187  sgmmul  16191  ppiqub  16194  perfect  16199  bposlem3  16211  bposlem5  16213  lgslem4  16220  lgsval  16221  lgsfvalg  16222  lgsval2lem  16227  lgsdir2lem4  16248  lgsdir  16252  lgsdilem2  16253  lgsdi  16254  lgsne0  16255  lgsmodeq  16262  lgsdirnn0  16264  lgsdinn0  16265  gausslemma2dlem0i  16274  gausslemma2dlem1a  16275  gausslemma2dlem1f1o  16277  gausslemma2dlem2  16279  gausslemma2dlem3  16280  gausslemma2dlem4  16281  lgseisenlem2  16288  lgsquadlem2  16295  lgsquadlem3  16296  lgsquad  16297  lgsquad2lem2  16299  2lgslem1a  16305  2lgslem1b  16306  2lgslem1c  16307  2lgslem3a  16310  2lgslem3b  16311  2lgslem3c  16312  2lgslem3d  16313  2lgslem3a1  16314  2lgslem3b1  16315  2lgslem3c1  16316  2lgslem3d1  16317  2lgs  16321  2lgsoddprmlem1  16322  2lgsoddprmlem3  16328  2sqlem2  16332  2sqlem6  16337  2sqlem8  16340  2sqlem9  16341  wlklenvm1  16680  wlklenvm1g  16681  wlkl1loop  16697  2wlklem  16715  clwwlknnn  16751  clwwlknp  16756  clwwlkn1  16757  clwwlkn2  16760  clwwlkext2edg  16761  umgr2cwwk2dif  16763  clwwlknon  16768  clwwlk0on0  16770  clwwlknonex2lem1  16776  clwwlknonex2lem2  16777  clwwlknonex2  16778  qdencn  17170  isomninn  17178  trirec0  17191  iswomninn  17198  ismkvnn  17201