Theorem oveq1 6095

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 3904	. . 3 ⊢ (𝐴 = 𝐵 → ⟨𝐴, 𝐶⟩ = ⟨𝐵, 𝐶⟩)
2	1	fveq2d 5702	. 2 ⊢ (𝐴 = 𝐵 → (𝐹‘⟨𝐴, 𝐶⟩) = (𝐹‘⟨𝐵, 𝐶⟩))
3		df-ov 6091	. 2 ⊢ (𝐴𝐹𝐶) = (𝐹‘⟨𝐴, 𝐶⟩)
4		df-ov 6091	. 2 ⊢ (𝐵𝐹𝐶) = (𝐹‘⟨𝐵, 𝐶⟩)
5	2, 3, 4	3eqtr4g 2296	1 ⊢ (𝐴 = 𝐵 → (𝐴𝐹𝐶) = (𝐵𝐹𝐶))

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  6739  oeicl  6740  omv2  6743  nnm0r  6757  nnacom  6762  nndi  6764  nnmass  6765  nnmsucr  6766  nnmcom  6767  nnaword  6789  nnmord  6795  nnm00  6808  eroveu  6905  th3qlem2  6917  th3q  6919  ecovcom  6921  ecovicom  6922  ecovass  6923  ecoviass  6924  ecovdi  6925  ecovidi  6926  map0g  6974  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  9744  zneo  9757  nneoor  9758  zeo  9761  peano5uzti  9764  nn0ind-raph  9773  uzind4s  10005  uzind4s2  10006  qmulz  10038  elpq  10065  cnref1o  10067  nn0ledivnn  10184  xaddnemnf  10275  xaddnepnf  10276  xaddcom  10279  xaddid1  10280  xnn0xadd0  10285  xaddass  10287  xpncan  10289  xleadd1a  10291  xltadd1  10294  xlt2add  10298  xsubge0  10299  xposdif  10300  xlesubadd  10301  xleaddadd  10305  fzsuc2  10502  fzm1  10523  fzoval  10571  exbtwnzlemstep  10698  exbtwnzlemshrink  10699  exbtwnzlemex  10700  exbtwnz  10701  rebtwn2zlemstep  10703  rebtwn2zlemshrink  10704  rebtwn2z  10705  flqlelt  10728  flaplelt  10729  flqbi  10745  fldiv4p1lem1div2  10760  fldiv4lem1div2  10762  modqval  10781  modqadd1  10818  modqmuladd  10823  modqmuladdnn0  10825  modqm1p1mod0  10832  modqmul1  10834  modfzo0difsn  10852  addmodlteq  10855  frec2uzzd  10857  frec2uzsucd  10858  frec2uzrand  10862  frecuzrdgrrn  10865  frec2uzrdg  10866  frecuzrdgrcl  10867  frecuzrdgsuc  10871  frecuzrdgrclt  10872  frecuzrdgg  10873  frecuzrdgdom  10875  frecuzrdgfun  10877  frecuzrdgsuctlem  10880  frecuzrdgsuct  10881  uzsinds  10901  iseqvalcbv  10916  seq3val  10917  seqvalcd  10918  seqf  10921  seq3p1  10922  seqovcd  10924  seqp1cd  10927  seq3fveq2  10932  seqfveq2g  10934  seq3shft2  10938  seqshft2g  10939  monoord  10942  monoord2  10943  seq3split  10945  seqsplitg  10946  seq3caopr3  10948  seqcaopr3g  10949  seq3caopr2  10950  seqcaopr2g  10951  iseqf1olemqval  10957  iseqf1olemqk  10964  seqf1oglem2a  10975  seqf1oglem2  10977  seq3id2  10983  seq3homo  10984  seq3z  10985  seqhomog  10987  seqfeq4g  10988  seq3distr  10989  m1expcl2  11018  mulexp  11035  expadd  11038  expmul  11041  sq0i  11088  qsqeqor  11107  resq01  11115  sqoddm1div8  11151  facp1  11189  faclbnd  11200  faclbnd3  11202  bcval  11208  bcn1  11217  bcval5  11222  bcpasc  11225  bccl  11226  hashfz1  11243  omgadd  11263  hashfzo  11284  hashfzp1  11286  hashxp  11288  hashmap  11289  hashf1lem2  11307  seq3coll  11315  lsw1  11375  ccats1val2  11429  ccatw2s1p2  11435  pfxsuff1eqwrdeq  11492  swrdswrd  11498  ccats1pfxeq  11507  ccatopth  11509  wrdind  11515  wrd2ind  11516  swrdccatin2  11522  pfxccatin12lem2  11524  swrdccat3blem  11532  ccats1pfxeqbi  11535  swrdccatin2d  11537  reuccatpfxs1  11540  shftlem  11602  shftfvalg  11604  shftfibg  11606  shftfval  11607  shftfib  11609  shftfn  11610  shftf  11616  2shfti  11617  shftvalg  11622  shftval4g  11623  cjval  11631  imval  11636  cjexp  11679  sq01  11681  cnrecnv  11697  cvg1nlemcau  11771  cvg1nlemres  11772  resqrexlemcalc3  11803  resqrexlemex  11812  rsqrmo  11814  resqrtcl  11816  rersqrtthlem  11817  sqrtsq  11831  absexp  11867  recan  11897  climshft  12094  climcn1  12098  climcn2  12099  subcn2  12101  fsumshft  12235  fisum0diag2  12238  fsumiun  12268  binomlem  12274  binom  12275  bcxmas  12280  isumsplit  12282  arisum2  12290  trireciplem  12291  trirecip  12292  geolim  12302  cvgratnnlemnexp  12315  cvgratnnlemmn  12316  clim2prod  12330  prodfrecap  12337  fprodcl2lem  12396  fprodfac  12406  fprodshft  12409  ef0lem  12451  efval  12452  efne0  12469  efexp  12473  demoivreALT  12565  dvdsval2  12581  p1modz1  12585  dvds0lem  12592  dvds1lem  12593  dvds2lem  12594  dvdsmulc  12610  divconjdvds  12640  odd2np1lem  12663  odd2np1  12664  ltoddhalfle  12684  halfleoddlt  12685  nn0o1gt2  12696  nn0o  12698  divalglemnn  12709  divalglemeunn  12712  divalglemex  12713  divalglemeuneg  12714  flodddiv4  12727  bitsinv1  12753  gcdabs1  12790  gcddiv  12820  dvdssqim  12825  rpmulgcd  12827  bezoutr1  12834  uzwodc  12838  dvdslcm  12871  lcmeq0  12873  lcmdvds  12881  divgcdcoprm0  12903  prmind2  12922  isprm5lem  12944  isprm6  12950  rpexp  12956  sqrt2irr  12965  pwbdvdslemn  12968  pwbdvdseu  12971  nnmaxpwlemxy  12972  nn0gcdsq  13004  nn0sqdcq  13012  phicl2  13020  phibndlem  13022  hashdvds  13027  crth  13030  phimullem  13031  eulerthlem1  13033  eulerthlemfi  13034  eulerthlemrprm  13035  eulerthlemth  13038  eulerth  13039  hashgcdlem  13044  phisum  13047  odzval  13048  modprm0  13061  nnnn0modprm0  13062  pythagtriplem1  13072  pythagtriplem6  13077  pythagtriplem7  13078  pythagtriplem12  13082  pythagtriplem14  13084  pythagtriplem18  13088  pythagtriplem19  13089  pceulem  13101  pceu  13102  pcval  13103  pczpre  13104  pcdiv  13109  pcqmul  13110  pcqcl  13113  pcexp  13116  pcaddlem  13146  pcadd  13147  pcmpt  13150  pcprod  13153  pcfac  13157  expnprm  13160  prmpwdvds  13162  pockthi  13165  1arithlem2  13171  4sqlem2  13196  4sqlem3  13197  4sqlem11  13208  4sqlem12  13209  4sqlem13m  13210  4sqlem17  13214  4sqlem18  13215  4sqlem19  13216  ballotfilemfc0  13289  ballotfilemfcc  13290  ennnfonelemr  13371  ctinfom  13376  infpn2  13404  ercpbl  13710  mgm1  13748  mgmidmo  13750  ismgmid  13755  mgmlrid  13757  ismgmid2  13758  lidrideqd  13759  lidrididd  13760  mgmidsssn0  13762  grprida  13765  gzsumfzval  13769  gzsumress  13770  gzsumval2  13772  isnsgrp  13779  sgrpass  13781  sgrp1  13784  sgrpidmndm  13791  ismndd  13808  mndinvmod  13816  imasmnd2  13817  mnd1  13820  mnd1id  13821  mhmpropd  13831  insubm  13850  mhmima  13856  gsumvallem2  13858  grppropd  13880  isgrpd2  13884  isgrpd  13886  dfgrp2  13890  grprcan  13900  grpinveu  13901  grpsubval  13909  grplinv  13913  grpinvid2  13916  isgrpinv  13917  grplrinv  13920  grpidinv2  13921  grpidinv  13922  grpidssd  13939  grpinvssd  13940  dfgrp3mlem  13961  dfgrp3m  13962  grplactfval  13964  grp1  13969  imasgrp2  13971  mhmmnd  13977  ghmgrp  13979  mulgnn0gzsum  13989  mulgnn0p1  13994  mulgnn0subcl  13996  mulgaddcom  14007  mulginvcom  14008  mulgnn0z  14010  mulgneg2  14017  mulgnnass  14018  mulgnn0ass  14019  mhmmulg  14024  issubg  14034  subgex  14037  issubg2m  14050  issubg4m  14054  isnsg2  14064  nsgbi  14065  isnsg3  14068  elnmz  14069  nmzbi  14070  ghmrn  14118  ghmnsgima  14129  elcntz  14153  cntzsnval  14155  elcntzsn  14156  cntzi  14161  cntzmhm  14172  gzsumconst  14232  gzsumshift  14238  gsumvalfi  14241  gsum2dfilem2  14271  gsum2dfi  14272  gsum2d2fi  14273  gsumcom2fi  14274  rngdi  14345  rngdir  14346  srgrz  14394  srgmulgass  14399  srgpcomp  14400  srgrmhm  14404  ringid  14437  ringinvnzdiv  14461  mulgass2  14469  ring1  14470  ringrghm  14473  gsummulc1fi  14474  imasring  14477  dvdsrmuld  14511  dvdsrmul1  14517  dvdsr01  14519  dvreq1  14557  rhmdvdsr  14590  lringuplu  14611  issubrng  14615  issubrng2  14626  issubrg  14637  issubrg2  14657  isrrg  14679  domneq0  14689  lmodlema  14736  islmodd  14737  lmodvsmmulgdi  14768  rmodislmodlem  14795  rmodislmod  14796  lssclg  14809  lss1d  14828  lspsn  14861  sraval  14882  rnglidlmcl  14925  quscrng  14978  cnfldmulg  15021  cnfldexp  15022  gsumfsum  15031  cnfldui  15032  expghmap  15050  mulgghm2  15051  mulgrhm  15052  zrhmulg  15063  zlmval  15070  znunit  15102  assalem  15111  asclvald  15130  assamulgscmlem2  15150  assamulgscm  15151  psrass1filem  15186  cnmptcom  15541  psmettri2  15571  isxmet2d  15591  xmeteq0  15602  xmettri2  15604  metrest  15749  mpomulcn  15809  expcn  15812  cncfval  15815  mulc1cncf  15832  addccncf  15843  mulcncf  15851  expcncf  15852  hovera  15890  hoverb  15891  hoverlt1  15892  hovergt0  15893  ivthdich  15896  limccnp2lem  15919  dvcnp2cntop  15942  dvcoapbr  15950  dvexp  15954  dvrecap  15956  dvef  15970  plyadd  15994  plymul  15995  plycoeid3  16000  plyco  16002  plycjlemc  16003  plycj  16004  plyrecj  16006  dvply1  16008  dvply2g  16009  sincn  16012  coscn  16013  ptolemy  16068  sincosq1eq  16083  rpcxpmul2  16163  efnthr  16193  logbgcd1irr  16220  logbgcd1irraplemexp  16221  2irrexpq  16229  2irrexpqap  16231  pellexlem3  16248  mpodvdsmulf1o  16301  fsumdvdsmul  16302  sgmppw  16303  sgmmul  16307  ppiqub  16310  perfect  16318  bposlem3  16330  bposlem5  16332  bposlem6  16333  bposlem8  16335  lgslem4  16344  lgsval  16345  lgsfvalg  16346  lgsval2lem  16351  lgsdir2lem4  16372  lgsdir  16376  lgsdilem2  16377  lgsdi  16378  lgsne0  16379  lgsmodeq  16386  lgsdirnn0  16388  lgsdinn0  16389  gausslemma2dlem0i  16398  gausslemma2dlem1a  16399  gausslemma2dlem1f1o  16401  gausslemma2dlem2  16403  gausslemma2dlem3  16404  gausslemma2dlem4  16405  lgseisenlem2  16412  lgsquadlem2  16419  lgsquadlem3  16420  lgsquad  16421  lgsquad2lem2  16423  2lgslem1a  16429  2lgslem1b  16430  2lgslem1c  16431  2lgslem3a  16434  2lgslem3b  16435  2lgslem3c  16436  2lgslem3d  16437  2lgslem3a1  16438  2lgslem3b1  16439  2lgslem3c1  16440  2lgslem3d1  16441  2lgs  16445  2lgsoddprmlem1  16446  2lgsoddprmlem3  16452  2sqlem2  16456  2sqlem6  16461  2sqlem8  16464  2sqlem9  16465  wlklenvm1  16804  wlklenvm1g  16805  wlkl1loop  16821  2wlklem  16839  clwwlknnn  16875  clwwlknp  16880  clwwlkn1  16881  clwwlkn2  16884  clwwlkext2edg  16885  umgr2cwwk2dif  16887  clwwlknon  16892  clwwlk0on0  16894  clwwlknonex2lem1  16900  clwwlknonex2lem2  16901  clwwlknonex2  16902  qdencn  17295  isomninn  17303  trirec0  17317  iswomninn  17324  ismkvnn  17327