Theorem oveq1 6065

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 3888	. . 3 ⊢ (𝐴 = 𝐵 → ⟨𝐴, 𝐶⟩ = ⟨𝐵, 𝐶⟩)
2	1	fveq2d 5679	. 2 ⊢ (𝐴 = 𝐵 → (𝐹‘⟨𝐴, 𝐶⟩) = (𝐹‘⟨𝐵, 𝐶⟩))
3		df-ov 6061	. 2 ⊢ (𝐴𝐹𝐶) = (𝐹‘⟨𝐴, 𝐶⟩)
4		df-ov 6061	. 2 ⊢ (𝐵𝐹𝐶) = (𝐹‘⟨𝐵, 𝐶⟩)
5	2, 3, 4	3eqtr4g 2292	1 ⊢ (𝐴 = 𝐵 → (𝐴𝐹𝐶) = (𝐵𝐹𝐶))

Syntax hints:   → wi 4   = wceq 1398  ⟨cop 3697  ‘cfv 5357  (class class class)co 6058

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 717  ax-5 1496  ax-7 1497  ax-gen 1498  ax-ie1 1542  ax-ie2 1543  ax-8 1553  ax-10 1554  ax-11 1555  ax-i12 1556  ax-bndl 1558  ax-4 1559  ax-17 1575  ax-i9 1579  ax-ial 1583  ax-i5r 1584  ax-ext 2216

This theorem depends on definitions:  df-bi 117  df-3an 1007  df-tru 1401  df-nf 1510  df-sb 1812  df-clab 2221  df-cleq 2227  df-clel 2230  df-nfc 2375  df-rex 2528  df-v 2817  df-un 3218  df-sn 3700  df-pr 3701  df-op 3703  df-uni 3920  df-br 4115  df-iota 5317  df-fv 5365  df-ov 6061

This theorem is referenced by:  oveq12  6067  oveq1i  6068  oveq1d  6073  ovrspc2v  6084  oveqrspc2v  6085  rspceov  6101  fovcld  6166  ovmpos  6185  ov2gf  6186  ovi3  6199  caovclg  6215  caovcomg  6218  caovassg  6221  caovcang  6224  caovcan  6227  caovordig  6228  caovordg  6230  caovord  6234  caovdig  6237  caovdirg  6240  caovimo  6256  suppssov1  6272  off  6288  caofid0r  6303  caofid1  6304  caofdig  6309  suppofss1dcl  6477  suppofss2dcl  6478  omcl  6707  oeicl  6708  omv2  6711  nnm0r  6725  nnacom  6730  nndi  6732  nnmass  6733  nnmsucr  6734  nnmcom  6735  nnaword  6757  nnmord  6763  nnm00  6776  eroveu  6873  th3qlem2  6885  th3q  6887  ecovcom  6889  ecovicom  6890  ecovass  6891  ecoviass  6892  ecovdi  6893  ecovidi  6894  map0g  6935  addcmpblnq  7698  addclnq  7706  mulclnq  7707  mulidnq  7720  recexnq  7721  recmulnqg  7722  ltanqg  7731  ltmnqg  7732  ltexnqq  7739  enq0ref  7764  enq0tr  7765  addcmpblnq0  7774  mulnnnq0  7781  addclnq0  7782  mulclnq0  7783  distrnq0  7790  mulcomnq0  7791  addassnq0  7793  prarloclemlo  7825  prarloclem3  7828  prarloclem5  7831  prarloclemcalc  7833  genipv  7840  genpassl  7855  genpassu  7856  addlocprlemeq  7864  distrlem4prl  7915  distrlem4pru  7916  ltexprlemdisj  7937  ltexprlemloc  7938  ltexprlemrl  7941  ltexprlemru  7943  prplnqu  7951  cauappcvgprlemm  7976  cauappcvgprlemopl  7977  cauappcvgprlemlol  7978  cauappcvgprlemdisj  7982  cauappcvgprlemloc  7983  cauappcvgprlemladdfl  7986  cauappcvgprlemladdru  7987  cauappcvgprlemladdrl  7988  cauappcvgprlem1  7990  cauappcvgprlemlim  7992  cauappcvgpr  7993  caucvgprlemm  7999  caucvgprlemopl  8000  caucvgprlemlol  8001  caucvgprlemdisj  8005  caucvgprlemloc  8006  caucvgprlemladdrl  8009  caucvgprlem1  8010  caucvgpr  8013  caucvgprprlemell  8016  caucvgprprlemml  8025  caucvgprpr  8043  mulcmpblnrlemg  8071  addclsr  8084  mulclsr  8085  0idsr  8098  1idsr  8099  00sr  8100  ltasrg  8101  recexgt0sr  8104  mulgt0sr  8109  mulextsr1  8112  prsrriota  8119  caucvgsrlemgt1  8126  caucvgsrlemoffres  8131  pitonn  8179  peano2nnnn  8184  axaddrcl  8196  axmulrcl  8198  axaddcom  8201  ax1rid  8208  ax0id  8209  axprecex  8211  axcnre  8212  axpre-ltadd  8217  axpre-mulgt0  8218  axpre-mulext  8219  rereceu  8220  peano5nnnn  8223  axcaucvglemcau  8229  axcaucvglemres  8230  mulrid  8287  cnegexlem1  8464  cnegexlem2  8465  cnegex  8467  addcan2  8470  subval  8481  addlsub  8659  apreim  8894  recexap  8944  receuap  8960  divvalap  8965  cju  9252  peano2nn  9266  nn1m1nn  9272  nn1suc  9273  nnsub  9293  fv0p1e1  9369  nnm1nn0  9554  zdiv  9684  zneo  9697  nneoor  9698  zeo  9701  peano5uzti  9704  nn0ind-raph  9713  uzind4s  9940  uzind4s2  9941  qmulz  9973  elpq  9999  cnref1o  10001  nn0ledivnn  10118  xaddnemnf  10209  xaddnepnf  10210  xaddcom  10213  xaddid1  10214  xnn0xadd0  10219  xaddass  10221  xpncan  10223  xleadd1a  10225  xltadd1  10228  xlt2add  10232  xsubge0  10233  xposdif  10234  xlesubadd  10235  xleaddadd  10239  fzsuc2  10435  fzm1  10456  fzoval  10504  exbtwnzlemstep  10631  exbtwnzlemshrink  10632  exbtwnzlemex  10633  exbtwnz  10634  rebtwn2zlemstep  10636  rebtwn2zlemshrink  10637  rebtwn2z  10638  flqlelt  10660  flqbi  10674  fldiv4p1lem1div2  10689  fldiv4lem1div2  10691  modqval  10710  modqadd1  10747  modqmuladd  10752  modqmuladdnn0  10754  modqm1p1mod0  10761  modqmul1  10763  modfzo0difsn  10781  addmodlteq  10784  frec2uzzd  10786  frec2uzsucd  10787  frec2uzrand  10791  frecuzrdgrrn  10794  frec2uzrdg  10795  frecuzrdgrcl  10796  frecuzrdgsuc  10800  frecuzrdgrclt  10801  frecuzrdgg  10802  frecuzrdgdom  10804  frecuzrdgfun  10806  frecuzrdgsuctlem  10809  frecuzrdgsuct  10810  uzsinds  10830  iseqvalcbv  10845  seq3val  10846  seqvalcd  10847  seqf  10850  seq3p1  10851  seqovcd  10853  seqp1cd  10856  seq3fveq2  10861  seqfveq2g  10863  seq3shft2  10867  seqshft2g  10868  monoord  10871  monoord2  10872  seq3split  10874  seqsplitg  10875  seq3caopr3  10877  seqcaopr3g  10878  seq3caopr2  10879  seqcaopr2g  10880  iseqf1olemqval  10886  iseqf1olemqk  10893  seqf1oglem2a  10904  seqf1oglem2  10906  seq3id2  10912  seq3homo  10913  seq3z  10914  seqhomog  10916  seqfeq4g  10917  seq3distr  10918  m1expcl2  10947  mulexp  10964  expadd  10967  expmul  10970  sq0i  11017  qsqeqor  11036  resq01  11044  sqoddm1div8  11080  facp1  11117  faclbnd  11128  faclbnd3  11130  bcval  11136  bcn1  11145  bcval5  11150  bcpasc  11153  bccl  11154  hashfz1  11171  omgadd  11191  hashfzo  11212  hashfzp1  11214  hashxp  11216  hashmap  11217  seq3coll  11239  lsw1  11299  ccats1val2  11353  ccatw2s1p2  11359  pfxsuff1eqwrdeq  11416  swrdswrd  11422  ccats1pfxeq  11431  ccatopth  11433  wrdind  11439  wrd2ind  11440  swrdccatin2  11446  pfxccatin12lem2  11448  swrdccat3blem  11456  ccats1pfxeqbi  11459  swrdccatin2d  11461  reuccatpfxs1  11464  shftlem  11526  shftfvalg  11528  shftfibg  11530  shftfval  11531  shftfib  11533  shftfn  11534  shftf  11540  2shfti  11541  shftvalg  11546  shftval4g  11547  cjval  11555  imval  11560  cjexp  11603  cnrecnv  11620  cvg1nlemcau  11694  cvg1nlemres  11695  resqrexlemcalc3  11726  resqrexlemex  11735  rsqrmo  11737  resqrtcl  11739  rersqrtthlem  11740  sqrtsq  11754  absexp  11789  recan  11819  climshft  12014  climcn1  12018  climcn2  12019  subcn2  12021  fsumshft  12155  fisum0diag2  12158  fsumiun  12188  binomlem  12194  binom  12195  bcxmas  12200  isumsplit  12202  arisum2  12210  trireciplem  12211  trirecip  12212  geolim  12222  cvgratnnlemnexp  12235  cvgratnnlemmn  12236  clim2prod  12250  prodfrecap  12257  fprodcl2lem  12316  fprodfac  12326  fprodshft  12329  ef0lem  12371  efval  12372  efne0  12389  efexp  12393  demoivreALT  12485  dvdsval2  12501  p1modz1  12505  dvds0lem  12512  dvds1lem  12513  dvds2lem  12514  dvdsmulc  12530  divconjdvds  12560  odd2np1lem  12583  odd2np1  12584  ltoddhalfle  12604  halfleoddlt  12605  nn0o1gt2  12616  nn0o  12618  divalglemnn  12629  divalglemeunn  12632  divalglemex  12633  divalglemeuneg  12634  flodddiv4  12647  bitsinv1  12673  gcdabs1  12710  gcddiv  12740  dvdssqim  12745  rpmulgcd  12747  bezoutr1  12754  uzwodc  12758  dvdslcm  12791  lcmeq0  12793  lcmdvds  12801  divgcdcoprm0  12823  prmind2  12842  isprm5lem  12863  isprm6  12869  rpexp  12875  sqrt2irr  12884  pw2dvdslemn  12887  pw2dvdseu  12890  oddpwdclemxy  12891  nn0gcdsq  12922  phicl2  12936  phibndlem  12938  hashdvds  12943  crth  12946  phimullem  12947  eulerthlem1  12949  eulerthlemfi  12950  eulerthlemrprm  12951  eulerthlemth  12954  eulerth  12955  hashgcdlem  12960  phisum  12963  odzval  12964  modprm0  12977  nnnn0modprm0  12978  pythagtriplem1  12988  pythagtriplem6  12993  pythagtriplem7  12994  pythagtriplem12  12998  pythagtriplem14  13000  pythagtriplem18  13004  pythagtriplem19  13005  pceulem  13017  pceu  13018  pcval  13019  pczpre  13020  pcdiv  13025  pcqmul  13026  pcqcl  13029  pcexp  13032  pcaddlem  13062  pcadd  13063  pcmpt  13066  pcprod  13069  pcfac  13073  expnprm  13076  prmpwdvds  13078  pockthi  13081  1arithlem2  13087  4sqlem2  13112  4sqlem3  13113  4sqlem11  13124  4sqlem12  13125  4sqlem13m  13126  4sqlem17  13130  4sqlem18  13131  4sqlem19  13132  ballotfilemfc0  13176  ballotfilemfcc  13177  ennnfonelemr  13258  ctinfom  13263  infpn2  13291  ercpbl  13595  mgm1  13633  mgmidmo  13635  ismgmid  13640  mgmlrid  13642  ismgmid2  13643  lidrideqd  13644  lidrididd  13645  mgmidsssn0  13647  grprida  13650  gsumfzval  13654  gsumress  13658  gsumval2  13660  isnsgrp  13669  sgrpass  13671  sgrp1  13674  sgrpidmndm  13681  ismndd  13698  mndinvmod  13706  imasmnd2  13707  mnd1  13710  mnd1id  13711  mhmpropd  13721  insubm  13740  mhmima  13746  gsumvallem2  13748  grppropd  13772  isgrpd2  13776  isgrpd  13778  dfgrp2  13782  grprcan  13792  grpinveu  13793  grpsubval  13801  grplinv  13805  grpinvid2  13808  isgrpinv  13809  grplrinv  13812  grpidinv2  13813  grpidinv  13814  grpidssd  13831  grpinvssd  13832  dfgrp3mlem  13853  dfgrp3m  13854  grplactfval  13856  grp1  13861  imasgrp2  13863  mhmmnd  13869  ghmgrp  13871  mulgnn0gsum  13881  mulgnn0p1  13886  mulgnn0subcl  13888  mulgaddcom  13899  mulginvcom  13900  mulgnn0z  13902  mulgneg2  13909  mulgnnass  13910  mulgnn0ass  13911  mhmmulg  13916  issubg  13926  subgex  13929  issubg2m  13942  issubg4m  13946  isnsg2  13956  nsgbi  13957  isnsg3  13960  elnmz  13961  nmzbi  13962  ghmrn  14010  ghmnsgima  14021  gsumfzconst  14094  gfsumval  14102  gsumshift  14105  rngdi  14179  rngdir  14180  srgrz  14227  srgmulgass  14232  srgpcomp  14233  srgrmhm  14237  ringid  14269  ringinvnzdiv  14293  mulgass2  14301  ring1  14302  ringrghm  14305  imasring  14307  dvdsrmuld  14341  dvdsrmul1  14347  dvdsr01  14349  dvreq1  14387  rhmdvdsr  14420  lringuplu  14441  issubrng  14445  issubrng2  14456  issubrg  14467  issubrg2  14487  isrrg  14509  domneq0  14519  lmodlema  14566  islmodd  14567  lmodvsmmulgdi  14597  rmodislmodlem  14624  rmodislmod  14625  lssclg  14638  lss1d  14657  lspsn  14690  sraval  14711  rnglidlmcl  14754  quscrng  14807  cnfldmulg  14850  cnfldexp  14851  gsumfzfsumlemm  14861  cnfldui  14863  expghmap  14881  mulgghm2  14882  mulgrhm  14883  zrhmulg  14894  zlmval  14901  znunit  14933  cnmptcom  15289  psmettri2  15319  isxmet2d  15339  xmeteq0  15350  xmettri2  15352  metrest  15497  mpomulcn  15557  expcn  15560  cncfval  15563  mulc1cncf  15580  addccncf  15591  mulcncf  15599  expcncf  15600  hovera  15638  hoverb  15639  hoverlt1  15640  hovergt0  15641  ivthdich  15644  limccnp2lem  15667  dvcnp2cntop  15690  dvcoapbr  15698  dvexp  15702  dvrecap  15704  dvef  15718  plyadd  15742  plymul  15743  plycoeid3  15748  plyco  15750  plycjlemc  15751  plycj  15752  plyrecj  15754  dvply1  15756  dvply2g  15757  sincn  15760  coscn  15761  ptolemy  15815  sincosq1eq  15830  rpcxpmul2  15904  logbgcd1irr  15958  logbgcd1irraplemexp  15959  2irrexpq  15967  2irrexpqap  15969  pellexlem3  15973  mpodvdsmulf1o  15984  fsumdvdsmul  15985  sgmppw  15986  sgmmul  15990  perfect  15995  lgslem4  16002  lgsval  16003  lgsfvalg  16004  lgsval2lem  16009  lgsdir2lem4  16030  lgsdir  16034  lgsdilem2  16035  lgsdi  16036  lgsne0  16037  lgsmodeq  16044  lgsdirnn0  16046  lgsdinn0  16047  gausslemma2dlem0i  16056  gausslemma2dlem1a  16057  gausslemma2dlem1f1o  16059  gausslemma2dlem2  16061  gausslemma2dlem3  16062  gausslemma2dlem4  16063  lgseisenlem2  16070  lgsquadlem2  16077  lgsquadlem3  16078  lgsquad  16079  lgsquad2lem2  16081  2lgslem1a  16087  2lgslem1b  16088  2lgslem1c  16089  2lgslem3a  16092  2lgslem3b  16093  2lgslem3c  16094  2lgslem3d  16095  2lgslem3a1  16096  2lgslem3b1  16097  2lgslem3c1  16098  2lgslem3d1  16099  2lgs  16103  2lgsoddprmlem1  16104  2lgsoddprmlem3  16110  2sqlem2  16114  2sqlem6  16119  2sqlem8  16122  2sqlem9  16123  wlklenvm1  16462  wlklenvm1g  16463  wlkl1loop  16479  2wlklem  16497  clwwlknnn  16533  clwwlknp  16538  clwwlkn1  16539  clwwlkn2  16542  clwwlkext2edg  16543  umgr2cwwk2dif  16545  clwwlknon  16550  clwwlk0on0  16552  clwwlknonex2lem1  16558  clwwlknonex2lem2  16559  clwwlknonex2  16560  qdencn  16933  isomninn  16941  trirec0  16954  iswomninn  16961  ismkvnn  16964