Theorem oveq1 6095

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 5702	. 2 |- ( A = B -> ( F ` <. A , C >. ) = ( F ` <. B , C >. ) )
3		df-ov 6091	. 2 |- ( A F C ) = ( F ` <. A , C >. )
4		df-ov 6091	. 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 5380  (class class class)co 6088

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 4132  df-iota 5340  df-fv 5388  df-ov 6091

This theorem is used by:  oveq12  6097  oveq1i  6098  oveq1d  6103  ovrspc2v  6114  oveqrspc2v  6115  rspceov  6131  fovcld  6196  ovmpos  6215  ov2gf  6216  ovi3  6229  caovclg  6245  caovcomg  6248  caovassg  6251  caovcang  6254  caovcan  6257  caovordig  6258  caovordg  6260  caovord  6264  caovdig  6267  caovdirg  6270  caovimo  6286  suppssov1  6302  off  6319  caofid0r  6334  caofid1  6335  caofdig  6340  suppofss1dcl  6508  suppofss2dcl  6509  omcl  6738  oeicl  6739  omv2  6742  nnm0r  6756  nnacom  6761  nndi  6763  nnmass  6764  nnmsucr  6765  nnmcom  6766  nnaword  6788  nnmord  6794  nnm00  6807  eroveu  6904  th3qlem2  6916  th3q  6918  ecovcom  6920  ecovicom  6921  ecovass  6922  ecoviass  6923  ecovdi  6924  ecovidi  6925  map0g  6973  addcmpblnq  7740  addclnq  7748  mulclnq  7749  mulidnq  7762  recexnq  7763  recmulnqg  7764  ltanqg  7773  ltmnqg  7774  ltexnqq  7781  enq0ref  7806  enq0tr  7807  addcmpblnq0  7816  mulnnnq0  7823  addclnq0  7824  mulclnq0  7825  distrnq0  7832  mulcomnq0  7833  addassnq0  7835  prarloclemlo  7867  prarloclem3  7870  prarloclem5  7873  prarloclemcalc  7875  genipv  7882  genpassl  7897  genpassu  7898  addlocprlemeq  7906  distrlem4prl  7957  distrlem4pru  7958  ltexprlemdisj  7979  ltexprlemloc  7980  ltexprlemrl  7983  ltexprlemru  7985  prplnqu  7993  cauappcvgprlemm  8018  cauappcvgprlemopl  8019  cauappcvgprlemlol  8020  cauappcvgprlemdisj  8024  cauappcvgprlemloc  8025  cauappcvgprlemladdfl  8028  cauappcvgprlemladdru  8029  cauappcvgprlemladdrl  8030  cauappcvgprlem1  8032  cauappcvgprlemlim  8034  cauappcvgpr  8035  caucvgprlemm  8041  caucvgprlemopl  8042  caucvgprlemlol  8043  caucvgprlemdisj  8047  caucvgprlemloc  8048  caucvgprlemladdrl  8051  caucvgprlem1  8052  caucvgpr  8055  caucvgprprlemell  8058  caucvgprprlemml  8067  caucvgprpr  8085  mulcmpblnrlemg  8113  addclsr  8126  mulclsr  8127  0idsr  8140  1idsr  8141  00sr  8142  ltasrg  8143  recexgt0sr  8146  mulgt0sr  8151  mulextsr1  8154  prsrriota  8161  caucvgsrlemgt1  8168  caucvgsrlemoffres  8173  pitonn  8221  peano2nnnn  8226  axaddrcl  8238  axmulrcl  8240  axaddcom  8243  ax1rid  8250  ax0id  8251  axprecex  8253  axcnre  8254  axpre-ltadd  8259  axpre-mulgt0  8260  axpre-mulext  8261  rereceu  8262  peano5nnnn  8265  axcaucvglemcau  8271  axcaucvglemres  8272  mulrid  8329  cnegexlem1  8508  cnegexlem2  8509  cnegex  8511  addcan2  8514  subval  8525  addlsub  8703  apreim  8939  recexap  8989  receuap  9007  divvalap  9012  cju  9299  peano2nn  9325  nn1m1nn  9331  nn1suc  9332  nnsub  9352  fv0p1e1  9428  nnm1nn0  9615  zdiv  9745  zneo  9758  nneoor  9759  zeo  9762  peano5uzti  9765  nn0ind-raph  9774  uzind4s  10006  uzind4s2  10007  qmulz  10039  elpq  10066  cnref1o  10068  nn0ledivnn  10185  xaddnemnf  10276  xaddnepnf  10277  xaddcom  10280  xaddid1  10281  xnn0xadd0  10286  xaddass  10288  xpncan  10290  xleadd1a  10292  xltadd1  10295  xlt2add  10299  xsubge0  10300  xposdif  10301  xlesubadd  10302  xleaddadd  10306  fzsuc2  10503  fzm1  10524  fzoval  10572  exbtwnzlemstep  10699  exbtwnzlemshrink  10700  exbtwnzlemex  10701  exbtwnz  10702  rebtwn2zlemstep  10704  rebtwn2zlemshrink  10705  rebtwn2z  10706  flqlelt  10729  flaplelt  10730  flqbi  10746  fldiv4p1lem1div2  10761  fldiv4lem1div2  10763  modqval  10782  modqadd1  10819  modqmuladd  10824  modqmuladdnn0  10826  modqm1p1mod0  10833  modqmul1  10835  modfzo0difsn  10853  addmodlteq  10856  frec2uzzd  10858  frec2uzsucd  10859  frec2uzrand  10863  frecuzrdgrrn  10866  frec2uzrdg  10867  frecuzrdgrcl  10868  frecuzrdgsuc  10872  frecuzrdgrclt  10873  frecuzrdgg  10874  frecuzrdgdom  10876  frecuzrdgfun  10878  frecuzrdgsuctlem  10881  frecuzrdgsuct  10882  uzsinds  10902  iseqvalcbv  10917  seq3val  10918  seqvalcd  10919  seqf  10922  seq3p1  10923  seqovcd  10925  seqp1cd  10928  seq3fveq2  10933  seqfveq2g  10935  seq3shft2  10939  seqshft2g  10940  monoord  10943  monoord2  10944  seq3split  10946  seqsplitg  10947  seq3caopr3  10949  seqcaopr3g  10950  seq3caopr2  10951  seqcaopr2g  10952  iseqf1olemqval  10958  iseqf1olemqk  10965  seqf1oglem2a  10976  seqf1oglem2  10978  seq3id2  10984  seq3homo  10985  seq3z  10986  seqhomog  10988  seqfeq4g  10989  seq3distr  10990  m1expcl2  11019  mulexp  11036  expadd  11039  expmul  11042  sq0i  11089  qsqeqor  11108  resq01  11116  sqoddm1div8  11152  facp1  11190  faclbnd  11201  faclbnd3  11203  bcval  11209  bcn1  11218  bcval5  11223  bcpasc  11226  bccl  11227  hashfz1  11244  omgadd  11264  hashfzo  11285  hashfzp1  11287  hashxp  11289  hashmap  11290  hashf1lem2  11308  seq3coll  11316  lsw1  11376  ccats1val2  11430  ccatw2s1p2  11436  pfxsuff1eqwrdeq  11493  swrdswrd  11499  ccats1pfxeq  11508  ccatopth  11510  wrdind  11516  wrd2ind  11517  swrdccatin2  11523  pfxccatin12lem2  11525  swrdccat3blem  11533  ccats1pfxeqbi  11536  swrdccatin2d  11538  reuccatpfxs1  11541  shftlem  11603  shftfvalg  11605  shftfibg  11607  shftfval  11608  shftfib  11610  shftfn  11611  shftf  11617  2shfti  11618  shftvalg  11623  shftval4g  11624  cjval  11632  imval  11637  cjexp  11680  sq01  11682  cnrecnv  11698  cvg1nlemcau  11772  cvg1nlemres  11773  resqrexlemcalc3  11804  resqrexlemex  11813  rsqrmo  11815  resqrtcl  11817  rersqrtthlem  11818  sqrtsq  11832  absexp  11868  recan  11898  climshft  12095  climcn1  12099  climcn2  12100  subcn2  12102  fsumshft  12236  fisum0diag2  12239  fsumiun  12269  binomlem  12275  binom  12276  bcxmas  12281  isumsplit  12283  arisum2  12291  trireciplem  12292  trirecip  12293  geolim  12303  cvgratnnlemnexp  12316  cvgratnnlemmn  12317  clim2prod  12331  prodfrecap  12338  fprodcl2lem  12397  fprodfac  12407  fprodshft  12410  ef0lem  12452  efval  12453  efne0  12470  efexp  12474  demoivreALT  12566  dvdsval2  12582  p1modz1  12586  dvds0lem  12593  dvds1lem  12594  dvds2lem  12595  dvdsmulc  12611  divconjdvds  12641  odd2np1lem  12664  odd2np1  12665  ltoddhalfle  12685  halfleoddlt  12686  nn0o1gt2  12697  nn0o  12699  divalglemnn  12710  divalglemeunn  12713  divalglemex  12714  divalglemeuneg  12715  flodddiv4  12728  bitsinv1  12754  gcdabs1  12791  gcddiv  12821  dvdssqim  12826  rpmulgcd  12828  bezoutr1  12835  uzwodc  12839  dvdslcm  12872  lcmeq0  12874  lcmdvds  12882  divgcdcoprm0  12904  prmind2  12923  isprm5lem  12945  isprm6  12951  rpexp  12957  sqrt2irr  12966  pwbdvdslemn  12969  pwbdvdseu  12972  nnmaxpwlemxy  12973  nn0gcdsq  13005  nn0sqdcq  13013  phicl2  13021  phibndlem  13023  hashdvds  13028  crth  13031  phimullem  13032  eulerthlem1  13034  eulerthlemfi  13035  eulerthlemrprm  13036  eulerthlemth  13039  eulerth  13040  hashgcdlem  13045  phisum  13048  odzval  13049  modprm0  13062  nnnn0modprm0  13063  pythagtriplem1  13073  pythagtriplem6  13078  pythagtriplem7  13079  pythagtriplem12  13083  pythagtriplem14  13085  pythagtriplem18  13089  pythagtriplem19  13090  pceulem  13102  pceu  13103  pcval  13104  pczpre  13105  pcdiv  13110  pcqmul  13111  pcqcl  13114  pcexp  13117  pcaddlem  13147  pcadd  13148  pcmpt  13151  pcprod  13154  pcfac  13158  expnprm  13161  prmpwdvds  13163  pockthi  13166  1arithlem2  13172  4sqlem2  13197  4sqlem3  13198  4sqlem11  13209  4sqlem12  13210  4sqlem13m  13211  4sqlem17  13215  4sqlem18  13216  4sqlem19  13217  ballotfilemfc0  13290  ballotfilemfcc  13291  ennnfonelemr  13372  ctinfom  13377  infpn2  13405  ercpbl  13711  mgm1  13749  mgmidmo  13751  ismgmid  13756  mgmlrid  13758  ismgmid2  13759  lidrideqd  13760  lidrididd  13761  mgmidsssn0  13763  grprida  13766  gzsumfzval  13770  gzsumress  13771  gzsumval2  13773  isnsgrp  13780  sgrpass  13782  sgrp1  13785  sgrpidmndm  13792  ismndd  13809  mndinvmod  13817  imasmnd2  13818  mnd1  13821  mnd1id  13822  mhmpropd  13832  insubm  13851  mhmima  13857  gsumvallem2  13859  grppropd  13881  isgrpd2  13885  isgrpd  13887  dfgrp2  13891  grprcan  13901  grpinveu  13902  grpsubval  13910  grplinv  13914  grpinvid2  13917  isgrpinv  13918  grplrinv  13921  grpidinv2  13922  grpidinv  13923  grpidssd  13940  grpinvssd  13941  dfgrp3mlem  13962  dfgrp3m  13963  grplactfval  13965  grp1  13970  imasgrp2  13972  mhmmnd  13978  ghmgrp  13980  mulgnn0gzsum  13990  mulgnn0p1  13995  mulgnn0subcl  13997  mulgaddcom  14008  mulginvcom  14009  mulgnn0z  14011  mulgneg2  14018  mulgnnass  14019  mulgnn0ass  14020  mhmmulg  14025  issubg  14035  subgex  14038  issubg2m  14051  issubg4m  14055  isnsg2  14065  nsgbi  14066  isnsg3  14069  elnmz  14070  nmzbi  14071  ghmrn  14119  ghmnsgima  14130  elcntz  14154  cntzsnval  14156  elcntzsn  14157  cntzi  14162  cntzmhm  14173  gzsumconst  14233  gzsumshift  14239  gsumvalfi  14242  gsum2dfilem2  14272  gsum2dfi  14273  gsum2d2fi  14274  gsumcom2fi  14275  rngdi  14346  rngdir  14347  srgrz  14395  srgmulgass  14400  srgpcomp  14401  srgrmhm  14405  ringid  14438  ringinvnzdiv  14462  mulgass2  14470  ring1  14471  ringrghm  14474  gsummulc1fi  14475  imasring  14478  dvdsrmuld  14512  dvdsrmul1  14518  dvdsr01  14520  dvreq1  14558  rhmdvdsr  14591  lringuplu  14612  issubrng  14616  issubrng2  14627  issubrg  14638  issubrg2  14658  isrrg  14680  domneq0  14690  lmodlema  14737  islmodd  14738  lmodvsmmulgdi  14769  rmodislmodlem  14796  rmodislmod  14797  lssclg  14810  lss1d  14829  lspsn  14862  sraval  14883  rnglidlmcl  14926  quscrng  14979  cnfldmulg  15022  cnfldexp  15023  gsumfsum  15032  cnfldui  15033  expghmap  15051  mulgghm2  15052  mulgrhm  15053  zrhmulg  15064  zlmval  15071  znunit  15103  assalem  15112  asclvald  15131  assamulgscmlem2  15151  assamulgscm  15152  psrass1filem  15177  cnmptcom  15524  psmettri2  15554  isxmet2d  15574  xmeteq0  15585  xmettri2  15587  metrest  15732  mpomulcn  15792  expcn  15795  cncfval  15798  mulc1cncf  15815  addccncf  15826  mulcncf  15834  expcncf  15835  hovera  15873  hoverb  15874  hoverlt1  15875  hovergt0  15876  ivthdich  15879  limccnp2lem  15902  dvcnp2cntop  15925  dvcoapbr  15933  dvexp  15937  dvrecap  15939  dvef  15953  plyadd  15977  plymul  15978  plycoeid3  15983  plyco  15985  plycjlemc  15986  plycj  15987  plyrecj  15989  dvply1  15991  dvply2g  15992  sincn  15995  coscn  15996  ptolemy  16051  sincosq1eq  16066  rpcxpmul2  16146  efnthr  16176  logbgcd1irr  16203  logbgcd1irraplemexp  16204  2irrexpq  16212  2irrexpqap  16214  pellexlem3  16231  mpodvdsmulf1o  16284  fsumdvdsmul  16285  sgmppw  16286  sgmmul  16290  ppiqub  16293  perfect  16301  bposlem3  16313  bposlem5  16315  bposlem6  16316  bposlem8  16318  lgslem4  16327  lgsval  16328  lgsfvalg  16329  lgsval2lem  16334  lgsdir2lem4  16355  lgsdir  16359  lgsdilem2  16360  lgsdi  16361  lgsne0  16362  lgsmodeq  16369  lgsdirnn0  16371  lgsdinn0  16372  gausslemma2dlem0i  16381  gausslemma2dlem1a  16382  gausslemma2dlem1f1o  16384  gausslemma2dlem2  16386  gausslemma2dlem3  16387  gausslemma2dlem4  16388  lgseisenlem2  16395  lgsquadlem2  16402  lgsquadlem3  16403  lgsquad  16404  lgsquad2lem2  16406  2lgslem1a  16412  2lgslem1b  16413  2lgslem1c  16414  2lgslem3a  16417  2lgslem3b  16418  2lgslem3c  16419  2lgslem3d  16420  2lgslem3a1  16421  2lgslem3b1  16422  2lgslem3c1  16423  2lgslem3d1  16424  2lgs  16428  2lgsoddprmlem1  16429  2lgsoddprmlem3  16435  2sqlem2  16439  2sqlem6  16444  2sqlem8  16447  2sqlem9  16448  wlklenvm1  16787  wlklenvm1g  16788  wlkl1loop  16804  2wlklem  16822  clwwlknnn  16858  clwwlknp  16863  clwwlkn1  16864  clwwlkn2  16867  clwwlkext2edg  16868  umgr2cwwk2dif  16870  clwwlknon  16875  clwwlk0on0  16877  clwwlknonex2lem1  16883  clwwlknonex2lem2  16884  clwwlknonex2  16885  qdencn  17278  isomninn  17286  trirec0  17300  iswomninn  17307  ismkvnn  17310