Theorem oveq1 5932

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 3809	. . 3 ⊢ (𝐴 = 𝐵 → ⟨𝐴, 𝐶⟩ = ⟨𝐵, 𝐶⟩)
2	1	fveq2d 5565	. 2 ⊢ (𝐴 = 𝐵 → (𝐹‘⟨𝐴, 𝐶⟩) = (𝐹‘⟨𝐵, 𝐶⟩))
3		df-ov 5928	. 2 ⊢ (𝐴𝐹𝐶) = (𝐹‘⟨𝐴, 𝐶⟩)
4		df-ov 5928	. 2 ⊢ (𝐵𝐹𝐶) = (𝐹‘⟨𝐵, 𝐶⟩)
5	2, 3, 4	3eqtr4g 2254	1 ⊢ (𝐴 = 𝐵 → (𝐴𝐹𝐶) = (𝐵𝐹𝐶))

Syntax hints:   → wi 4   = wceq 1364  ⟨cop 3626  ‘cfv 5259  (class class class)co 5925

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 710  ax-5 1461  ax-7 1462  ax-gen 1463  ax-ie1 1507  ax-ie2 1508  ax-8 1518  ax-10 1519  ax-11 1520  ax-i12 1521  ax-bndl 1523  ax-4 1524  ax-17 1540  ax-i9 1544  ax-ial 1548  ax-i5r 1549  ax-ext 2178

This theorem depends on definitions:  df-bi 117  df-3an 982  df-tru 1367  df-nf 1475  df-sb 1777  df-clab 2183  df-cleq 2189  df-clel 2192  df-nfc 2328  df-rex 2481  df-v 2765  df-un 3161  df-sn 3629  df-pr 3630  df-op 3632  df-uni 3841  df-br 4035  df-iota 5220  df-fv 5267  df-ov 5928

This theorem is referenced by:  oveq12  5934  oveq1i  5935  oveq1d  5940  ovrspc2v  5951  oveqrspc2v  5952  rspceov  5968  fovcld  6031  ovmpos  6050  ov2gf  6051  ovi3  6064  caovclg  6080  caovcomg  6083  caovassg  6086  caovcang  6089  caovcan  6092  caovordig  6093  caovordg  6095  caovord  6099  caovdig  6102  caovdirg  6105  caovimo  6121  suppssov1  6136  off  6152  caofid0r  6167  caofid1  6168  caofdig  6173  omcl  6528  oeicl  6529  omv2  6532  nnm0r  6546  nnacom  6551  nndi  6553  nnmass  6554  nnmsucr  6555  nnmcom  6556  nnaword  6578  nnmord  6584  nnm00  6597  eroveu  6694  th3qlem2  6706  th3q  6708  ecovcom  6710  ecovicom  6711  ecovass  6712  ecoviass  6713  ecovdi  6714  ecovidi  6715  map0g  6756  addcmpblnq  7453  addclnq  7461  mulclnq  7462  mulidnq  7475  recexnq  7476  recmulnqg  7477  ltanqg  7486  ltmnqg  7487  ltexnqq  7494  enq0ref  7519  enq0tr  7520  addcmpblnq0  7529  mulnnnq0  7536  addclnq0  7537  mulclnq0  7538  distrnq0  7545  mulcomnq0  7546  addassnq0  7548  prarloclemlo  7580  prarloclem3  7583  prarloclem5  7586  prarloclemcalc  7588  genipv  7595  genpassl  7610  genpassu  7611  addlocprlemeq  7619  distrlem4prl  7670  distrlem4pru  7671  ltexprlemdisj  7692  ltexprlemloc  7693  ltexprlemrl  7696  ltexprlemru  7698  prplnqu  7706  cauappcvgprlemm  7731  cauappcvgprlemopl  7732  cauappcvgprlemlol  7733  cauappcvgprlemdisj  7737  cauappcvgprlemloc  7738  cauappcvgprlemladdfl  7741  cauappcvgprlemladdru  7742  cauappcvgprlemladdrl  7743  cauappcvgprlem1  7745  cauappcvgprlemlim  7747  cauappcvgpr  7748  caucvgprlemm  7754  caucvgprlemopl  7755  caucvgprlemlol  7756  caucvgprlemdisj  7760  caucvgprlemloc  7761  caucvgprlemladdrl  7764  caucvgprlem1  7765  caucvgpr  7768  caucvgprprlemell  7771  caucvgprprlemml  7780  caucvgprpr  7798  mulcmpblnrlemg  7826  addclsr  7839  mulclsr  7840  0idsr  7853  1idsr  7854  00sr  7855  ltasrg  7856  recexgt0sr  7859  mulgt0sr  7864  mulextsr1  7867  prsrriota  7874  caucvgsrlemgt1  7881  caucvgsrlemoffres  7886  pitonn  7934  peano2nnnn  7939  axaddrcl  7951  axmulrcl  7953  axaddcom  7956  ax1rid  7963  ax0id  7964  axprecex  7966  axcnre  7967  axpre-ltadd  7972  axpre-mulgt0  7973  axpre-mulext  7974  rereceu  7975  peano5nnnn  7978  axcaucvglemcau  7984  axcaucvglemres  7985  mulrid  8042  cnegexlem1  8220  cnegexlem2  8221  cnegex  8223  addcan2  8226  subval  8237  addlsub  8415  apreim  8649  recexap  8699  receuap  8715  divvalap  8720  cju  9007  peano2nn  9021  nn1m1nn  9027  nn1suc  9028  nnsub  9048  fv0p1e1  9124  nnm1nn0  9309  zdiv  9433  zneo  9446  nneoor  9447  zeo  9450  peano5uzti  9453  nn0ind-raph  9462  uzind4s  9683  uzind4s2  9684  qmulz  9716  elpq  9742  cnref1o  9744  nn0ledivnn  9861  xaddnemnf  9951  xaddnepnf  9952  xaddcom  9955  xaddid1  9956  xnn0xadd0  9961  xaddass  9963  xpncan  9965  xleadd1a  9967  xltadd1  9970  xlt2add  9974  xsubge0  9975  xposdif  9976  xlesubadd  9977  xleaddadd  9981  fzsuc2  10173  fzm1  10194  fzoval  10242  exbtwnzlemstep  10356  exbtwnzlemshrink  10357  exbtwnzlemex  10358  exbtwnz  10359  rebtwn2zlemstep  10361  rebtwn2zlemshrink  10362  rebtwn2z  10363  flqlelt  10385  flqbi  10399  fldiv4p1lem1div2  10414  fldiv4lem1div2  10416  modqval  10435  modqadd1  10472  modqmuladd  10477  modqmuladdnn0  10479  modqm1p1mod0  10486  modqmul1  10488  modfzo0difsn  10506  addmodlteq  10509  frec2uzzd  10511  frec2uzsucd  10512  frec2uzrand  10516  frecuzrdgrrn  10519  frec2uzrdg  10520  frecuzrdgrcl  10521  frecuzrdgsuc  10525  frecuzrdgrclt  10526  frecuzrdgg  10527  frecuzrdgdom  10529  frecuzrdgfun  10531  frecuzrdgsuctlem  10534  frecuzrdgsuct  10535  uzsinds  10555  iseqvalcbv  10570  seq3val  10571  seqvalcd  10572  seqf  10575  seq3p1  10576  seqovcd  10578  seqp1cd  10581  seq3fveq2  10586  seqfveq2g  10588  seq3shft2  10592  seqshft2g  10593  monoord  10596  monoord2  10597  seq3split  10599  seqsplitg  10600  seq3caopr3  10602  seqcaopr3g  10603  seq3caopr2  10604  seqcaopr2g  10605  iseqf1olemqval  10611  iseqf1olemqk  10618  seqf1oglem2a  10629  seqf1oglem2  10631  seq3id2  10637  seq3homo  10638  seq3z  10639  seqhomog  10641  seqfeq4g  10642  seq3distr  10643  m1expcl2  10672  mulexp  10689  expadd  10692  expmul  10695  sq0i  10742  qsqeqor  10761  sqoddm1div8  10804  facp1  10841  faclbnd  10852  faclbnd3  10854  bcval  10860  bcn1  10869  bcval5  10874  bcpasc  10877  bccl  10878  hashfz1  10894  omgadd  10913  hashfzo  10933  hashfzp1  10935  hashxp  10937  seq3coll  10953  shftlem  11000  shftfvalg  11002  shftfibg  11004  shftfval  11005  shftfib  11007  shftfn  11008  shftf  11014  2shfti  11015  shftvalg  11020  shftval4g  11021  cjval  11029  imval  11034  cjexp  11077  cnrecnv  11094  cvg1nlemcau  11168  cvg1nlemres  11169  resqrexlemcalc3  11200  resqrexlemex  11209  rsqrmo  11211  resqrtcl  11213  rersqrtthlem  11214  sqrtsq  11228  absexp  11263  recan  11293  climshft  11488  climcn1  11492  climcn2  11493  subcn2  11495  fsumshft  11628  fisum0diag2  11631  fsumiun  11661  binomlem  11667  binom  11668  bcxmas  11673  isumsplit  11675  arisum2  11683  trireciplem  11684  trirecip  11685  geolim  11695  cvgratnnlemnexp  11708  cvgratnnlemmn  11709  clim2prod  11723  prodfrecap  11730  fprodcl2lem  11789  fprodfac  11799  fprodshft  11802  ef0lem  11844  efval  11845  efne0  11862  efexp  11866  demoivreALT  11958  dvdsval2  11974  p1modz1  11978  dvds0lem  11985  dvds1lem  11986  dvds2lem  11987  dvdsmulc  12003  divconjdvds  12033  odd2np1lem  12056  odd2np1  12057  ltoddhalfle  12077  halfleoddlt  12078  nn0o1gt2  12089  nn0o  12091  divalglemnn  12102  divalglemeunn  12105  divalglemex  12106  divalglemeuneg  12107  flodddiv4  12120  bitsinv1  12146  gcdabs1  12183  gcddiv  12213  dvdssqim  12218  rpmulgcd  12220  bezoutr1  12227  uzwodc  12231  dvdslcm  12264  lcmeq0  12266  lcmdvds  12274  divgcdcoprm0  12296  prmind2  12315  isprm5lem  12336  isprm6  12342  rpexp  12348  sqrt2irr  12357  pw2dvdslemn  12360  pw2dvdseu  12363  oddpwdclemxy  12364  nn0gcdsq  12395  phicl2  12409  phibndlem  12411  hashdvds  12416  crth  12419  phimullem  12420  eulerthlem1  12422  eulerthlemfi  12423  eulerthlemrprm  12424  eulerthlemth  12427  eulerth  12428  hashgcdlem  12433  phisum  12436  odzval  12437  modprm0  12450  nnnn0modprm0  12451  pythagtriplem1  12461  pythagtriplem6  12466  pythagtriplem7  12467  pythagtriplem12  12471  pythagtriplem14  12473  pythagtriplem18  12477  pythagtriplem19  12478  pceulem  12490  pceu  12491  pcval  12492  pczpre  12493  pcdiv  12498  pcqmul  12499  pcqcl  12502  pcexp  12505  pcaddlem  12535  pcadd  12536  pcmpt  12539  pcprod  12542  pcfac  12546  expnprm  12549  prmpwdvds  12551  pockthi  12554  1arithlem2  12560  4sqlem2  12585  4sqlem3  12586  4sqlem11  12597  4sqlem12  12598  4sqlem13m  12599  4sqlem17  12603  4sqlem18  12604  4sqlem19  12605  ennnfonelemr  12667  ctinfom  12672  infpn2  12700  ercpbl  13035  mgm1  13074  mgmidmo  13076  ismgmid  13081  mgmlrid  13083  ismgmid2  13084  lidrideqd  13085  lidrididd  13086  mgmidsssn0  13088  grprida  13091  gsumfzval  13095  gsumress  13099  gsumval2  13101  isnsgrp  13110  sgrpass  13112  sgrp1  13115  sgrpidmndm  13124  ismndd  13141  mndinvmod  13149  imasmnd2  13156  mnd1  13159  mnd1id  13160  mhmpropd  13170  insubm  13189  mhmima  13195  gsumvallem2  13197  grppropd  13221  isgrpd2  13225  isgrpd  13227  dfgrp2  13231  grprcan  13241  grpinveu  13242  grpsubval  13250  grplinv  13254  grpinvid2  13257  isgrpinv  13258  grplrinv  13261  grpidinv2  13262  grpidinv  13263  grpidssd  13280  grpinvssd  13281  dfgrp3mlem  13302  dfgrp3m  13303  grplactfval  13305  grp1  13310  imasgrp2  13318  mhmmnd  13324  ghmgrp  13326  mulgnn0gsum  13336  mulgnn0p1  13341  mulgnn0subcl  13343  mulgaddcom  13354  mulginvcom  13355  mulgnn0z  13357  mulgneg2  13364  mulgnnass  13365  mulgnn0ass  13366  mhmmulg  13371  issubg  13381  subgex  13384  issubg2m  13397  issubg4m  13401  isnsg2  13411  nsgbi  13412  isnsg3  13415  elnmz  13416  nmzbi  13417  ghmrn  13465  ghmnsgima  13476  gsumfzconst  13549  rngdi  13574  rngdir  13575  srgrz  13618  srgmulgass  13623  srgpcomp  13624  srgrmhm  13628  ringid  13660  ringinvnzdiv  13684  mulgass2  13692  ring1  13693  ringrghm  13696  imasring  13698  dvdsrmuld  13730  dvdsrmul1  13736  dvdsr01  13738  dvreq1  13776  rhmdvdsr  13809  lringuplu  13830  issubrng  13833  issubrng2  13844  issubrg  13855  issubrg2  13875  isrrg  13897  domneq0  13906  lmodlema  13926  islmodd  13927  lmodvsmmulgdi  13957  rmodislmodlem  13984  rmodislmod  13985  lssclg  13998  lss1d  14017  lspsn  14050  sraval  14071  rnglidlmcl  14114  quscrng  14167  cnfldmulg  14210  cnfldexp  14211  gsumfzfsumlemm  14221  cnfldui  14223  expghmap  14241  mulgghm2  14242  mulgrhm  14243  zrhmulg  14254  zlmval  14261  znunit  14293  cnmptcom  14642  psmettri2  14672  isxmet2d  14692  xmeteq0  14703  xmettri2  14705  metrest  14850  mpomulcn  14910  expcn  14913  cncfval  14916  mulc1cncf  14933  addccncf  14944  mulcncf  14952  expcncf  14953  hovera  14991  hoverb  14992  hoverlt1  14993  hovergt0  14994  ivthdich  14997  limccnp2lem  15020  dvcnp2cntop  15043  dvcoapbr  15051  dvexp  15055  dvrecap  15057  dvef  15071  plyadd  15095  plymul  15096  plycoeid3  15101  plyco  15103  plycjlemc  15104  plycj  15105  plyrecj  15107  dvply1  15109  dvply2g  15110  sincn  15113  coscn  15114  ptolemy  15168  sincosq1eq  15183  rpcxpmul2  15257  logbgcd1irr  15311  logbgcd1irraplemexp  15312  2irrexpq  15320  2irrexpqap  15322  mpodvdsmulf1o  15334  fsumdvdsmul  15335  sgmppw  15336  sgmmul  15340  perfect  15345  lgslem4  15352  lgsval  15353  lgsfvalg  15354  lgsval2lem  15359  lgsdir2lem4  15380  lgsdir  15384  lgsdilem2  15385  lgsdi  15386  lgsne0  15387  lgsmodeq  15394  lgsdirnn0  15396  lgsdinn0  15397  gausslemma2dlem0i  15406  gausslemma2dlem1a  15407  gausslemma2dlem1f1o  15409  gausslemma2dlem2  15411  gausslemma2dlem3  15412  gausslemma2dlem4  15413  lgseisenlem2  15420  lgsquadlem2  15427  lgsquadlem3  15428  lgsquad  15429  lgsquad2lem2  15431  2lgslem1a  15437  2lgslem1b  15438  2lgslem1c  15439  2lgslem3a  15442  2lgslem3b  15443  2lgslem3c  15444  2lgslem3d  15445  2lgslem3a1  15446  2lgslem3b1  15447  2lgslem3c1  15448  2lgslem3d1  15449  2lgs  15453  2lgsoddprmlem1  15454  2lgsoddprmlem3  15460  2sqlem2  15464  2sqlem6  15469  2sqlem8  15472  2sqlem9  15473  qdencn  15784  isomninn  15788  trirec0  15801  iswomninn  15807  ismkvnn  15810