Theorem oveq1 6025

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 3862	. . 3 ⊢ (𝐴 = 𝐵 → ⟨𝐴, 𝐶⟩ = ⟨𝐵, 𝐶⟩)
2	1	fveq2d 5643	. 2 ⊢ (𝐴 = 𝐵 → (𝐹‘⟨𝐴, 𝐶⟩) = (𝐹‘⟨𝐵, 𝐶⟩))
3		df-ov 6021	. 2 ⊢ (𝐴𝐹𝐶) = (𝐹‘⟨𝐴, 𝐶⟩)
4		df-ov 6021	. 2 ⊢ (𝐵𝐹𝐶) = (𝐹‘⟨𝐵, 𝐶⟩)
5	2, 3, 4	3eqtr4g 2289	1 ⊢ (𝐴 = 𝐵 → (𝐴𝐹𝐶) = (𝐵𝐹𝐶))

Syntax hints:   → wi 4   = wceq 1397  ⟨cop 3672  ‘cfv 5326  (class class class)co 6018

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 716  ax-5 1495  ax-7 1496  ax-gen 1497  ax-ie1 1541  ax-ie2 1542  ax-8 1552  ax-10 1553  ax-11 1554  ax-i12 1555  ax-bndl 1557  ax-4 1558  ax-17 1574  ax-i9 1578  ax-ial 1582  ax-i5r 1583  ax-ext 2213

This theorem depends on definitions:  df-bi 117  df-3an 1006  df-tru 1400  df-nf 1509  df-sb 1811  df-clab 2218  df-cleq 2224  df-clel 2227  df-nfc 2363  df-rex 2516  df-v 2804  df-un 3204  df-sn 3675  df-pr 3676  df-op 3678  df-uni 3894  df-br 4089  df-iota 5286  df-fv 5334  df-ov 6021

This theorem is referenced by:  oveq12  6027  oveq1i  6028  oveq1d  6033  ovrspc2v  6044  oveqrspc2v  6045  rspceov  6061  fovcld  6126  ovmpos  6145  ov2gf  6146  ovi3  6159  caovclg  6175  caovcomg  6178  caovassg  6181  caovcang  6184  caovcan  6187  caovordig  6188  caovordg  6190  caovord  6194  caovdig  6197  caovdirg  6200  caovimo  6216  suppssov1  6232  off  6248  caofid0r  6263  caofid1  6264  caofdig  6269  omcl  6629  oeicl  6630  omv2  6633  nnm0r  6647  nnacom  6652  nndi  6654  nnmass  6655  nnmsucr  6656  nnmcom  6657  nnaword  6679  nnmord  6685  nnm00  6698  eroveu  6795  th3qlem2  6807  th3q  6809  ecovcom  6811  ecovicom  6812  ecovass  6813  ecoviass  6814  ecovdi  6815  ecovidi  6816  map0g  6857  addcmpblnq  7587  addclnq  7595  mulclnq  7596  mulidnq  7609  recexnq  7610  recmulnqg  7611  ltanqg  7620  ltmnqg  7621  ltexnqq  7628  enq0ref  7653  enq0tr  7654  addcmpblnq0  7663  mulnnnq0  7670  addclnq0  7671  mulclnq0  7672  distrnq0  7679  mulcomnq0  7680  addassnq0  7682  prarloclemlo  7714  prarloclem3  7717  prarloclem5  7720  prarloclemcalc  7722  genipv  7729  genpassl  7744  genpassu  7745  addlocprlemeq  7753  distrlem4prl  7804  distrlem4pru  7805  ltexprlemdisj  7826  ltexprlemloc  7827  ltexprlemrl  7830  ltexprlemru  7832  prplnqu  7840  cauappcvgprlemm  7865  cauappcvgprlemopl  7866  cauappcvgprlemlol  7867  cauappcvgprlemdisj  7871  cauappcvgprlemloc  7872  cauappcvgprlemladdfl  7875  cauappcvgprlemladdru  7876  cauappcvgprlemladdrl  7877  cauappcvgprlem1  7879  cauappcvgprlemlim  7881  cauappcvgpr  7882  caucvgprlemm  7888  caucvgprlemopl  7889  caucvgprlemlol  7890  caucvgprlemdisj  7894  caucvgprlemloc  7895  caucvgprlemladdrl  7898  caucvgprlem1  7899  caucvgpr  7902  caucvgprprlemell  7905  caucvgprprlemml  7914  caucvgprpr  7932  mulcmpblnrlemg  7960  addclsr  7973  mulclsr  7974  0idsr  7987  1idsr  7988  00sr  7989  ltasrg  7990  recexgt0sr  7993  mulgt0sr  7998  mulextsr1  8001  prsrriota  8008  caucvgsrlemgt1  8015  caucvgsrlemoffres  8020  pitonn  8068  peano2nnnn  8073  axaddrcl  8085  axmulrcl  8087  axaddcom  8090  ax1rid  8097  ax0id  8098  axprecex  8100  axcnre  8101  axpre-ltadd  8106  axpre-mulgt0  8107  axpre-mulext  8108  rereceu  8109  peano5nnnn  8112  axcaucvglemcau  8118  axcaucvglemres  8119  mulrid  8176  cnegexlem1  8354  cnegexlem2  8355  cnegex  8357  addcan2  8360  subval  8371  addlsub  8549  apreim  8783  recexap  8833  receuap  8849  divvalap  8854  cju  9141  peano2nn  9155  nn1m1nn  9161  nn1suc  9162  nnsub  9182  fv0p1e1  9258  nnm1nn0  9443  zdiv  9568  zneo  9581  nneoor  9582  zeo  9585  peano5uzti  9588  nn0ind-raph  9597  uzind4s  9824  uzind4s2  9825  qmulz  9857  elpq  9883  cnref1o  9885  nn0ledivnn  10002  xaddnemnf  10092  xaddnepnf  10093  xaddcom  10096  xaddid1  10097  xnn0xadd0  10102  xaddass  10104  xpncan  10106  xleadd1a  10108  xltadd1  10111  xlt2add  10115  xsubge0  10116  xposdif  10117  xlesubadd  10118  xleaddadd  10122  fzsuc2  10314  fzm1  10335  fzoval  10383  exbtwnzlemstep  10508  exbtwnzlemshrink  10509  exbtwnzlemex  10510  exbtwnz  10511  rebtwn2zlemstep  10513  rebtwn2zlemshrink  10514  rebtwn2z  10515  flqlelt  10537  flqbi  10551  fldiv4p1lem1div2  10566  fldiv4lem1div2  10568  modqval  10587  modqadd1  10624  modqmuladd  10629  modqmuladdnn0  10631  modqm1p1mod0  10638  modqmul1  10640  modfzo0difsn  10658  addmodlteq  10661  frec2uzzd  10663  frec2uzsucd  10664  frec2uzrand  10668  frecuzrdgrrn  10671  frec2uzrdg  10672  frecuzrdgrcl  10673  frecuzrdgsuc  10677  frecuzrdgrclt  10678  frecuzrdgg  10679  frecuzrdgdom  10681  frecuzrdgfun  10683  frecuzrdgsuctlem  10686  frecuzrdgsuct  10687  uzsinds  10707  iseqvalcbv  10722  seq3val  10723  seqvalcd  10724  seqf  10727  seq3p1  10728  seqovcd  10730  seqp1cd  10733  seq3fveq2  10738  seqfveq2g  10740  seq3shft2  10744  seqshft2g  10745  monoord  10748  monoord2  10749  seq3split  10751  seqsplitg  10752  seq3caopr3  10754  seqcaopr3g  10755  seq3caopr2  10756  seqcaopr2g  10757  iseqf1olemqval  10763  iseqf1olemqk  10770  seqf1oglem2a  10781  seqf1oglem2  10783  seq3id2  10789  seq3homo  10790  seq3z  10791  seqhomog  10793  seqfeq4g  10794  seq3distr  10795  m1expcl2  10824  mulexp  10841  expadd  10844  expmul  10847  sq0i  10894  qsqeqor  10913  sqoddm1div8  10956  facp1  10993  faclbnd  11004  faclbnd3  11006  bcval  11012  bcn1  11021  bcval5  11026  bcpasc  11029  bccl  11030  hashfz1  11046  omgadd  11066  hashfzo  11087  hashfzp1  11089  hashxp  11091  seq3coll  11107  lsw1  11167  ccats1val2  11221  ccatw2s1p2  11227  pfxsuff1eqwrdeq  11284  swrdswrd  11290  ccats1pfxeq  11299  ccatopth  11301  wrdind  11307  wrd2ind  11308  swrdccatin2  11314  pfxccatin12lem2  11316  swrdccat3blem  11324  ccats1pfxeqbi  11327  swrdccatin2d  11329  reuccatpfxs1  11332  shftlem  11394  shftfvalg  11396  shftfibg  11398  shftfval  11399  shftfib  11401  shftfn  11402  shftf  11408  2shfti  11409  shftvalg  11414  shftval4g  11415  cjval  11423  imval  11428  cjexp  11471  cnrecnv  11488  cvg1nlemcau  11562  cvg1nlemres  11563  resqrexlemcalc3  11594  resqrexlemex  11603  rsqrmo  11605  resqrtcl  11607  rersqrtthlem  11608  sqrtsq  11622  absexp  11657  recan  11687  climshft  11882  climcn1  11886  climcn2  11887  subcn2  11889  fsumshft  12023  fisum0diag2  12026  fsumiun  12056  binomlem  12062  binom  12063  bcxmas  12068  isumsplit  12070  arisum2  12078  trireciplem  12079  trirecip  12080  geolim  12090  cvgratnnlemnexp  12103  cvgratnnlemmn  12104  clim2prod  12118  prodfrecap  12125  fprodcl2lem  12184  fprodfac  12194  fprodshft  12197  ef0lem  12239  efval  12240  efne0  12257  efexp  12261  demoivreALT  12353  dvdsval2  12369  p1modz1  12373  dvds0lem  12380  dvds1lem  12381  dvds2lem  12382  dvdsmulc  12398  divconjdvds  12428  odd2np1lem  12451  odd2np1  12452  ltoddhalfle  12472  halfleoddlt  12473  nn0o1gt2  12484  nn0o  12486  divalglemnn  12497  divalglemeunn  12500  divalglemex  12501  divalglemeuneg  12502  flodddiv4  12515  bitsinv1  12541  gcdabs1  12578  gcddiv  12608  dvdssqim  12613  rpmulgcd  12615  bezoutr1  12622  uzwodc  12626  dvdslcm  12659  lcmeq0  12661  lcmdvds  12669  divgcdcoprm0  12691  prmind2  12710  isprm5lem  12731  isprm6  12737  rpexp  12743  sqrt2irr  12752  pw2dvdslemn  12755  pw2dvdseu  12758  oddpwdclemxy  12759  nn0gcdsq  12790  phicl2  12804  phibndlem  12806  hashdvds  12811  crth  12814  phimullem  12815  eulerthlem1  12817  eulerthlemfi  12818  eulerthlemrprm  12819  eulerthlemth  12822  eulerth  12823  hashgcdlem  12828  phisum  12831  odzval  12832  modprm0  12845  nnnn0modprm0  12846  pythagtriplem1  12856  pythagtriplem6  12861  pythagtriplem7  12862  pythagtriplem12  12866  pythagtriplem14  12868  pythagtriplem18  12872  pythagtriplem19  12873  pceulem  12885  pceu  12886  pcval  12887  pczpre  12888  pcdiv  12893  pcqmul  12894  pcqcl  12897  pcexp  12900  pcaddlem  12930  pcadd  12931  pcmpt  12934  pcprod  12937  pcfac  12941  expnprm  12944  prmpwdvds  12946  pockthi  12949  1arithlem2  12955  4sqlem2  12980  4sqlem3  12981  4sqlem11  12992  4sqlem12  12993  4sqlem13m  12994  4sqlem17  12998  4sqlem18  12999  4sqlem19  13000  ennnfonelemr  13062  ctinfom  13067  infpn2  13095  ercpbl  13432  mgm1  13471  mgmidmo  13473  ismgmid  13478  mgmlrid  13480  ismgmid2  13481  lidrideqd  13482  lidrididd  13483  mgmidsssn0  13485  grprida  13488  gsumfzval  13492  gsumress  13496  gsumval2  13498  isnsgrp  13507  sgrpass  13509  sgrp1  13512  sgrpidmndm  13521  ismndd  13538  mndinvmod  13546  imasmnd2  13553  mnd1  13556  mnd1id  13557  mhmpropd  13567  insubm  13586  mhmima  13592  gsumvallem2  13594  grppropd  13618  isgrpd2  13622  isgrpd  13624  dfgrp2  13628  grprcan  13638  grpinveu  13639  grpsubval  13647  grplinv  13651  grpinvid2  13654  isgrpinv  13655  grplrinv  13658  grpidinv2  13659  grpidinv  13660  grpidssd  13677  grpinvssd  13678  dfgrp3mlem  13699  dfgrp3m  13700  grplactfval  13702  grp1  13707  imasgrp2  13715  mhmmnd  13721  ghmgrp  13723  mulgnn0gsum  13733  mulgnn0p1  13738  mulgnn0subcl  13740  mulgaddcom  13751  mulginvcom  13752  mulgnn0z  13754  mulgneg2  13761  mulgnnass  13762  mulgnn0ass  13763  mhmmulg  13768  issubg  13778  subgex  13781  issubg2m  13794  issubg4m  13798  isnsg2  13808  nsgbi  13809  isnsg3  13812  elnmz  13813  nmzbi  13814  ghmrn  13862  ghmnsgima  13873  gsumfzconst  13946  rngdi  13972  rngdir  13973  srgrz  14016  srgmulgass  14021  srgpcomp  14022  srgrmhm  14026  ringid  14058  ringinvnzdiv  14082  mulgass2  14090  ring1  14091  ringrghm  14094  imasring  14096  dvdsrmuld  14129  dvdsrmul1  14135  dvdsr01  14137  dvreq1  14175  rhmdvdsr  14208  lringuplu  14229  issubrng  14232  issubrng2  14243  issubrg  14254  issubrg2  14274  isrrg  14296  domneq0  14305  lmodlema  14325  islmodd  14326  lmodvsmmulgdi  14356  rmodislmodlem  14383  rmodislmod  14384  lssclg  14397  lss1d  14416  lspsn  14449  sraval  14470  rnglidlmcl  14513  quscrng  14566  cnfldmulg  14609  cnfldexp  14610  gsumfzfsumlemm  14620  cnfldui  14622  expghmap  14640  mulgghm2  14641  mulgrhm  14642  zrhmulg  14653  zlmval  14660  znunit  14692  cnmptcom  15041  psmettri2  15071  isxmet2d  15091  xmeteq0  15102  xmettri2  15104  metrest  15249  mpomulcn  15309  expcn  15312  cncfval  15315  mulc1cncf  15332  addccncf  15343  mulcncf  15351  expcncf  15352  hovera  15390  hoverb  15391  hoverlt1  15392  hovergt0  15393  ivthdich  15396  limccnp2lem  15419  dvcnp2cntop  15442  dvcoapbr  15450  dvexp  15454  dvrecap  15456  dvef  15470  plyadd  15494  plymul  15495  plycoeid3  15500  plyco  15502  plycjlemc  15503  plycj  15504  plyrecj  15506  dvply1  15508  dvply2g  15509  sincn  15512  coscn  15513  ptolemy  15567  sincosq1eq  15582  rpcxpmul2  15656  logbgcd1irr  15710  logbgcd1irraplemexp  15711  2irrexpq  15719  2irrexpqap  15721  mpodvdsmulf1o  15733  fsumdvdsmul  15734  sgmppw  15735  sgmmul  15739  perfect  15744  lgslem4  15751  lgsval  15752  lgsfvalg  15753  lgsval2lem  15758  lgsdir2lem4  15779  lgsdir  15783  lgsdilem2  15784  lgsdi  15785  lgsne0  15786  lgsmodeq  15793  lgsdirnn0  15795  lgsdinn0  15796  gausslemma2dlem0i  15805  gausslemma2dlem1a  15806  gausslemma2dlem1f1o  15808  gausslemma2dlem2  15810  gausslemma2dlem3  15811  gausslemma2dlem4  15812  lgseisenlem2  15819  lgsquadlem2  15826  lgsquadlem3  15827  lgsquad  15828  lgsquad2lem2  15830  2lgslem1a  15836  2lgslem1b  15837  2lgslem1c  15838  2lgslem3a  15841  2lgslem3b  15842  2lgslem3c  15843  2lgslem3d  15844  2lgslem3a1  15845  2lgslem3b1  15846  2lgslem3c1  15847  2lgslem3d1  15848  2lgs  15852  2lgsoddprmlem1  15853  2lgsoddprmlem3  15859  2sqlem2  15863  2sqlem6  15868  2sqlem8  15871  2sqlem9  15872  wlklenvm1  16211  wlklenvm1g  16212  wlkl1loop  16228  2wlklem  16246  clwwlknnn  16282  clwwlknp  16287  clwwlkn1  16288  clwwlkn2  16291  clwwlkext2edg  16292  umgr2cwwk2dif  16294  clwwlknon  16299  clwwlk0on0  16301  clwwlknonex2lem1  16307  clwwlknonex2lem2  16308  clwwlknonex2  16309  qdencn  16682  isomninn  16686  trirec0  16699  iswomninn  16706  ismkvnn  16709  gfsumval  16732  gsumgfsumlem  16735