Theorem oveq1 6020

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 3860	. . 3 ⊢ (𝐴 = 𝐵 → ⟨𝐴, 𝐶⟩ = ⟨𝐵, 𝐶⟩)
2	1	fveq2d 5639	. 2 ⊢ (𝐴 = 𝐵 → (𝐹‘⟨𝐴, 𝐶⟩) = (𝐹‘⟨𝐵, 𝐶⟩))
3		df-ov 6016	. 2 ⊢ (𝐴𝐹𝐶) = (𝐹‘⟨𝐴, 𝐶⟩)
4		df-ov 6016	. 2 ⊢ (𝐵𝐹𝐶) = (𝐹‘⟨𝐵, 𝐶⟩)
5	2, 3, 4	3eqtr4g 2287	1 ⊢ (𝐴 = 𝐵 → (𝐴𝐹𝐶) = (𝐵𝐹𝐶))

Syntax hints:   → wi 4   = wceq 1395  ⟨cop 3670  ‘cfv 5324  (class class class)co 6013

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 714  ax-5 1493  ax-7 1494  ax-gen 1495  ax-ie1 1539  ax-ie2 1540  ax-8 1550  ax-10 1551  ax-11 1552  ax-i12 1553  ax-bndl 1555  ax-4 1556  ax-17 1572  ax-i9 1576  ax-ial 1580  ax-i5r 1581  ax-ext 2211

This theorem depends on definitions:  df-bi 117  df-3an 1004  df-tru 1398  df-nf 1507  df-sb 1809  df-clab 2216  df-cleq 2222  df-clel 2225  df-nfc 2361  df-rex 2514  df-v 2802  df-un 3202  df-sn 3673  df-pr 3674  df-op 3676  df-uni 3892  df-br 4087  df-iota 5284  df-fv 5332  df-ov 6016

This theorem is referenced by:  oveq12  6022  oveq1i  6023  oveq1d  6028  ovrspc2v  6039  oveqrspc2v  6040  rspceov  6056  fovcld  6121  ovmpos  6140  ov2gf  6141  ovi3  6154  caovclg  6170  caovcomg  6173  caovassg  6176  caovcang  6179  caovcan  6182  caovordig  6183  caovordg  6185  caovord  6189  caovdig  6192  caovdirg  6195  caovimo  6211  suppssov1  6227  off  6243  caofid0r  6258  caofid1  6259  caofdig  6264  omcl  6624  oeicl  6625  omv2  6628  nnm0r  6642  nnacom  6647  nndi  6649  nnmass  6650  nnmsucr  6651  nnmcom  6652  nnaword  6674  nnmord  6680  nnm00  6693  eroveu  6790  th3qlem2  6802  th3q  6804  ecovcom  6806  ecovicom  6807  ecovass  6808  ecoviass  6809  ecovdi  6810  ecovidi  6811  map0g  6852  addcmpblnq  7577  addclnq  7585  mulclnq  7586  mulidnq  7599  recexnq  7600  recmulnqg  7601  ltanqg  7610  ltmnqg  7611  ltexnqq  7618  enq0ref  7643  enq0tr  7644  addcmpblnq0  7653  mulnnnq0  7660  addclnq0  7661  mulclnq0  7662  distrnq0  7669  mulcomnq0  7670  addassnq0  7672  prarloclemlo  7704  prarloclem3  7707  prarloclem5  7710  prarloclemcalc  7712  genipv  7719  genpassl  7734  genpassu  7735  addlocprlemeq  7743  distrlem4prl  7794  distrlem4pru  7795  ltexprlemdisj  7816  ltexprlemloc  7817  ltexprlemrl  7820  ltexprlemru  7822  prplnqu  7830  cauappcvgprlemm  7855  cauappcvgprlemopl  7856  cauappcvgprlemlol  7857  cauappcvgprlemdisj  7861  cauappcvgprlemloc  7862  cauappcvgprlemladdfl  7865  cauappcvgprlemladdru  7866  cauappcvgprlemladdrl  7867  cauappcvgprlem1  7869  cauappcvgprlemlim  7871  cauappcvgpr  7872  caucvgprlemm  7878  caucvgprlemopl  7879  caucvgprlemlol  7880  caucvgprlemdisj  7884  caucvgprlemloc  7885  caucvgprlemladdrl  7888  caucvgprlem1  7889  caucvgpr  7892  caucvgprprlemell  7895  caucvgprprlemml  7904  caucvgprpr  7922  mulcmpblnrlemg  7950  addclsr  7963  mulclsr  7964  0idsr  7977  1idsr  7978  00sr  7979  ltasrg  7980  recexgt0sr  7983  mulgt0sr  7988  mulextsr1  7991  prsrriota  7998  caucvgsrlemgt1  8005  caucvgsrlemoffres  8010  pitonn  8058  peano2nnnn  8063  axaddrcl  8075  axmulrcl  8077  axaddcom  8080  ax1rid  8087  ax0id  8088  axprecex  8090  axcnre  8091  axpre-ltadd  8096  axpre-mulgt0  8097  axpre-mulext  8098  rereceu  8099  peano5nnnn  8102  axcaucvglemcau  8108  axcaucvglemres  8109  mulrid  8166  cnegexlem1  8344  cnegexlem2  8345  cnegex  8347  addcan2  8350  subval  8361  addlsub  8539  apreim  8773  recexap  8823  receuap  8839  divvalap  8844  cju  9131  peano2nn  9145  nn1m1nn  9151  nn1suc  9152  nnsub  9172  fv0p1e1  9248  nnm1nn0  9433  zdiv  9558  zneo  9571  nneoor  9572  zeo  9575  peano5uzti  9578  nn0ind-raph  9587  uzind4s  9814  uzind4s2  9815  qmulz  9847  elpq  9873  cnref1o  9875  nn0ledivnn  9992  xaddnemnf  10082  xaddnepnf  10083  xaddcom  10086  xaddid1  10087  xnn0xadd0  10092  xaddass  10094  xpncan  10096  xleadd1a  10098  xltadd1  10101  xlt2add  10105  xsubge0  10106  xposdif  10107  xlesubadd  10108  xleaddadd  10112  fzsuc2  10304  fzm1  10325  fzoval  10373  exbtwnzlemstep  10497  exbtwnzlemshrink  10498  exbtwnzlemex  10499  exbtwnz  10500  rebtwn2zlemstep  10502  rebtwn2zlemshrink  10503  rebtwn2z  10504  flqlelt  10526  flqbi  10540  fldiv4p1lem1div2  10555  fldiv4lem1div2  10557  modqval  10576  modqadd1  10613  modqmuladd  10618  modqmuladdnn0  10620  modqm1p1mod0  10627  modqmul1  10629  modfzo0difsn  10647  addmodlteq  10650  frec2uzzd  10652  frec2uzsucd  10653  frec2uzrand  10657  frecuzrdgrrn  10660  frec2uzrdg  10661  frecuzrdgrcl  10662  frecuzrdgsuc  10666  frecuzrdgrclt  10667  frecuzrdgg  10668  frecuzrdgdom  10670  frecuzrdgfun  10672  frecuzrdgsuctlem  10675  frecuzrdgsuct  10676  uzsinds  10696  iseqvalcbv  10711  seq3val  10712  seqvalcd  10713  seqf  10716  seq3p1  10717  seqovcd  10719  seqp1cd  10722  seq3fveq2  10727  seqfveq2g  10729  seq3shft2  10733  seqshft2g  10734  monoord  10737  monoord2  10738  seq3split  10740  seqsplitg  10741  seq3caopr3  10743  seqcaopr3g  10744  seq3caopr2  10745  seqcaopr2g  10746  iseqf1olemqval  10752  iseqf1olemqk  10759  seqf1oglem2a  10770  seqf1oglem2  10772  seq3id2  10778  seq3homo  10779  seq3z  10780  seqhomog  10782  seqfeq4g  10783  seq3distr  10784  m1expcl2  10813  mulexp  10830  expadd  10833  expmul  10836  sq0i  10883  qsqeqor  10902  sqoddm1div8  10945  facp1  10982  faclbnd  10993  faclbnd3  10995  bcval  11001  bcn1  11010  bcval5  11015  bcpasc  11018  bccl  11019  hashfz1  11035  omgadd  11055  hashfzo  11076  hashfzp1  11078  hashxp  11080  seq3coll  11096  lsw1  11153  ccats1val2  11207  ccatw2s1p2  11213  pfxsuff1eqwrdeq  11270  swrdswrd  11276  ccats1pfxeq  11285  ccatopth  11287  wrdind  11293  wrd2ind  11294  swrdccatin2  11300  pfxccatin12lem2  11302  swrdccat3blem  11310  ccats1pfxeqbi  11313  swrdccatin2d  11315  reuccatpfxs1  11318  shftlem  11367  shftfvalg  11369  shftfibg  11371  shftfval  11372  shftfib  11374  shftfn  11375  shftf  11381  2shfti  11382  shftvalg  11387  shftval4g  11388  cjval  11396  imval  11401  cjexp  11444  cnrecnv  11461  cvg1nlemcau  11535  cvg1nlemres  11536  resqrexlemcalc3  11567  resqrexlemex  11576  rsqrmo  11578  resqrtcl  11580  rersqrtthlem  11581  sqrtsq  11595  absexp  11630  recan  11660  climshft  11855  climcn1  11859  climcn2  11860  subcn2  11862  fsumshft  11995  fisum0diag2  11998  fsumiun  12028  binomlem  12034  binom  12035  bcxmas  12040  isumsplit  12042  arisum2  12050  trireciplem  12051  trirecip  12052  geolim  12062  cvgratnnlemnexp  12075  cvgratnnlemmn  12076  clim2prod  12090  prodfrecap  12097  fprodcl2lem  12156  fprodfac  12166  fprodshft  12169  ef0lem  12211  efval  12212  efne0  12229  efexp  12233  demoivreALT  12325  dvdsval2  12341  p1modz1  12345  dvds0lem  12352  dvds1lem  12353  dvds2lem  12354  dvdsmulc  12370  divconjdvds  12400  odd2np1lem  12423  odd2np1  12424  ltoddhalfle  12444  halfleoddlt  12445  nn0o1gt2  12456  nn0o  12458  divalglemnn  12469  divalglemeunn  12472  divalglemex  12473  divalglemeuneg  12474  flodddiv4  12487  bitsinv1  12513  gcdabs1  12550  gcddiv  12580  dvdssqim  12585  rpmulgcd  12587  bezoutr1  12594  uzwodc  12598  dvdslcm  12631  lcmeq0  12633  lcmdvds  12641  divgcdcoprm0  12663  prmind2  12682  isprm5lem  12703  isprm6  12709  rpexp  12715  sqrt2irr  12724  pw2dvdslemn  12727  pw2dvdseu  12730  oddpwdclemxy  12731  nn0gcdsq  12762  phicl2  12776  phibndlem  12778  hashdvds  12783  crth  12786  phimullem  12787  eulerthlem1  12789  eulerthlemfi  12790  eulerthlemrprm  12791  eulerthlemth  12794  eulerth  12795  hashgcdlem  12800  phisum  12803  odzval  12804  modprm0  12817  nnnn0modprm0  12818  pythagtriplem1  12828  pythagtriplem6  12833  pythagtriplem7  12834  pythagtriplem12  12838  pythagtriplem14  12840  pythagtriplem18  12844  pythagtriplem19  12845  pceulem  12857  pceu  12858  pcval  12859  pczpre  12860  pcdiv  12865  pcqmul  12866  pcqcl  12869  pcexp  12872  pcaddlem  12902  pcadd  12903  pcmpt  12906  pcprod  12909  pcfac  12913  expnprm  12916  prmpwdvds  12918  pockthi  12921  1arithlem2  12927  4sqlem2  12952  4sqlem3  12953  4sqlem11  12964  4sqlem12  12965  4sqlem13m  12966  4sqlem17  12970  4sqlem18  12971  4sqlem19  12972  ennnfonelemr  13034  ctinfom  13039  infpn2  13067  ercpbl  13404  mgm1  13443  mgmidmo  13445  ismgmid  13450  mgmlrid  13452  ismgmid2  13453  lidrideqd  13454  lidrididd  13455  mgmidsssn0  13457  grprida  13460  gsumfzval  13464  gsumress  13468  gsumval2  13470  isnsgrp  13479  sgrpass  13481  sgrp1  13484  sgrpidmndm  13493  ismndd  13510  mndinvmod  13518  imasmnd2  13525  mnd1  13528  mnd1id  13529  mhmpropd  13539  insubm  13558  mhmima  13564  gsumvallem2  13566  grppropd  13590  isgrpd2  13594  isgrpd  13596  dfgrp2  13600  grprcan  13610  grpinveu  13611  grpsubval  13619  grplinv  13623  grpinvid2  13626  isgrpinv  13627  grplrinv  13630  grpidinv2  13631  grpidinv  13632  grpidssd  13649  grpinvssd  13650  dfgrp3mlem  13671  dfgrp3m  13672  grplactfval  13674  grp1  13679  imasgrp2  13687  mhmmnd  13693  ghmgrp  13695  mulgnn0gsum  13705  mulgnn0p1  13710  mulgnn0subcl  13712  mulgaddcom  13723  mulginvcom  13724  mulgnn0z  13726  mulgneg2  13733  mulgnnass  13734  mulgnn0ass  13735  mhmmulg  13740  issubg  13750  subgex  13753  issubg2m  13766  issubg4m  13770  isnsg2  13780  nsgbi  13781  isnsg3  13784  elnmz  13785  nmzbi  13786  ghmrn  13834  ghmnsgima  13845  gsumfzconst  13918  rngdi  13943  rngdir  13944  srgrz  13987  srgmulgass  13992  srgpcomp  13993  srgrmhm  13997  ringid  14029  ringinvnzdiv  14053  mulgass2  14061  ring1  14062  ringrghm  14065  imasring  14067  dvdsrmuld  14100  dvdsrmul1  14106  dvdsr01  14108  dvreq1  14146  rhmdvdsr  14179  lringuplu  14200  issubrng  14203  issubrng2  14214  issubrg  14225  issubrg2  14245  isrrg  14267  domneq0  14276  lmodlema  14296  islmodd  14297  lmodvsmmulgdi  14327  rmodislmodlem  14354  rmodislmod  14355  lssclg  14368  lss1d  14387  lspsn  14420  sraval  14441  rnglidlmcl  14484  quscrng  14537  cnfldmulg  14580  cnfldexp  14581  gsumfzfsumlemm  14591  cnfldui  14593  expghmap  14611  mulgghm2  14612  mulgrhm  14613  zrhmulg  14624  zlmval  14631  znunit  14663  cnmptcom  15012  psmettri2  15042  isxmet2d  15062  xmeteq0  15073  xmettri2  15075  metrest  15220  mpomulcn  15280  expcn  15283  cncfval  15286  mulc1cncf  15303  addccncf  15314  mulcncf  15322  expcncf  15323  hovera  15361  hoverb  15362  hoverlt1  15363  hovergt0  15364  ivthdich  15367  limccnp2lem  15390  dvcnp2cntop  15413  dvcoapbr  15421  dvexp  15425  dvrecap  15427  dvef  15441  plyadd  15465  plymul  15466  plycoeid3  15471  plyco  15473  plycjlemc  15474  plycj  15475  plyrecj  15477  dvply1  15479  dvply2g  15480  sincn  15483  coscn  15484  ptolemy  15538  sincosq1eq  15553  rpcxpmul2  15627  logbgcd1irr  15681  logbgcd1irraplemexp  15682  2irrexpq  15690  2irrexpqap  15692  mpodvdsmulf1o  15704  fsumdvdsmul  15705  sgmppw  15706  sgmmul  15710  perfect  15715  lgslem4  15722  lgsval  15723  lgsfvalg  15724  lgsval2lem  15729  lgsdir2lem4  15750  lgsdir  15754  lgsdilem2  15755  lgsdi  15756  lgsne0  15757  lgsmodeq  15764  lgsdirnn0  15766  lgsdinn0  15767  gausslemma2dlem0i  15776  gausslemma2dlem1a  15777  gausslemma2dlem1f1o  15779  gausslemma2dlem2  15781  gausslemma2dlem3  15782  gausslemma2dlem4  15783  lgseisenlem2  15790  lgsquadlem2  15797  lgsquadlem3  15798  lgsquad  15799  lgsquad2lem2  15801  2lgslem1a  15807  2lgslem1b  15808  2lgslem1c  15809  2lgslem3a  15812  2lgslem3b  15813  2lgslem3c  15814  2lgslem3d  15815  2lgslem3a1  15816  2lgslem3b1  15817  2lgslem3c1  15818  2lgslem3d1  15819  2lgs  15823  2lgsoddprmlem1  15824  2lgsoddprmlem3  15830  2sqlem2  15834  2sqlem6  15839  2sqlem8  15842  2sqlem9  15843  wlklenvm1  16138  wlklenvm1g  16139  wlkl1loop  16155  2wlklem  16171  clwwlknnn  16207  clwwlknp  16212  clwwlkn1  16213  clwwlkn2  16216  clwwlkext2edg  16217  umgr2cwwk2dif  16219  clwwlknon  16224  clwwlk0on0  16226  clwwlknonex2lem1  16232  clwwlknonex2lem2  16233  clwwlknonex2  16234  qdencn  16567  isomninn  16571  trirec0  16584  iswomninn  16590  ismkvnn  16593