Theorem oveq1 6008

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 5631	. 2 ⊢ (𝐴 = 𝐵 → (𝐹‘⟨𝐴, 𝐶⟩) = (𝐹‘⟨𝐵, 𝐶⟩))
3		df-ov 6004	. 2 ⊢ (𝐴𝐹𝐶) = (𝐹‘⟨𝐴, 𝐶⟩)
4		df-ov 6004	. 2 ⊢ (𝐵𝐹𝐶) = (𝐹‘⟨𝐵, 𝐶⟩)
5	2, 3, 4	3eqtr4g 2287	1 ⊢ (𝐴 = 𝐵 → (𝐴𝐹𝐶) = (𝐵𝐹𝐶))

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

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 6004

This theorem is referenced by:  oveq12  6010  oveq1i  6011  oveq1d  6016  ovrspc2v  6027  oveqrspc2v  6028  rspceov  6044  fovcld  6109  ovmpos  6128  ov2gf  6129  ovi3  6142  caovclg  6158  caovcomg  6161  caovassg  6164  caovcang  6167  caovcan  6170  caovordig  6171  caovordg  6173  caovord  6177  caovdig  6180  caovdirg  6183  caovimo  6199  suppssov1  6215  off  6231  caofid0r  6246  caofid1  6247  caofdig  6252  omcl  6607  oeicl  6608  omv2  6611  nnm0r  6625  nnacom  6630  nndi  6632  nnmass  6633  nnmsucr  6634  nnmcom  6635  nnaword  6657  nnmord  6663  nnm00  6676  eroveu  6773  th3qlem2  6785  th3q  6787  ecovcom  6789  ecovicom  6790  ecovass  6791  ecoviass  6792  ecovdi  6793  ecovidi  6794  map0g  6835  addcmpblnq  7554  addclnq  7562  mulclnq  7563  mulidnq  7576  recexnq  7577  recmulnqg  7578  ltanqg  7587  ltmnqg  7588  ltexnqq  7595  enq0ref  7620  enq0tr  7621  addcmpblnq0  7630  mulnnnq0  7637  addclnq0  7638  mulclnq0  7639  distrnq0  7646  mulcomnq0  7647  addassnq0  7649  prarloclemlo  7681  prarloclem3  7684  prarloclem5  7687  prarloclemcalc  7689  genipv  7696  genpassl  7711  genpassu  7712  addlocprlemeq  7720  distrlem4prl  7771  distrlem4pru  7772  ltexprlemdisj  7793  ltexprlemloc  7794  ltexprlemrl  7797  ltexprlemru  7799  prplnqu  7807  cauappcvgprlemm  7832  cauappcvgprlemopl  7833  cauappcvgprlemlol  7834  cauappcvgprlemdisj  7838  cauappcvgprlemloc  7839  cauappcvgprlemladdfl  7842  cauappcvgprlemladdru  7843  cauappcvgprlemladdrl  7844  cauappcvgprlem1  7846  cauappcvgprlemlim  7848  cauappcvgpr  7849  caucvgprlemm  7855  caucvgprlemopl  7856  caucvgprlemlol  7857  caucvgprlemdisj  7861  caucvgprlemloc  7862  caucvgprlemladdrl  7865  caucvgprlem1  7866  caucvgpr  7869  caucvgprprlemell  7872  caucvgprprlemml  7881  caucvgprpr  7899  mulcmpblnrlemg  7927  addclsr  7940  mulclsr  7941  0idsr  7954  1idsr  7955  00sr  7956  ltasrg  7957  recexgt0sr  7960  mulgt0sr  7965  mulextsr1  7968  prsrriota  7975  caucvgsrlemgt1  7982  caucvgsrlemoffres  7987  pitonn  8035  peano2nnnn  8040  axaddrcl  8052  axmulrcl  8054  axaddcom  8057  ax1rid  8064  ax0id  8065  axprecex  8067  axcnre  8068  axpre-ltadd  8073  axpre-mulgt0  8074  axpre-mulext  8075  rereceu  8076  peano5nnnn  8079  axcaucvglemcau  8085  axcaucvglemres  8086  mulrid  8143  cnegexlem1  8321  cnegexlem2  8322  cnegex  8324  addcan2  8327  subval  8338  addlsub  8516  apreim  8750  recexap  8800  receuap  8816  divvalap  8821  cju  9108  peano2nn  9122  nn1m1nn  9128  nn1suc  9129  nnsub  9149  fv0p1e1  9225  nnm1nn0  9410  zdiv  9535  zneo  9548  nneoor  9549  zeo  9552  peano5uzti  9555  nn0ind-raph  9564  uzind4s  9785  uzind4s2  9786  qmulz  9818  elpq  9844  cnref1o  9846  nn0ledivnn  9963  xaddnemnf  10053  xaddnepnf  10054  xaddcom  10057  xaddid1  10058  xnn0xadd0  10063  xaddass  10065  xpncan  10067  xleadd1a  10069  xltadd1  10072  xlt2add  10076  xsubge0  10077  xposdif  10078  xlesubadd  10079  xleaddadd  10083  fzsuc2  10275  fzm1  10296  fzoval  10344  exbtwnzlemstep  10467  exbtwnzlemshrink  10468  exbtwnzlemex  10469  exbtwnz  10470  rebtwn2zlemstep  10472  rebtwn2zlemshrink  10473  rebtwn2z  10474  flqlelt  10496  flqbi  10510  fldiv4p1lem1div2  10525  fldiv4lem1div2  10527  modqval  10546  modqadd1  10583  modqmuladd  10588  modqmuladdnn0  10590  modqm1p1mod0  10597  modqmul1  10599  modfzo0difsn  10617  addmodlteq  10620  frec2uzzd  10622  frec2uzsucd  10623  frec2uzrand  10627  frecuzrdgrrn  10630  frec2uzrdg  10631  frecuzrdgrcl  10632  frecuzrdgsuc  10636  frecuzrdgrclt  10637  frecuzrdgg  10638  frecuzrdgdom  10640  frecuzrdgfun  10642  frecuzrdgsuctlem  10645  frecuzrdgsuct  10646  uzsinds  10666  iseqvalcbv  10681  seq3val  10682  seqvalcd  10683  seqf  10686  seq3p1  10687  seqovcd  10689  seqp1cd  10692  seq3fveq2  10697  seqfveq2g  10699  seq3shft2  10703  seqshft2g  10704  monoord  10707  monoord2  10708  seq3split  10710  seqsplitg  10711  seq3caopr3  10713  seqcaopr3g  10714  seq3caopr2  10715  seqcaopr2g  10716  iseqf1olemqval  10722  iseqf1olemqk  10729  seqf1oglem2a  10740  seqf1oglem2  10742  seq3id2  10748  seq3homo  10749  seq3z  10750  seqhomog  10752  seqfeq4g  10753  seq3distr  10754  m1expcl2  10783  mulexp  10800  expadd  10803  expmul  10806  sq0i  10853  qsqeqor  10872  sqoddm1div8  10915  facp1  10952  faclbnd  10963  faclbnd3  10965  bcval  10971  bcn1  10980  bcval5  10985  bcpasc  10988  bccl  10989  hashfz1  11005  omgadd  11024  hashfzo  11044  hashfzp1  11046  hashxp  11048  seq3coll  11064  lsw1  11121  ccats1val2  11171  ccatw2s1p2  11176  pfxsuff1eqwrdeq  11231  swrdswrd  11237  ccats1pfxeq  11246  ccatopth  11248  wrdind  11254  wrd2ind  11255  swrdccatin2  11261  pfxccatin12lem2  11263  swrdccat3blem  11271  ccats1pfxeqbi  11274  swrdccatin2d  11276  reuccatpfxs1  11279  shftlem  11327  shftfvalg  11329  shftfibg  11331  shftfval  11332  shftfib  11334  shftfn  11335  shftf  11341  2shfti  11342  shftvalg  11347  shftval4g  11348  cjval  11356  imval  11361  cjexp  11404  cnrecnv  11421  cvg1nlemcau  11495  cvg1nlemres  11496  resqrexlemcalc3  11527  resqrexlemex  11536  rsqrmo  11538  resqrtcl  11540  rersqrtthlem  11541  sqrtsq  11555  absexp  11590  recan  11620  climshft  11815  climcn1  11819  climcn2  11820  subcn2  11822  fsumshft  11955  fisum0diag2  11958  fsumiun  11988  binomlem  11994  binom  11995  bcxmas  12000  isumsplit  12002  arisum2  12010  trireciplem  12011  trirecip  12012  geolim  12022  cvgratnnlemnexp  12035  cvgratnnlemmn  12036  clim2prod  12050  prodfrecap  12057  fprodcl2lem  12116  fprodfac  12126  fprodshft  12129  ef0lem  12171  efval  12172  efne0  12189  efexp  12193  demoivreALT  12285  dvdsval2  12301  p1modz1  12305  dvds0lem  12312  dvds1lem  12313  dvds2lem  12314  dvdsmulc  12330  divconjdvds  12360  odd2np1lem  12383  odd2np1  12384  ltoddhalfle  12404  halfleoddlt  12405  nn0o1gt2  12416  nn0o  12418  divalglemnn  12429  divalglemeunn  12432  divalglemex  12433  divalglemeuneg  12434  flodddiv4  12447  bitsinv1  12473  gcdabs1  12510  gcddiv  12540  dvdssqim  12545  rpmulgcd  12547  bezoutr1  12554  uzwodc  12558  dvdslcm  12591  lcmeq0  12593  lcmdvds  12601  divgcdcoprm0  12623  prmind2  12642  isprm5lem  12663  isprm6  12669  rpexp  12675  sqrt2irr  12684  pw2dvdslemn  12687  pw2dvdseu  12690  oddpwdclemxy  12691  nn0gcdsq  12722  phicl2  12736  phibndlem  12738  hashdvds  12743  crth  12746  phimullem  12747  eulerthlem1  12749  eulerthlemfi  12750  eulerthlemrprm  12751  eulerthlemth  12754  eulerth  12755  hashgcdlem  12760  phisum  12763  odzval  12764  modprm0  12777  nnnn0modprm0  12778  pythagtriplem1  12788  pythagtriplem6  12793  pythagtriplem7  12794  pythagtriplem12  12798  pythagtriplem14  12800  pythagtriplem18  12804  pythagtriplem19  12805  pceulem  12817  pceu  12818  pcval  12819  pczpre  12820  pcdiv  12825  pcqmul  12826  pcqcl  12829  pcexp  12832  pcaddlem  12862  pcadd  12863  pcmpt  12866  pcprod  12869  pcfac  12873  expnprm  12876  prmpwdvds  12878  pockthi  12881  1arithlem2  12887  4sqlem2  12912  4sqlem3  12913  4sqlem11  12924  4sqlem12  12925  4sqlem13m  12926  4sqlem17  12930  4sqlem18  12931  4sqlem19  12932  ennnfonelemr  12994  ctinfom  12999  infpn2  13027  ercpbl  13364  mgm1  13403  mgmidmo  13405  ismgmid  13410  mgmlrid  13412  ismgmid2  13413  lidrideqd  13414  lidrididd  13415  mgmidsssn0  13417  grprida  13420  gsumfzval  13424  gsumress  13428  gsumval2  13430  isnsgrp  13439  sgrpass  13441  sgrp1  13444  sgrpidmndm  13453  ismndd  13470  mndinvmod  13478  imasmnd2  13485  mnd1  13488  mnd1id  13489  mhmpropd  13499  insubm  13518  mhmima  13524  gsumvallem2  13526  grppropd  13550  isgrpd2  13554  isgrpd  13556  dfgrp2  13560  grprcan  13570  grpinveu  13571  grpsubval  13579  grplinv  13583  grpinvid2  13586  isgrpinv  13587  grplrinv  13590  grpidinv2  13591  grpidinv  13592  grpidssd  13609  grpinvssd  13610  dfgrp3mlem  13631  dfgrp3m  13632  grplactfval  13634  grp1  13639  imasgrp2  13647  mhmmnd  13653  ghmgrp  13655  mulgnn0gsum  13665  mulgnn0p1  13670  mulgnn0subcl  13672  mulgaddcom  13683  mulginvcom  13684  mulgnn0z  13686  mulgneg2  13693  mulgnnass  13694  mulgnn0ass  13695  mhmmulg  13700  issubg  13710  subgex  13713  issubg2m  13726  issubg4m  13730  isnsg2  13740  nsgbi  13741  isnsg3  13744  elnmz  13745  nmzbi  13746  ghmrn  13794  ghmnsgima  13805  gsumfzconst  13878  rngdi  13903  rngdir  13904  srgrz  13947  srgmulgass  13952  srgpcomp  13953  srgrmhm  13957  ringid  13989  ringinvnzdiv  14013  mulgass2  14021  ring1  14022  ringrghm  14025  imasring  14027  dvdsrmuld  14060  dvdsrmul1  14066  dvdsr01  14068  dvreq1  14106  rhmdvdsr  14139  lringuplu  14160  issubrng  14163  issubrng2  14174  issubrg  14185  issubrg2  14205  isrrg  14227  domneq0  14236  lmodlema  14256  islmodd  14257  lmodvsmmulgdi  14287  rmodislmodlem  14314  rmodislmod  14315  lssclg  14328  lss1d  14347  lspsn  14380  sraval  14401  rnglidlmcl  14444  quscrng  14497  cnfldmulg  14540  cnfldexp  14541  gsumfzfsumlemm  14551  cnfldui  14553  expghmap  14571  mulgghm2  14572  mulgrhm  14573  zrhmulg  14584  zlmval  14591  znunit  14623  cnmptcom  14972  psmettri2  15002  isxmet2d  15022  xmeteq0  15033  xmettri2  15035  metrest  15180  mpomulcn  15240  expcn  15243  cncfval  15246  mulc1cncf  15263  addccncf  15274  mulcncf  15282  expcncf  15283  hovera  15321  hoverb  15322  hoverlt1  15323  hovergt0  15324  ivthdich  15327  limccnp2lem  15350  dvcnp2cntop  15373  dvcoapbr  15381  dvexp  15385  dvrecap  15387  dvef  15401  plyadd  15425  plymul  15426  plycoeid3  15431  plyco  15433  plycjlemc  15434  plycj  15435  plyrecj  15437  dvply1  15439  dvply2g  15440  sincn  15443  coscn  15444  ptolemy  15498  sincosq1eq  15513  rpcxpmul2  15587  logbgcd1irr  15641  logbgcd1irraplemexp  15642  2irrexpq  15650  2irrexpqap  15652  mpodvdsmulf1o  15664  fsumdvdsmul  15665  sgmppw  15666  sgmmul  15670  perfect  15675  lgslem4  15682  lgsval  15683  lgsfvalg  15684  lgsval2lem  15689  lgsdir2lem4  15710  lgsdir  15714  lgsdilem2  15715  lgsdi  15716  lgsne0  15717  lgsmodeq  15724  lgsdirnn0  15726  lgsdinn0  15727  gausslemma2dlem0i  15736  gausslemma2dlem1a  15737  gausslemma2dlem1f1o  15739  gausslemma2dlem2  15741  gausslemma2dlem3  15742  gausslemma2dlem4  15743  lgseisenlem2  15750  lgsquadlem2  15757  lgsquadlem3  15758  lgsquad  15759  lgsquad2lem2  15761  2lgslem1a  15767  2lgslem1b  15768  2lgslem1c  15769  2lgslem3a  15772  2lgslem3b  15773  2lgslem3c  15774  2lgslem3d  15775  2lgslem3a1  15776  2lgslem3b1  15777  2lgslem3c1  15778  2lgslem3d1  15779  2lgs  15783  2lgsoddprmlem1  15784  2lgsoddprmlem3  15790  2sqlem2  15794  2sqlem6  15799  2sqlem8  15802  2sqlem9  15803  wlklenvm1  16052  wlklenvm1g  16053  wlkl1loop  16069  qdencn  16395  isomninn  16399  trirec0  16412  iswomninn  16418  ismkvnn  16421