Theorem oveq1 5974

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 3833	. . 3 ⊢ (𝐴 = 𝐵 → ⟨𝐴, 𝐶⟩ = ⟨𝐵, 𝐶⟩)
2	1	fveq2d 5603	. 2 ⊢ (𝐴 = 𝐵 → (𝐹‘⟨𝐴, 𝐶⟩) = (𝐹‘⟨𝐵, 𝐶⟩))
3		df-ov 5970	. 2 ⊢ (𝐴𝐹𝐶) = (𝐹‘⟨𝐴, 𝐶⟩)
4		df-ov 5970	. 2 ⊢ (𝐵𝐹𝐶) = (𝐹‘⟨𝐵, 𝐶⟩)
5	2, 3, 4	3eqtr4g 2265	1 ⊢ (𝐴 = 𝐵 → (𝐴𝐹𝐶) = (𝐵𝐹𝐶))

Syntax hints:   → wi 4   = wceq 1373  ⟨cop 3646  ‘cfv 5290  (class class class)co 5967

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 711  ax-5 1471  ax-7 1472  ax-gen 1473  ax-ie1 1517  ax-ie2 1518  ax-8 1528  ax-10 1529  ax-11 1530  ax-i12 1531  ax-bndl 1533  ax-4 1534  ax-17 1550  ax-i9 1554  ax-ial 1558  ax-i5r 1559  ax-ext 2189

This theorem depends on definitions:  df-bi 117  df-3an 983  df-tru 1376  df-nf 1485  df-sb 1787  df-clab 2194  df-cleq 2200  df-clel 2203  df-nfc 2339  df-rex 2492  df-v 2778  df-un 3178  df-sn 3649  df-pr 3650  df-op 3652  df-uni 3865  df-br 4060  df-iota 5251  df-fv 5298  df-ov 5970

This theorem is referenced by:  oveq12  5976  oveq1i  5977  oveq1d  5982  ovrspc2v  5993  oveqrspc2v  5994  rspceov  6010  fovcld  6073  ovmpos  6092  ov2gf  6093  ovi3  6106  caovclg  6122  caovcomg  6125  caovassg  6128  caovcang  6131  caovcan  6134  caovordig  6135  caovordg  6137  caovord  6141  caovdig  6144  caovdirg  6147  caovimo  6163  suppssov1  6178  off  6194  caofid0r  6209  caofid1  6210  caofdig  6215  omcl  6570  oeicl  6571  omv2  6574  nnm0r  6588  nnacom  6593  nndi  6595  nnmass  6596  nnmsucr  6597  nnmcom  6598  nnaword  6620  nnmord  6626  nnm00  6639  eroveu  6736  th3qlem2  6748  th3q  6750  ecovcom  6752  ecovicom  6753  ecovass  6754  ecoviass  6755  ecovdi  6756  ecovidi  6757  map0g  6798  addcmpblnq  7515  addclnq  7523  mulclnq  7524  mulidnq  7537  recexnq  7538  recmulnqg  7539  ltanqg  7548  ltmnqg  7549  ltexnqq  7556  enq0ref  7581  enq0tr  7582  addcmpblnq0  7591  mulnnnq0  7598  addclnq0  7599  mulclnq0  7600  distrnq0  7607  mulcomnq0  7608  addassnq0  7610  prarloclemlo  7642  prarloclem3  7645  prarloclem5  7648  prarloclemcalc  7650  genipv  7657  genpassl  7672  genpassu  7673  addlocprlemeq  7681  distrlem4prl  7732  distrlem4pru  7733  ltexprlemdisj  7754  ltexprlemloc  7755  ltexprlemrl  7758  ltexprlemru  7760  prplnqu  7768  cauappcvgprlemm  7793  cauappcvgprlemopl  7794  cauappcvgprlemlol  7795  cauappcvgprlemdisj  7799  cauappcvgprlemloc  7800  cauappcvgprlemladdfl  7803  cauappcvgprlemladdru  7804  cauappcvgprlemladdrl  7805  cauappcvgprlem1  7807  cauappcvgprlemlim  7809  cauappcvgpr  7810  caucvgprlemm  7816  caucvgprlemopl  7817  caucvgprlemlol  7818  caucvgprlemdisj  7822  caucvgprlemloc  7823  caucvgprlemladdrl  7826  caucvgprlem1  7827  caucvgpr  7830  caucvgprprlemell  7833  caucvgprprlemml  7842  caucvgprpr  7860  mulcmpblnrlemg  7888  addclsr  7901  mulclsr  7902  0idsr  7915  1idsr  7916  00sr  7917  ltasrg  7918  recexgt0sr  7921  mulgt0sr  7926  mulextsr1  7929  prsrriota  7936  caucvgsrlemgt1  7943  caucvgsrlemoffres  7948  pitonn  7996  peano2nnnn  8001  axaddrcl  8013  axmulrcl  8015  axaddcom  8018  ax1rid  8025  ax0id  8026  axprecex  8028  axcnre  8029  axpre-ltadd  8034  axpre-mulgt0  8035  axpre-mulext  8036  rereceu  8037  peano5nnnn  8040  axcaucvglemcau  8046  axcaucvglemres  8047  mulrid  8104  cnegexlem1  8282  cnegexlem2  8283  cnegex  8285  addcan2  8288  subval  8299  addlsub  8477  apreim  8711  recexap  8761  receuap  8777  divvalap  8782  cju  9069  peano2nn  9083  nn1m1nn  9089  nn1suc  9090  nnsub  9110  fv0p1e1  9186  nnm1nn0  9371  zdiv  9496  zneo  9509  nneoor  9510  zeo  9513  peano5uzti  9516  nn0ind-raph  9525  uzind4s  9746  uzind4s2  9747  qmulz  9779  elpq  9805  cnref1o  9807  nn0ledivnn  9924  xaddnemnf  10014  xaddnepnf  10015  xaddcom  10018  xaddid1  10019  xnn0xadd0  10024  xaddass  10026  xpncan  10028  xleadd1a  10030  xltadd1  10033  xlt2add  10037  xsubge0  10038  xposdif  10039  xlesubadd  10040  xleaddadd  10044  fzsuc2  10236  fzm1  10257  fzoval  10305  exbtwnzlemstep  10427  exbtwnzlemshrink  10428  exbtwnzlemex  10429  exbtwnz  10430  rebtwn2zlemstep  10432  rebtwn2zlemshrink  10433  rebtwn2z  10434  flqlelt  10456  flqbi  10470  fldiv4p1lem1div2  10485  fldiv4lem1div2  10487  modqval  10506  modqadd1  10543  modqmuladd  10548  modqmuladdnn0  10550  modqm1p1mod0  10557  modqmul1  10559  modfzo0difsn  10577  addmodlteq  10580  frec2uzzd  10582  frec2uzsucd  10583  frec2uzrand  10587  frecuzrdgrrn  10590  frec2uzrdg  10591  frecuzrdgrcl  10592  frecuzrdgsuc  10596  frecuzrdgrclt  10597  frecuzrdgg  10598  frecuzrdgdom  10600  frecuzrdgfun  10602  frecuzrdgsuctlem  10605  frecuzrdgsuct  10606  uzsinds  10626  iseqvalcbv  10641  seq3val  10642  seqvalcd  10643  seqf  10646  seq3p1  10647  seqovcd  10649  seqp1cd  10652  seq3fveq2  10657  seqfveq2g  10659  seq3shft2  10663  seqshft2g  10664  monoord  10667  monoord2  10668  seq3split  10670  seqsplitg  10671  seq3caopr3  10673  seqcaopr3g  10674  seq3caopr2  10675  seqcaopr2g  10676  iseqf1olemqval  10682  iseqf1olemqk  10689  seqf1oglem2a  10700  seqf1oglem2  10702  seq3id2  10708  seq3homo  10709  seq3z  10710  seqhomog  10712  seqfeq4g  10713  seq3distr  10714  m1expcl2  10743  mulexp  10760  expadd  10763  expmul  10766  sq0i  10813  qsqeqor  10832  sqoddm1div8  10875  facp1  10912  faclbnd  10923  faclbnd3  10925  bcval  10931  bcn1  10940  bcval5  10945  bcpasc  10948  bccl  10949  hashfz1  10965  omgadd  10984  hashfzo  11004  hashfzp1  11006  hashxp  11008  seq3coll  11024  lsw1  11080  ccats1val2  11130  ccatw2s1p2  11135  pfxsuff1eqwrdeq  11190  swrdswrd  11196  ccats1pfxeq  11205  ccatopth  11207  wrdind  11213  wrd2ind  11214  swrdccatin2  11220  pfxccatin12lem2  11222  swrdccat3blem  11230  ccats1pfxeqbi  11233  swrdccatin2d  11235  reuccatpfxs1  11238  shftlem  11242  shftfvalg  11244  shftfibg  11246  shftfval  11247  shftfib  11249  shftfn  11250  shftf  11256  2shfti  11257  shftvalg  11262  shftval4g  11263  cjval  11271  imval  11276  cjexp  11319  cnrecnv  11336  cvg1nlemcau  11410  cvg1nlemres  11411  resqrexlemcalc3  11442  resqrexlemex  11451  rsqrmo  11453  resqrtcl  11455  rersqrtthlem  11456  sqrtsq  11470  absexp  11505  recan  11535  climshft  11730  climcn1  11734  climcn2  11735  subcn2  11737  fsumshft  11870  fisum0diag2  11873  fsumiun  11903  binomlem  11909  binom  11910  bcxmas  11915  isumsplit  11917  arisum2  11925  trireciplem  11926  trirecip  11927  geolim  11937  cvgratnnlemnexp  11950  cvgratnnlemmn  11951  clim2prod  11965  prodfrecap  11972  fprodcl2lem  12031  fprodfac  12041  fprodshft  12044  ef0lem  12086  efval  12087  efne0  12104  efexp  12108  demoivreALT  12200  dvdsval2  12216  p1modz1  12220  dvds0lem  12227  dvds1lem  12228  dvds2lem  12229  dvdsmulc  12245  divconjdvds  12275  odd2np1lem  12298  odd2np1  12299  ltoddhalfle  12319  halfleoddlt  12320  nn0o1gt2  12331  nn0o  12333  divalglemnn  12344  divalglemeunn  12347  divalglemex  12348  divalglemeuneg  12349  flodddiv4  12362  bitsinv1  12388  gcdabs1  12425  gcddiv  12455  dvdssqim  12460  rpmulgcd  12462  bezoutr1  12469  uzwodc  12473  dvdslcm  12506  lcmeq0  12508  lcmdvds  12516  divgcdcoprm0  12538  prmind2  12557  isprm5lem  12578  isprm6  12584  rpexp  12590  sqrt2irr  12599  pw2dvdslemn  12602  pw2dvdseu  12605  oddpwdclemxy  12606  nn0gcdsq  12637  phicl2  12651  phibndlem  12653  hashdvds  12658  crth  12661  phimullem  12662  eulerthlem1  12664  eulerthlemfi  12665  eulerthlemrprm  12666  eulerthlemth  12669  eulerth  12670  hashgcdlem  12675  phisum  12678  odzval  12679  modprm0  12692  nnnn0modprm0  12693  pythagtriplem1  12703  pythagtriplem6  12708  pythagtriplem7  12709  pythagtriplem12  12713  pythagtriplem14  12715  pythagtriplem18  12719  pythagtriplem19  12720  pceulem  12732  pceu  12733  pcval  12734  pczpre  12735  pcdiv  12740  pcqmul  12741  pcqcl  12744  pcexp  12747  pcaddlem  12777  pcadd  12778  pcmpt  12781  pcprod  12784  pcfac  12788  expnprm  12791  prmpwdvds  12793  pockthi  12796  1arithlem2  12802  4sqlem2  12827  4sqlem3  12828  4sqlem11  12839  4sqlem12  12840  4sqlem13m  12841  4sqlem17  12845  4sqlem18  12846  4sqlem19  12847  ennnfonelemr  12909  ctinfom  12914  infpn2  12942  ercpbl  13278  mgm1  13317  mgmidmo  13319  ismgmid  13324  mgmlrid  13326  ismgmid2  13327  lidrideqd  13328  lidrididd  13329  mgmidsssn0  13331  grprida  13334  gsumfzval  13338  gsumress  13342  gsumval2  13344  isnsgrp  13353  sgrpass  13355  sgrp1  13358  sgrpidmndm  13367  ismndd  13384  mndinvmod  13392  imasmnd2  13399  mnd1  13402  mnd1id  13403  mhmpropd  13413  insubm  13432  mhmima  13438  gsumvallem2  13440  grppropd  13464  isgrpd2  13468  isgrpd  13470  dfgrp2  13474  grprcan  13484  grpinveu  13485  grpsubval  13493  grplinv  13497  grpinvid2  13500  isgrpinv  13501  grplrinv  13504  grpidinv2  13505  grpidinv  13506  grpidssd  13523  grpinvssd  13524  dfgrp3mlem  13545  dfgrp3m  13546  grplactfval  13548  grp1  13553  imasgrp2  13561  mhmmnd  13567  ghmgrp  13569  mulgnn0gsum  13579  mulgnn0p1  13584  mulgnn0subcl  13586  mulgaddcom  13597  mulginvcom  13598  mulgnn0z  13600  mulgneg2  13607  mulgnnass  13608  mulgnn0ass  13609  mhmmulg  13614  issubg  13624  subgex  13627  issubg2m  13640  issubg4m  13644  isnsg2  13654  nsgbi  13655  isnsg3  13658  elnmz  13659  nmzbi  13660  ghmrn  13708  ghmnsgima  13719  gsumfzconst  13792  rngdi  13817  rngdir  13818  srgrz  13861  srgmulgass  13866  srgpcomp  13867  srgrmhm  13871  ringid  13903  ringinvnzdiv  13927  mulgass2  13935  ring1  13936  ringrghm  13939  imasring  13941  dvdsrmuld  13973  dvdsrmul1  13979  dvdsr01  13981  dvreq1  14019  rhmdvdsr  14052  lringuplu  14073  issubrng  14076  issubrng2  14087  issubrg  14098  issubrg2  14118  isrrg  14140  domneq0  14149  lmodlema  14169  islmodd  14170  lmodvsmmulgdi  14200  rmodislmodlem  14227  rmodislmod  14228  lssclg  14241  lss1d  14260  lspsn  14293  sraval  14314  rnglidlmcl  14357  quscrng  14410  cnfldmulg  14453  cnfldexp  14454  gsumfzfsumlemm  14464  cnfldui  14466  expghmap  14484  mulgghm2  14485  mulgrhm  14486  zrhmulg  14497  zlmval  14504  znunit  14536  cnmptcom  14885  psmettri2  14915  isxmet2d  14935  xmeteq0  14946  xmettri2  14948  metrest  15093  mpomulcn  15153  expcn  15156  cncfval  15159  mulc1cncf  15176  addccncf  15187  mulcncf  15195  expcncf  15196  hovera  15234  hoverb  15235  hoverlt1  15236  hovergt0  15237  ivthdich  15240  limccnp2lem  15263  dvcnp2cntop  15286  dvcoapbr  15294  dvexp  15298  dvrecap  15300  dvef  15314  plyadd  15338  plymul  15339  plycoeid3  15344  plyco  15346  plycjlemc  15347  plycj  15348  plyrecj  15350  dvply1  15352  dvply2g  15353  sincn  15356  coscn  15357  ptolemy  15411  sincosq1eq  15426  rpcxpmul2  15500  logbgcd1irr  15554  logbgcd1irraplemexp  15555  2irrexpq  15563  2irrexpqap  15565  mpodvdsmulf1o  15577  fsumdvdsmul  15578  sgmppw  15579  sgmmul  15583  perfect  15588  lgslem4  15595  lgsval  15596  lgsfvalg  15597  lgsval2lem  15602  lgsdir2lem4  15623  lgsdir  15627  lgsdilem2  15628  lgsdi  15629  lgsne0  15630  lgsmodeq  15637  lgsdirnn0  15639  lgsdinn0  15640  gausslemma2dlem0i  15649  gausslemma2dlem1a  15650  gausslemma2dlem1f1o  15652  gausslemma2dlem2  15654  gausslemma2dlem3  15655  gausslemma2dlem4  15656  lgseisenlem2  15663  lgsquadlem2  15670  lgsquadlem3  15671  lgsquad  15672  lgsquad2lem2  15674  2lgslem1a  15680  2lgslem1b  15681  2lgslem1c  15682  2lgslem3a  15685  2lgslem3b  15686  2lgslem3c  15687  2lgslem3d  15688  2lgslem3a1  15689  2lgslem3b1  15690  2lgslem3c1  15691  2lgslem3d1  15692  2lgs  15696  2lgsoddprmlem1  15697  2lgsoddprmlem3  15703  2sqlem2  15707  2sqlem6  15712  2sqlem8  15715  2sqlem9  15716  qdencn  16168  isomninn  16172  trirec0  16185  iswomninn  16191  ismkvnn  16194