Theorem oveq1 6085

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

Syntax hints:   → wi 4   = wceq 1402  ⟨cop 3711  ‘cfv 5375  (class class class)co 6078

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 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 theorem 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 3714  df-pr 3715  df-op 3717  df-uni 3934  df-br 4129  df-iota 5335  df-fv 5383  df-ov 6081

This theorem is referenced by:  oveq12  6087  oveq1i  6088  oveq1d  6093  ovrspc2v  6104  oveqrspc2v  6105  rspceov  6121  fovcld  6186  ovmpos  6205  ov2gf  6206  ovi3  6219  caovclg  6235  caovcomg  6238  caovassg  6241  caovcang  6244  caovcan  6247  caovordig  6248  caovordg  6250  caovord  6254  caovdig  6257  caovdirg  6260  caovimo  6276  suppssov1  6292  off  6308  caofid0r  6323  caofid1  6324  caofdig  6329  suppofss1dcl  6497  suppofss2dcl  6498  omcl  6727  oeicl  6728  omv2  6731  nnm0r  6745  nnacom  6750  nndi  6752  nnmass  6753  nnmsucr  6754  nnmcom  6755  nnaword  6777  nnmord  6783  nnm00  6796  eroveu  6893  th3qlem2  6905  th3q  6907  ecovcom  6909  ecovicom  6910  ecovass  6911  ecoviass  6912  ecovdi  6913  ecovidi  6914  map0g  6962  addcmpblnq  7727  addclnq  7735  mulclnq  7736  mulidnq  7749  recexnq  7750  recmulnqg  7751  ltanqg  7760  ltmnqg  7761  ltexnqq  7768  enq0ref  7793  enq0tr  7794  addcmpblnq0  7803  mulnnnq0  7810  addclnq0  7811  mulclnq0  7812  distrnq0  7819  mulcomnq0  7820  addassnq0  7822  prarloclemlo  7854  prarloclem3  7857  prarloclem5  7860  prarloclemcalc  7862  genipv  7869  genpassl  7884  genpassu  7885  addlocprlemeq  7893  distrlem4prl  7944  distrlem4pru  7945  ltexprlemdisj  7966  ltexprlemloc  7967  ltexprlemrl  7970  ltexprlemru  7972  prplnqu  7980  cauappcvgprlemm  8005  cauappcvgprlemopl  8006  cauappcvgprlemlol  8007  cauappcvgprlemdisj  8011  cauappcvgprlemloc  8012  cauappcvgprlemladdfl  8015  cauappcvgprlemladdru  8016  cauappcvgprlemladdrl  8017  cauappcvgprlem1  8019  cauappcvgprlemlim  8021  cauappcvgpr  8022  caucvgprlemm  8028  caucvgprlemopl  8029  caucvgprlemlol  8030  caucvgprlemdisj  8034  caucvgprlemloc  8035  caucvgprlemladdrl  8038  caucvgprlem1  8039  caucvgpr  8042  caucvgprprlemell  8045  caucvgprprlemml  8054  caucvgprpr  8072  mulcmpblnrlemg  8100  addclsr  8113  mulclsr  8114  0idsr  8127  1idsr  8128  00sr  8129  ltasrg  8130  recexgt0sr  8133  mulgt0sr  8138  mulextsr1  8141  prsrriota  8148  caucvgsrlemgt1  8155  caucvgsrlemoffres  8160  pitonn  8208  peano2nnnn  8213  axaddrcl  8225  axmulrcl  8227  axaddcom  8230  ax1rid  8237  ax0id  8238  axprecex  8240  axcnre  8241  axpre-ltadd  8246  axpre-mulgt0  8247  axpre-mulext  8248  rereceu  8249  peano5nnnn  8252  axcaucvglemcau  8258  axcaucvglemres  8259  mulrid  8316  cnegexlem1  8494  cnegexlem2  8495  cnegex  8497  addcan2  8500  subval  8511  addlsub  8689  apreim  8924  recexap  8974  receuap  8992  divvalap  8997  cju  9284  peano2nn  9298  nn1m1nn  9304  nn1suc  9305  nnsub  9325  fv0p1e1  9401  nnm1nn0  9586  zdiv  9716  zneo  9729  nneoor  9730  zeo  9733  peano5uzti  9736  nn0ind-raph  9745  uzind4s  9972  uzind4s2  9973  qmulz  10005  elpq  10031  cnref1o  10033  nn0ledivnn  10150  xaddnemnf  10241  xaddnepnf  10242  xaddcom  10245  xaddid1  10246  xnn0xadd0  10251  xaddass  10253  xpncan  10255  xleadd1a  10257  xltadd1  10260  xlt2add  10264  xsubge0  10265  xposdif  10266  xlesubadd  10267  xleaddadd  10271  fzsuc2  10467  fzm1  10488  fzoval  10536  exbtwnzlemstep  10663  exbtwnzlemshrink  10664  exbtwnzlemex  10665  exbtwnz  10666  rebtwn2zlemstep  10668  rebtwn2zlemshrink  10669  rebtwn2z  10670  flqlelt  10692  flqbi  10706  fldiv4p1lem1div2  10721  fldiv4lem1div2  10723  modqval  10742  modqadd1  10779  modqmuladd  10784  modqmuladdnn0  10786  modqm1p1mod0  10793  modqmul1  10795  modfzo0difsn  10813  addmodlteq  10816  frec2uzzd  10818  frec2uzsucd  10819  frec2uzrand  10823  frecuzrdgrrn  10826  frec2uzrdg  10827  frecuzrdgrcl  10828  frecuzrdgsuc  10832  frecuzrdgrclt  10833  frecuzrdgg  10834  frecuzrdgdom  10836  frecuzrdgfun  10838  frecuzrdgsuctlem  10841  frecuzrdgsuct  10842  uzsinds  10862  iseqvalcbv  10877  seq3val  10878  seqvalcd  10879  seqf  10882  seq3p1  10883  seqovcd  10885  seqp1cd  10888  seq3fveq2  10893  seqfveq2g  10895  seq3shft2  10899  seqshft2g  10900  monoord  10903  monoord2  10904  seq3split  10906  seqsplitg  10907  seq3caopr3  10909  seqcaopr3g  10910  seq3caopr2  10911  seqcaopr2g  10912  iseqf1olemqval  10918  iseqf1olemqk  10925  seqf1oglem2a  10936  seqf1oglem2  10938  seq3id2  10944  seq3homo  10945  seq3z  10946  seqhomog  10948  seqfeq4g  10949  seq3distr  10950  m1expcl2  10979  mulexp  10996  expadd  10999  expmul  11002  sq0i  11049  qsqeqor  11068  resq01  11076  sqoddm1div8  11112  facp1  11149  faclbnd  11160  faclbnd3  11162  bcval  11168  bcn1  11177  bcval5  11182  bcpasc  11185  bccl  11186  hashfz1  11203  omgadd  11223  hashfzo  11244  hashfzp1  11246  hashxp  11248  hashmap  11249  hashf1lem2  11267  seq3coll  11275  lsw1  11335  ccats1val2  11389  ccatw2s1p2  11395  pfxsuff1eqwrdeq  11452  swrdswrd  11458  ccats1pfxeq  11467  ccatopth  11469  wrdind  11475  wrd2ind  11476  swrdccatin2  11482  pfxccatin12lem2  11484  swrdccat3blem  11492  ccats1pfxeqbi  11495  swrdccatin2d  11497  reuccatpfxs1  11500  shftlem  11562  shftfvalg  11564  shftfibg  11566  shftfval  11567  shftfib  11569  shftfn  11570  shftf  11576  2shfti  11577  shftvalg  11582  shftval4g  11583  cjval  11591  imval  11596  cjexp  11639  sq01  11641  cnrecnv  11657  cvg1nlemcau  11731  cvg1nlemres  11732  resqrexlemcalc3  11763  resqrexlemex  11772  rsqrmo  11774  resqrtcl  11776  rersqrtthlem  11777  sqrtsq  11791  absexp  11826  recan  11856  climshft  12051  climcn1  12055  climcn2  12056  subcn2  12058  fsumshft  12192  fisum0diag2  12195  fsumiun  12225  binomlem  12231  binom  12232  bcxmas  12237  isumsplit  12239  arisum2  12247  trireciplem  12248  trirecip  12249  geolim  12259  cvgratnnlemnexp  12272  cvgratnnlemmn  12273  clim2prod  12287  prodfrecap  12294  fprodcl2lem  12353  fprodfac  12363  fprodshft  12366  ef0lem  12408  efval  12409  efne0  12426  efexp  12430  demoivreALT  12522  dvdsval2  12538  p1modz1  12542  dvds0lem  12549  dvds1lem  12550  dvds2lem  12551  dvdsmulc  12567  divconjdvds  12597  odd2np1lem  12620  odd2np1  12621  ltoddhalfle  12641  halfleoddlt  12642  nn0o1gt2  12653  nn0o  12655  divalglemnn  12666  divalglemeunn  12669  divalglemex  12670  divalglemeuneg  12671  flodddiv4  12684  bitsinv1  12710  gcdabs1  12747  gcddiv  12777  dvdssqim  12782  rpmulgcd  12784  bezoutr1  12791  uzwodc  12795  dvdslcm  12828  lcmeq0  12830  lcmdvds  12838  divgcdcoprm0  12860  prmind2  12879  isprm5lem  12900  isprm6  12906  rpexp  12912  sqrt2irr  12921  pw2dvdslemn  12924  pw2dvdseu  12927  oddpwdclemxy  12928  nn0gcdsq  12959  phicl2  12973  phibndlem  12975  hashdvds  12980  crth  12983  phimullem  12984  eulerthlem1  12986  eulerthlemfi  12987  eulerthlemrprm  12988  eulerthlemth  12991  eulerth  12992  hashgcdlem  12997  phisum  13000  odzval  13001  modprm0  13014  nnnn0modprm0  13015  pythagtriplem1  13025  pythagtriplem6  13030  pythagtriplem7  13031  pythagtriplem12  13035  pythagtriplem14  13037  pythagtriplem18  13041  pythagtriplem19  13042  pceulem  13054  pceu  13055  pcval  13056  pczpre  13057  pcdiv  13062  pcqmul  13063  pcqcl  13066  pcexp  13069  pcaddlem  13099  pcadd  13100  pcmpt  13103  pcprod  13106  pcfac  13110  expnprm  13113  prmpwdvds  13115  pockthi  13118  1arithlem2  13124  4sqlem2  13149  4sqlem3  13150  4sqlem11  13161  4sqlem12  13162  4sqlem13m  13163  4sqlem17  13167  4sqlem18  13168  4sqlem19  13169  ballotfilemfc0  13213  ballotfilemfcc  13214  ennnfonelemr  13295  ctinfom  13300  infpn2  13328  ercpbl  13632  mgm1  13670  mgmidmo  13672  ismgmid  13677  mgmlrid  13679  ismgmid2  13680  lidrideqd  13681  lidrididd  13682  mgmidsssn0  13684  grprida  13687  gzsumfzval  13691  gzsumress  13692  gzsumval2  13694  isnsgrp  13701  sgrpass  13703  sgrp1  13706  sgrpidmndm  13713  ismndd  13730  mndinvmod  13738  imasmnd2  13739  mnd1  13742  mnd1id  13743  mhmpropd  13753  insubm  13772  mhmima  13778  gsumvallem2  13780  grppropd  13802  isgrpd2  13806  isgrpd  13808  dfgrp2  13812  grprcan  13822  grpinveu  13823  grpsubval  13831  grplinv  13835  grpinvid2  13838  isgrpinv  13839  grplrinv  13842  grpidinv2  13843  grpidinv  13844  grpidssd  13861  grpinvssd  13862  dfgrp3mlem  13883  dfgrp3m  13884  grplactfval  13886  grp1  13891  imasgrp2  13893  mhmmnd  13899  ghmgrp  13901  mulgnn0gzsum  13911  mulgnn0p1  13916  mulgnn0subcl  13918  mulgaddcom  13929  mulginvcom  13930  mulgnn0z  13932  mulgneg2  13939  mulgnnass  13940  mulgnn0ass  13941  mhmmulg  13946  issubg  13956  subgex  13959  issubg2m  13972  issubg4m  13976  isnsg2  13986  nsgbi  13987  isnsg3  13990  elnmz  13991  nmzbi  13992  ghmrn  14040  ghmnsgima  14051  gzsumconst  14123  gzsumshift  14129  gsumvalfi  14132  rngdi  14217  rngdir  14218  srgrz  14265  srgmulgass  14270  srgpcomp  14271  srgrmhm  14275  ringid  14307  ringinvnzdiv  14331  mulgass2  14339  ring1  14340  ringrghm  14343  imasring  14345  dvdsrmuld  14379  dvdsrmul1  14385  dvdsr01  14387  dvreq1  14425  rhmdvdsr  14458  lringuplu  14479  issubrng  14483  issubrng2  14494  issubrg  14505  issubrg2  14525  isrrg  14547  domneq0  14557  lmodlema  14604  islmodd  14605  lmodvsmmulgdi  14635  rmodislmodlem  14662  rmodislmod  14663  lssclg  14676  lss1d  14695  lspsn  14728  sraval  14749  rnglidlmcl  14792  quscrng  14845  cnfldmulg  14888  cnfldexp  14889  gsumfsum  14898  cnfldui  14899  expghmap  14917  mulgghm2  14918  mulgrhm  14919  zrhmulg  14930  zlmval  14937  znunit  14969  cnmptcom  15325  psmettri2  15355  isxmet2d  15375  xmeteq0  15386  xmettri2  15388  metrest  15533  mpomulcn  15593  expcn  15596  cncfval  15599  mulc1cncf  15616  addccncf  15627  mulcncf  15635  expcncf  15636  hovera  15674  hoverb  15675  hoverlt1  15676  hovergt0  15677  ivthdich  15680  limccnp2lem  15703  dvcnp2cntop  15726  dvcoapbr  15734  dvexp  15738  dvrecap  15740  dvef  15754  plyadd  15778  plymul  15779  plycoeid3  15784  plyco  15786  plycjlemc  15787  plycj  15788  plyrecj  15790  dvply1  15792  dvply2g  15793  sincn  15796  coscn  15797  ptolemy  15851  sincosq1eq  15866  rpcxpmul2  15941  logbgcd1irr  15995  logbgcd1irraplemexp  15996  2irrexpq  16004  2irrexpqap  16006  pellexlem3  16010  mpodvdsmulf1o  16021  fsumdvdsmul  16022  sgmppw  16023  sgmmul  16027  perfect  16032  lgslem4  16039  lgsval  16040  lgsfvalg  16041  lgsval2lem  16046  lgsdir2lem4  16067  lgsdir  16071  lgsdilem2  16072  lgsdi  16073  lgsne0  16074  lgsmodeq  16081  lgsdirnn0  16083  lgsdinn0  16084  gausslemma2dlem0i  16093  gausslemma2dlem1a  16094  gausslemma2dlem1f1o  16096  gausslemma2dlem2  16098  gausslemma2dlem3  16099  gausslemma2dlem4  16100  lgseisenlem2  16107  lgsquadlem2  16114  lgsquadlem3  16115  lgsquad  16116  lgsquad2lem2  16118  2lgslem1a  16124  2lgslem1b  16125  2lgslem1c  16126  2lgslem3a  16129  2lgslem3b  16130  2lgslem3c  16131  2lgslem3d  16132  2lgslem3a1  16133  2lgslem3b1  16134  2lgslem3c1  16135  2lgslem3d1  16136  2lgs  16140  2lgsoddprmlem1  16141  2lgsoddprmlem3  16147  2sqlem2  16151  2sqlem6  16156  2sqlem8  16159  2sqlem9  16160  wlklenvm1  16499  wlklenvm1g  16500  wlkl1loop  16516  2wlklem  16534  clwwlknnn  16570  clwwlknp  16575  clwwlkn1  16576  clwwlkn2  16579  clwwlkext2edg  16580  umgr2cwwk2dif  16582  clwwlknon  16587  clwwlk0on0  16589  clwwlknonex2lem1  16595  clwwlknonex2lem2  16596  clwwlknonex2  16597  qdencn  16980  isomninn  16988  trirec0  17001  iswomninn  17008  ismkvnn  17011