Theorem oveq1 6035

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

Syntax hints:   → wi 4   = wceq 1398  ⟨cop 3676  ‘cfv 5333  (class class class)co 6028

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 2213

This theorem depends on definitions:  df-bi 117  df-3an 1007  df-tru 1401  df-nf 1510  df-sb 1811  df-clab 2218  df-cleq 2224  df-clel 2227  df-nfc 2364  df-rex 2517  df-v 2805  df-un 3205  df-sn 3679  df-pr 3680  df-op 3682  df-uni 3899  df-br 4094  df-iota 5293  df-fv 5341  df-ov 6031

This theorem is referenced by:  oveq12  6037  oveq1i  6038  oveq1d  6043  ovrspc2v  6054  oveqrspc2v  6055  rspceov  6071  fovcld  6136  ovmpos  6155  ov2gf  6156  ovi3  6169  caovclg  6185  caovcomg  6188  caovassg  6191  caovcang  6194  caovcan  6197  caovordig  6198  caovordg  6200  caovord  6204  caovdig  6207  caovdirg  6210  caovimo  6226  suppssov1  6241  off  6257  caofid0r  6272  caofid1  6273  caofdig  6278  suppofss1dcl  6442  suppofss2dcl  6443  omcl  6672  oeicl  6673  omv2  6676  nnm0r  6690  nnacom  6695  nndi  6697  nnmass  6698  nnmsucr  6699  nnmcom  6700  nnaword  6722  nnmord  6728  nnm00  6741  eroveu  6838  th3qlem2  6850  th3q  6852  ecovcom  6854  ecovicom  6855  ecovass  6856  ecoviass  6857  ecovdi  6858  ecovidi  6859  map0g  6900  addcmpblnq  7647  addclnq  7655  mulclnq  7656  mulidnq  7669  recexnq  7670  recmulnqg  7671  ltanqg  7680  ltmnqg  7681  ltexnqq  7688  enq0ref  7713  enq0tr  7714  addcmpblnq0  7723  mulnnnq0  7730  addclnq0  7731  mulclnq0  7732  distrnq0  7739  mulcomnq0  7740  addassnq0  7742  prarloclemlo  7774  prarloclem3  7777  prarloclem5  7780  prarloclemcalc  7782  genipv  7789  genpassl  7804  genpassu  7805  addlocprlemeq  7813  distrlem4prl  7864  distrlem4pru  7865  ltexprlemdisj  7886  ltexprlemloc  7887  ltexprlemrl  7890  ltexprlemru  7892  prplnqu  7900  cauappcvgprlemm  7925  cauappcvgprlemopl  7926  cauappcvgprlemlol  7927  cauappcvgprlemdisj  7931  cauappcvgprlemloc  7932  cauappcvgprlemladdfl  7935  cauappcvgprlemladdru  7936  cauappcvgprlemladdrl  7937  cauappcvgprlem1  7939  cauappcvgprlemlim  7941  cauappcvgpr  7942  caucvgprlemm  7948  caucvgprlemopl  7949  caucvgprlemlol  7950  caucvgprlemdisj  7954  caucvgprlemloc  7955  caucvgprlemladdrl  7958  caucvgprlem1  7959  caucvgpr  7962  caucvgprprlemell  7965  caucvgprprlemml  7974  caucvgprpr  7992  mulcmpblnrlemg  8020  addclsr  8033  mulclsr  8034  0idsr  8047  1idsr  8048  00sr  8049  ltasrg  8050  recexgt0sr  8053  mulgt0sr  8058  mulextsr1  8061  prsrriota  8068  caucvgsrlemgt1  8075  caucvgsrlemoffres  8080  pitonn  8128  peano2nnnn  8133  axaddrcl  8145  axmulrcl  8147  axaddcom  8150  ax1rid  8157  ax0id  8158  axprecex  8160  axcnre  8161  axpre-ltadd  8166  axpre-mulgt0  8167  axpre-mulext  8168  rereceu  8169  peano5nnnn  8172  axcaucvglemcau  8178  axcaucvglemres  8179  mulrid  8236  cnegexlem1  8413  cnegexlem2  8414  cnegex  8416  addcan2  8419  subval  8430  addlsub  8608  apreim  8842  recexap  8892  receuap  8908  divvalap  8913  cju  9200  peano2nn  9214  nn1m1nn  9220  nn1suc  9221  nnsub  9241  fv0p1e1  9317  nnm1nn0  9502  zdiv  9629  zneo  9642  nneoor  9643  zeo  9646  peano5uzti  9649  nn0ind-raph  9658  uzind4s  9885  uzind4s2  9886  qmulz  9918  elpq  9944  cnref1o  9946  nn0ledivnn  10063  xaddnemnf  10153  xaddnepnf  10154  xaddcom  10157  xaddid1  10158  xnn0xadd0  10163  xaddass  10165  xpncan  10167  xleadd1a  10169  xltadd1  10172  xlt2add  10176  xsubge0  10177  xposdif  10178  xlesubadd  10179  xleaddadd  10183  fzsuc2  10376  fzm1  10397  fzoval  10445  exbtwnzlemstep  10570  exbtwnzlemshrink  10571  exbtwnzlemex  10572  exbtwnz  10573  rebtwn2zlemstep  10575  rebtwn2zlemshrink  10576  rebtwn2z  10577  flqlelt  10599  flqbi  10613  fldiv4p1lem1div2  10628  fldiv4lem1div2  10630  modqval  10649  modqadd1  10686  modqmuladd  10691  modqmuladdnn0  10693  modqm1p1mod0  10700  modqmul1  10702  modfzo0difsn  10720  addmodlteq  10723  frec2uzzd  10725  frec2uzsucd  10726  frec2uzrand  10730  frecuzrdgrrn  10733  frec2uzrdg  10734  frecuzrdgrcl  10735  frecuzrdgsuc  10739  frecuzrdgrclt  10740  frecuzrdgg  10741  frecuzrdgdom  10743  frecuzrdgfun  10745  frecuzrdgsuctlem  10748  frecuzrdgsuct  10749  uzsinds  10769  iseqvalcbv  10784  seq3val  10785  seqvalcd  10786  seqf  10789  seq3p1  10790  seqovcd  10792  seqp1cd  10795  seq3fveq2  10800  seqfveq2g  10802  seq3shft2  10806  seqshft2g  10807  monoord  10810  monoord2  10811  seq3split  10813  seqsplitg  10814  seq3caopr3  10816  seqcaopr3g  10817  seq3caopr2  10818  seqcaopr2g  10819  iseqf1olemqval  10825  iseqf1olemqk  10832  seqf1oglem2a  10843  seqf1oglem2  10845  seq3id2  10851  seq3homo  10852  seq3z  10853  seqhomog  10855  seqfeq4g  10856  seq3distr  10857  m1expcl2  10886  mulexp  10903  expadd  10906  expmul  10909  sq0i  10956  qsqeqor  10975  sqoddm1div8  11018  facp1  11055  faclbnd  11066  faclbnd3  11068  bcval  11074  bcn1  11083  bcval5  11088  bcpasc  11091  bccl  11092  hashfz1  11108  omgadd  11128  hashfzo  11149  hashfzp1  11151  hashxp  11153  seq3coll  11169  lsw1  11229  ccats1val2  11283  ccatw2s1p2  11289  pfxsuff1eqwrdeq  11346  swrdswrd  11352  ccats1pfxeq  11361  ccatopth  11363  wrdind  11369  wrd2ind  11370  swrdccatin2  11376  pfxccatin12lem2  11378  swrdccat3blem  11386  ccats1pfxeqbi  11389  swrdccatin2d  11391  reuccatpfxs1  11394  shftlem  11456  shftfvalg  11458  shftfibg  11460  shftfval  11461  shftfib  11463  shftfn  11464  shftf  11470  2shfti  11471  shftvalg  11476  shftval4g  11477  cjval  11485  imval  11490  cjexp  11533  cnrecnv  11550  cvg1nlemcau  11624  cvg1nlemres  11625  resqrexlemcalc3  11656  resqrexlemex  11665  rsqrmo  11667  resqrtcl  11669  rersqrtthlem  11670  sqrtsq  11684  absexp  11719  recan  11749  climshft  11944  climcn1  11948  climcn2  11949  subcn2  11951  fsumshft  12085  fisum0diag2  12088  fsumiun  12118  binomlem  12124  binom  12125  bcxmas  12130  isumsplit  12132  arisum2  12140  trireciplem  12141  trirecip  12142  geolim  12152  cvgratnnlemnexp  12165  cvgratnnlemmn  12166  clim2prod  12180  prodfrecap  12187  fprodcl2lem  12246  fprodfac  12256  fprodshft  12259  ef0lem  12301  efval  12302  efne0  12319  efexp  12323  demoivreALT  12415  dvdsval2  12431  p1modz1  12435  dvds0lem  12442  dvds1lem  12443  dvds2lem  12444  dvdsmulc  12460  divconjdvds  12490  odd2np1lem  12513  odd2np1  12514  ltoddhalfle  12534  halfleoddlt  12535  nn0o1gt2  12546  nn0o  12548  divalglemnn  12559  divalglemeunn  12562  divalglemex  12563  divalglemeuneg  12564  flodddiv4  12577  bitsinv1  12603  gcdabs1  12640  gcddiv  12670  dvdssqim  12675  rpmulgcd  12677  bezoutr1  12684  uzwodc  12688  dvdslcm  12721  lcmeq0  12723  lcmdvds  12731  divgcdcoprm0  12753  prmind2  12772  isprm5lem  12793  isprm6  12799  rpexp  12805  sqrt2irr  12814  pw2dvdslemn  12817  pw2dvdseu  12820  oddpwdclemxy  12821  nn0gcdsq  12852  phicl2  12866  phibndlem  12868  hashdvds  12873  crth  12876  phimullem  12877  eulerthlem1  12879  eulerthlemfi  12880  eulerthlemrprm  12881  eulerthlemth  12884  eulerth  12885  hashgcdlem  12890  phisum  12893  odzval  12894  modprm0  12907  nnnn0modprm0  12908  pythagtriplem1  12918  pythagtriplem6  12923  pythagtriplem7  12924  pythagtriplem12  12928  pythagtriplem14  12930  pythagtriplem18  12934  pythagtriplem19  12935  pceulem  12947  pceu  12948  pcval  12949  pczpre  12950  pcdiv  12955  pcqmul  12956  pcqcl  12959  pcexp  12962  pcaddlem  12992  pcadd  12993  pcmpt  12996  pcprod  12999  pcfac  13003  expnprm  13006  prmpwdvds  13008  pockthi  13011  1arithlem2  13017  4sqlem2  13042  4sqlem3  13043  4sqlem11  13054  4sqlem12  13055  4sqlem13m  13056  4sqlem17  13060  4sqlem18  13061  4sqlem19  13062  ennnfonelemr  13124  ctinfom  13129  infpn2  13157  ercpbl  13494  mgm1  13533  mgmidmo  13535  ismgmid  13540  mgmlrid  13542  ismgmid2  13543  lidrideqd  13544  lidrididd  13545  mgmidsssn0  13547  grprida  13550  gsumfzval  13554  gsumress  13558  gsumval2  13560  isnsgrp  13569  sgrpass  13571  sgrp1  13574  sgrpidmndm  13583  ismndd  13600  mndinvmod  13608  imasmnd2  13615  mnd1  13618  mnd1id  13619  mhmpropd  13629  insubm  13648  mhmima  13654  gsumvallem2  13656  grppropd  13680  isgrpd2  13684  isgrpd  13686  dfgrp2  13690  grprcan  13700  grpinveu  13701  grpsubval  13709  grplinv  13713  grpinvid2  13716  isgrpinv  13717  grplrinv  13720  grpidinv2  13721  grpidinv  13722  grpidssd  13739  grpinvssd  13740  dfgrp3mlem  13761  dfgrp3m  13762  grplactfval  13764  grp1  13769  imasgrp2  13777  mhmmnd  13783  ghmgrp  13785  mulgnn0gsum  13795  mulgnn0p1  13800  mulgnn0subcl  13802  mulgaddcom  13813  mulginvcom  13814  mulgnn0z  13816  mulgneg2  13823  mulgnnass  13824  mulgnn0ass  13825  mhmmulg  13830  issubg  13840  subgex  13843  issubg2m  13856  issubg4m  13860  isnsg2  13870  nsgbi  13871  isnsg3  13874  elnmz  13875  nmzbi  13876  ghmrn  13924  ghmnsgima  13935  gsumfzconst  14008  rngdi  14034  rngdir  14035  srgrz  14078  srgmulgass  14083  srgpcomp  14084  srgrmhm  14088  ringid  14120  ringinvnzdiv  14144  mulgass2  14152  ring1  14153  ringrghm  14156  imasring  14158  dvdsrmuld  14191  dvdsrmul1  14197  dvdsr01  14199  dvreq1  14237  rhmdvdsr  14270  lringuplu  14291  issubrng  14294  issubrng2  14305  issubrg  14316  issubrg2  14336  isrrg  14358  domneq0  14368  lmodlema  14388  islmodd  14389  lmodvsmmulgdi  14419  rmodislmodlem  14446  rmodislmod  14447  lssclg  14460  lss1d  14479  lspsn  14512  sraval  14533  rnglidlmcl  14576  quscrng  14629  cnfldmulg  14672  cnfldexp  14673  gsumfzfsumlemm  14683  cnfldui  14685  expghmap  14703  mulgghm2  14704  mulgrhm  14705  zrhmulg  14716  zlmval  14723  znunit  14755  cnmptcom  15109  psmettri2  15139  isxmet2d  15159  xmeteq0  15170  xmettri2  15172  metrest  15317  mpomulcn  15377  expcn  15380  cncfval  15383  mulc1cncf  15400  addccncf  15411  mulcncf  15419  expcncf  15420  hovera  15458  hoverb  15459  hoverlt1  15460  hovergt0  15461  ivthdich  15464  limccnp2lem  15487  dvcnp2cntop  15510  dvcoapbr  15518  dvexp  15522  dvrecap  15524  dvef  15538  plyadd  15562  plymul  15563  plycoeid3  15568  plyco  15570  plycjlemc  15571  plycj  15572  plyrecj  15574  dvply1  15576  dvply2g  15577  sincn  15580  coscn  15581  ptolemy  15635  sincosq1eq  15650  rpcxpmul2  15724  logbgcd1irr  15778  logbgcd1irraplemexp  15779  2irrexpq  15787  2irrexpqap  15789  pellexlem3  15793  mpodvdsmulf1o  15804  fsumdvdsmul  15805  sgmppw  15806  sgmmul  15810  perfect  15815  lgslem4  15822  lgsval  15823  lgsfvalg  15824  lgsval2lem  15829  lgsdir2lem4  15850  lgsdir  15854  lgsdilem2  15855  lgsdi  15856  lgsne0  15857  lgsmodeq  15864  lgsdirnn0  15866  lgsdinn0  15867  gausslemma2dlem0i  15876  gausslemma2dlem1a  15877  gausslemma2dlem1f1o  15879  gausslemma2dlem2  15881  gausslemma2dlem3  15882  gausslemma2dlem4  15883  lgseisenlem2  15890  lgsquadlem2  15897  lgsquadlem3  15898  lgsquad  15899  lgsquad2lem2  15901  2lgslem1a  15907  2lgslem1b  15908  2lgslem1c  15909  2lgslem3a  15912  2lgslem3b  15913  2lgslem3c  15914  2lgslem3d  15915  2lgslem3a1  15916  2lgslem3b1  15917  2lgslem3c1  15918  2lgslem3d1  15919  2lgs  15923  2lgsoddprmlem1  15924  2lgsoddprmlem3  15930  2sqlem2  15934  2sqlem6  15939  2sqlem8  15942  2sqlem9  15943  wlklenvm1  16282  wlklenvm1g  16283  wlkl1loop  16299  2wlklem  16317  clwwlknnn  16353  clwwlknp  16358  clwwlkn1  16359  clwwlkn2  16362  clwwlkext2edg  16363  umgr2cwwk2dif  16365  clwwlknon  16370  clwwlk0on0  16372  clwwlknonex2lem1  16378  clwwlknonex2lem2  16379  clwwlknonex2  16380  qdencn  16755  isomninn  16763  trirec0  16776  iswomninn  16783  ismkvnn  16786  gfsumval  16809  gsumgfsumlem  16812