Theorem oveq1 6014

Description: Equality theorem for operation value. (Contributed by NM, 28-Feb-1995.)

Assertion

Ref	Expression
oveq1	⊢ (𝐴 = 𝐵 → (𝐴𝐹𝐶) = (𝐵𝐹𝐶))

Proof of Theorem oveq1

Step	Hyp	Ref	Expression
1		opeq1 3857	. . 3 ⊢ (𝐴 = 𝐵 → ⟨𝐴, 𝐶⟩ = ⟨𝐵, 𝐶⟩)
2	1	fveq2d 5633	. 2 ⊢ (𝐴 = 𝐵 → (𝐹‘⟨𝐴, 𝐶⟩) = (𝐹‘⟨𝐵, 𝐶⟩))
3		df-ov 6010	. 2 ⊢ (𝐴𝐹𝐶) = (𝐹‘⟨𝐴, 𝐶⟩)
4		df-ov 6010	. 2 ⊢ (𝐵𝐹𝐶) = (𝐹‘⟨𝐵, 𝐶⟩)
5	2, 3, 4	3eqtr4g 2287	1 ⊢ (𝐴 = 𝐵 → (𝐴𝐹𝐶) = (𝐵𝐹𝐶))

Syntax hints:   → wi 4   = wceq 1395  ⟨cop 3669  ‘cfv 5318  (class class class)co 6007

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 714  ax-5 1493  ax-7 1494  ax-gen 1495  ax-ie1 1539  ax-ie2 1540  ax-8 1550  ax-10 1551  ax-11 1552  ax-i12 1553  ax-bndl 1555  ax-4 1556  ax-17 1572  ax-i9 1576  ax-ial 1580  ax-i5r 1581  ax-ext 2211

This theorem depends on definitions:  df-bi 117  df-3an 1004  df-tru 1398  df-nf 1507  df-sb 1809  df-clab 2216  df-cleq 2222  df-clel 2225  df-nfc 2361  df-rex 2514  df-v 2801  df-un 3201  df-sn 3672  df-pr 3673  df-op 3675  df-uni 3889  df-br 4084  df-iota 5278  df-fv 5326  df-ov 6010

This theorem is referenced by:  oveq12  6016  oveq1i  6017  oveq1d  6022  ovrspc2v  6033  oveqrspc2v  6034  rspceov  6050  fovcld  6115  ovmpos  6134  ov2gf  6135  ovi3  6148  caovclg  6164  caovcomg  6167  caovassg  6170  caovcang  6173  caovcan  6176  caovordig  6177  caovordg  6179  caovord  6183  caovdig  6186  caovdirg  6189  caovimo  6205  suppssov1  6221  off  6237  caofid0r  6252  caofid1  6253  caofdig  6258  omcl  6615  oeicl  6616  omv2  6619  nnm0r  6633  nnacom  6638  nndi  6640  nnmass  6641  nnmsucr  6642  nnmcom  6643  nnaword  6665  nnmord  6671  nnm00  6684  eroveu  6781  th3qlem2  6793  th3q  6795  ecovcom  6797  ecovicom  6798  ecovass  6799  ecoviass  6800  ecovdi  6801  ecovidi  6802  map0g  6843  addcmpblnq  7565  addclnq  7573  mulclnq  7574  mulidnq  7587  recexnq  7588  recmulnqg  7589  ltanqg  7598  ltmnqg  7599  ltexnqq  7606  enq0ref  7631  enq0tr  7632  addcmpblnq0  7641  mulnnnq0  7648  addclnq0  7649  mulclnq0  7650  distrnq0  7657  mulcomnq0  7658  addassnq0  7660  prarloclemlo  7692  prarloclem3  7695  prarloclem5  7698  prarloclemcalc  7700  genipv  7707  genpassl  7722  genpassu  7723  addlocprlemeq  7731  distrlem4prl  7782  distrlem4pru  7783  ltexprlemdisj  7804  ltexprlemloc  7805  ltexprlemrl  7808  ltexprlemru  7810  prplnqu  7818  cauappcvgprlemm  7843  cauappcvgprlemopl  7844  cauappcvgprlemlol  7845  cauappcvgprlemdisj  7849  cauappcvgprlemloc  7850  cauappcvgprlemladdfl  7853  cauappcvgprlemladdru  7854  cauappcvgprlemladdrl  7855  cauappcvgprlem1  7857  cauappcvgprlemlim  7859  cauappcvgpr  7860  caucvgprlemm  7866  caucvgprlemopl  7867  caucvgprlemlol  7868  caucvgprlemdisj  7872  caucvgprlemloc  7873  caucvgprlemladdrl  7876  caucvgprlem1  7877  caucvgpr  7880  caucvgprprlemell  7883  caucvgprprlemml  7892  caucvgprpr  7910  mulcmpblnrlemg  7938  addclsr  7951  mulclsr  7952  0idsr  7965  1idsr  7966  00sr  7967  ltasrg  7968  recexgt0sr  7971  mulgt0sr  7976  mulextsr1  7979  prsrriota  7986  caucvgsrlemgt1  7993  caucvgsrlemoffres  7998  pitonn  8046  peano2nnnn  8051  axaddrcl  8063  axmulrcl  8065  axaddcom  8068  ax1rid  8075  ax0id  8076  axprecex  8078  axcnre  8079  axpre-ltadd  8084  axpre-mulgt0  8085  axpre-mulext  8086  rereceu  8087  peano5nnnn  8090  axcaucvglemcau  8096  axcaucvglemres  8097  mulrid  8154  cnegexlem1  8332  cnegexlem2  8333  cnegex  8335  addcan2  8338  subval  8349  addlsub  8527  apreim  8761  recexap  8811  receuap  8827  divvalap  8832  cju  9119  peano2nn  9133  nn1m1nn  9139  nn1suc  9140  nnsub  9160  fv0p1e1  9236  nnm1nn0  9421  zdiv  9546  zneo  9559  nneoor  9560  zeo  9563  peano5uzti  9566  nn0ind-raph  9575  uzind4s  9797  uzind4s2  9798  qmulz  9830  elpq  9856  cnref1o  9858  nn0ledivnn  9975  xaddnemnf  10065  xaddnepnf  10066  xaddcom  10069  xaddid1  10070  xnn0xadd0  10075  xaddass  10077  xpncan  10079  xleadd1a  10081  xltadd1  10084  xlt2add  10088  xsubge0  10089  xposdif  10090  xlesubadd  10091  xleaddadd  10095  fzsuc2  10287  fzm1  10308  fzoval  10356  exbtwnzlemstep  10479  exbtwnzlemshrink  10480  exbtwnzlemex  10481  exbtwnz  10482  rebtwn2zlemstep  10484  rebtwn2zlemshrink  10485  rebtwn2z  10486  flqlelt  10508  flqbi  10522  fldiv4p1lem1div2  10537  fldiv4lem1div2  10539  modqval  10558  modqadd1  10595  modqmuladd  10600  modqmuladdnn0  10602  modqm1p1mod0  10609  modqmul1  10611  modfzo0difsn  10629  addmodlteq  10632  frec2uzzd  10634  frec2uzsucd  10635  frec2uzrand  10639  frecuzrdgrrn  10642  frec2uzrdg  10643  frecuzrdgrcl  10644  frecuzrdgsuc  10648  frecuzrdgrclt  10649  frecuzrdgg  10650  frecuzrdgdom  10652  frecuzrdgfun  10654  frecuzrdgsuctlem  10657  frecuzrdgsuct  10658  uzsinds  10678  iseqvalcbv  10693  seq3val  10694  seqvalcd  10695  seqf  10698  seq3p1  10699  seqovcd  10701  seqp1cd  10704  seq3fveq2  10709  seqfveq2g  10711  seq3shft2  10715  seqshft2g  10716  monoord  10719  monoord2  10720  seq3split  10722  seqsplitg  10723  seq3caopr3  10725  seqcaopr3g  10726  seq3caopr2  10727  seqcaopr2g  10728  iseqf1olemqval  10734  iseqf1olemqk  10741  seqf1oglem2a  10752  seqf1oglem2  10754  seq3id2  10760  seq3homo  10761  seq3z  10762  seqhomog  10764  seqfeq4g  10765  seq3distr  10766  m1expcl2  10795  mulexp  10812  expadd  10815  expmul  10818  sq0i  10865  qsqeqor  10884  sqoddm1div8  10927  facp1  10964  faclbnd  10975  faclbnd3  10977  bcval  10983  bcn1  10992  bcval5  10997  bcpasc  11000  bccl  11001  hashfz1  11017  omgadd  11036  hashfzo  11057  hashfzp1  11059  hashxp  11061  seq3coll  11077  lsw1  11134  ccats1val2  11187  ccatw2s1p2  11192  pfxsuff1eqwrdeq  11247  swrdswrd  11253  ccats1pfxeq  11262  ccatopth  11264  wrdind  11270  wrd2ind  11271  swrdccatin2  11277  pfxccatin12lem2  11279  swrdccat3blem  11287  ccats1pfxeqbi  11290  swrdccatin2d  11292  reuccatpfxs1  11295  shftlem  11343  shftfvalg  11345  shftfibg  11347  shftfval  11348  shftfib  11350  shftfn  11351  shftf  11357  2shfti  11358  shftvalg  11363  shftval4g  11364  cjval  11372  imval  11377  cjexp  11420  cnrecnv  11437  cvg1nlemcau  11511  cvg1nlemres  11512  resqrexlemcalc3  11543  resqrexlemex  11552  rsqrmo  11554  resqrtcl  11556  rersqrtthlem  11557  sqrtsq  11571  absexp  11606  recan  11636  climshft  11831  climcn1  11835  climcn2  11836  subcn2  11838  fsumshft  11971  fisum0diag2  11974  fsumiun  12004  binomlem  12010  binom  12011  bcxmas  12016  isumsplit  12018  arisum2  12026  trireciplem  12027  trirecip  12028  geolim  12038  cvgratnnlemnexp  12051  cvgratnnlemmn  12052  clim2prod  12066  prodfrecap  12073  fprodcl2lem  12132  fprodfac  12142  fprodshft  12145  ef0lem  12187  efval  12188  efne0  12205  efexp  12209  demoivreALT  12301  dvdsval2  12317  p1modz1  12321  dvds0lem  12328  dvds1lem  12329  dvds2lem  12330  dvdsmulc  12346  divconjdvds  12376  odd2np1lem  12399  odd2np1  12400  ltoddhalfle  12420  halfleoddlt  12421  nn0o1gt2  12432  nn0o  12434  divalglemnn  12445  divalglemeunn  12448  divalglemex  12449  divalglemeuneg  12450  flodddiv4  12463  bitsinv1  12489  gcdabs1  12526  gcddiv  12556  dvdssqim  12561  rpmulgcd  12563  bezoutr1  12570  uzwodc  12574  dvdslcm  12607  lcmeq0  12609  lcmdvds  12617  divgcdcoprm0  12639  prmind2  12658  isprm5lem  12679  isprm6  12685  rpexp  12691  sqrt2irr  12700  pw2dvdslemn  12703  pw2dvdseu  12706  oddpwdclemxy  12707  nn0gcdsq  12738  phicl2  12752  phibndlem  12754  hashdvds  12759  crth  12762  phimullem  12763  eulerthlem1  12765  eulerthlemfi  12766  eulerthlemrprm  12767  eulerthlemth  12770  eulerth  12771  hashgcdlem  12776  phisum  12779  odzval  12780  modprm0  12793  nnnn0modprm0  12794  pythagtriplem1  12804  pythagtriplem6  12809  pythagtriplem7  12810  pythagtriplem12  12814  pythagtriplem14  12816  pythagtriplem18  12820  pythagtriplem19  12821  pceulem  12833  pceu  12834  pcval  12835  pczpre  12836  pcdiv  12841  pcqmul  12842  pcqcl  12845  pcexp  12848  pcaddlem  12878  pcadd  12879  pcmpt  12882  pcprod  12885  pcfac  12889  expnprm  12892  prmpwdvds  12894  pockthi  12897  1arithlem2  12903  4sqlem2  12928  4sqlem3  12929  4sqlem11  12940  4sqlem12  12941  4sqlem13m  12942  4sqlem17  12946  4sqlem18  12947  4sqlem19  12948  ennnfonelemr  13010  ctinfom  13015  infpn2  13043  ercpbl  13380  mgm1  13419  mgmidmo  13421  ismgmid  13426  mgmlrid  13428  ismgmid2  13429  lidrideqd  13430  lidrididd  13431  mgmidsssn0  13433  grprida  13436  gsumfzval  13440  gsumress  13444  gsumval2  13446  isnsgrp  13455  sgrpass  13457  sgrp1  13460  sgrpidmndm  13469  ismndd  13486  mndinvmod  13494  imasmnd2  13501  mnd1  13504  mnd1id  13505  mhmpropd  13515  insubm  13534  mhmima  13540  gsumvallem2  13542  grppropd  13566  isgrpd2  13570  isgrpd  13572  dfgrp2  13576  grprcan  13586  grpinveu  13587  grpsubval  13595  grplinv  13599  grpinvid2  13602  isgrpinv  13603  grplrinv  13606  grpidinv2  13607  grpidinv  13608  grpidssd  13625  grpinvssd  13626  dfgrp3mlem  13647  dfgrp3m  13648  grplactfval  13650  grp1  13655  imasgrp2  13663  mhmmnd  13669  ghmgrp  13671  mulgnn0gsum  13681  mulgnn0p1  13686  mulgnn0subcl  13688  mulgaddcom  13699  mulginvcom  13700  mulgnn0z  13702  mulgneg2  13709  mulgnnass  13710  mulgnn0ass  13711  mhmmulg  13716  issubg  13726  subgex  13729  issubg2m  13742  issubg4m  13746  isnsg2  13756  nsgbi  13757  isnsg3  13760  elnmz  13761  nmzbi  13762  ghmrn  13810  ghmnsgima  13821  gsumfzconst  13894  rngdi  13919  rngdir  13920  srgrz  13963  srgmulgass  13968  srgpcomp  13969  srgrmhm  13973  ringid  14005  ringinvnzdiv  14029  mulgass2  14037  ring1  14038  ringrghm  14041  imasring  14043  dvdsrmuld  14076  dvdsrmul1  14082  dvdsr01  14084  dvreq1  14122  rhmdvdsr  14155  lringuplu  14176  issubrng  14179  issubrng2  14190  issubrg  14201  issubrg2  14221  isrrg  14243  domneq0  14252  lmodlema  14272  islmodd  14273  lmodvsmmulgdi  14303  rmodislmodlem  14330  rmodislmod  14331  lssclg  14344  lss1d  14363  lspsn  14396  sraval  14417  rnglidlmcl  14460  quscrng  14513  cnfldmulg  14556  cnfldexp  14557  gsumfzfsumlemm  14567  cnfldui  14569  expghmap  14587  mulgghm2  14588  mulgrhm  14589  zrhmulg  14600  zlmval  14607  znunit  14639  cnmptcom  14988  psmettri2  15018  isxmet2d  15038  xmeteq0  15049  xmettri2  15051  metrest  15196  mpomulcn  15256  expcn  15259  cncfval  15262  mulc1cncf  15279  addccncf  15290  mulcncf  15298  expcncf  15299  hovera  15337  hoverb  15338  hoverlt1  15339  hovergt0  15340  ivthdich  15343  limccnp2lem  15366  dvcnp2cntop  15389  dvcoapbr  15397  dvexp  15401  dvrecap  15403  dvef  15417  plyadd  15441  plymul  15442  plycoeid3  15447  plyco  15449  plycjlemc  15450  plycj  15451  plyrecj  15453  dvply1  15455  dvply2g  15456  sincn  15459  coscn  15460  ptolemy  15514  sincosq1eq  15529  rpcxpmul2  15603  logbgcd1irr  15657  logbgcd1irraplemexp  15658  2irrexpq  15666  2irrexpqap  15668  mpodvdsmulf1o  15680  fsumdvdsmul  15681  sgmppw  15682  sgmmul  15686  perfect  15691  lgslem4  15698  lgsval  15699  lgsfvalg  15700  lgsval2lem  15705  lgsdir2lem4  15726  lgsdir  15730  lgsdilem2  15731  lgsdi  15732  lgsne0  15733  lgsmodeq  15740  lgsdirnn0  15742  lgsdinn0  15743  gausslemma2dlem0i  15752  gausslemma2dlem1a  15753  gausslemma2dlem1f1o  15755  gausslemma2dlem2  15757  gausslemma2dlem3  15758  gausslemma2dlem4  15759  lgseisenlem2  15766  lgsquadlem2  15773  lgsquadlem3  15774  lgsquad  15775  lgsquad2lem2  15777  2lgslem1a  15783  2lgslem1b  15784  2lgslem1c  15785  2lgslem3a  15788  2lgslem3b  15789  2lgslem3c  15790  2lgslem3d  15791  2lgslem3a1  15792  2lgslem3b1  15793  2lgslem3c1  15794  2lgslem3d1  15795  2lgs  15799  2lgsoddprmlem1  15800  2lgsoddprmlem3  15806  2sqlem2  15810  2sqlem6  15815  2sqlem8  15818  2sqlem9  15819  wlklenvm1  16087  wlklenvm1g  16088  wlkl1loop  16104  2wlklem  16120  clwwlknnn  16155  clwwlknp  16159  clwwlkn1  16160  clwwlkn2  16163  clwwlkext2edg  16164  umgr2cwwk2dif  16166  qdencn  16483  isomninn  16487  trirec0  16500  iswomninn  16506  ismkvnn  16509