Theorem oveq1 6092

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

This proof depends on syntax axioms:   → wi 4   = wceq 1402  ⟨cop 3712  ‘cfv 5377  (class class class)co 6085

This proof depends on 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 proof 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 3715  df-pr 3716  df-op 3718  df-uni 3936  df-br 4131  df-iota 5337  df-fv 5385  df-ov 6088

This theorem is used by:  oveq12  6094  oveq1i  6095  oveq1d  6100  ovrspc2v  6111  oveqrspc2v  6112  rspceov  6128  fovcld  6193  ovmpos  6212  ov2gf  6213  ovi3  6226  caovclg  6242  caovcomg  6245  caovassg  6248  caovcang  6251  caovcan  6254  caovordig  6255  caovordg  6257  caovord  6261  caovdig  6264  caovdirg  6267  caovimo  6283  suppssov1  6299  off  6315  caofid0r  6330  caofid1  6331  caofdig  6336  suppofss1dcl  6504  suppofss2dcl  6505  omcl  6734  oeicl  6735  omv2  6738  nnm0r  6752  nnacom  6757  nndi  6759  nnmass  6760  nnmsucr  6761  nnmcom  6762  nnaword  6784  nnmord  6790  nnm00  6803  eroveu  6900  th3qlem2  6912  th3q  6914  ecovcom  6916  ecovicom  6917  ecovass  6918  ecoviass  6919  ecovdi  6920  ecovidi  6921  map0g  6969  addcmpblnq  7735  addclnq  7743  mulclnq  7744  mulidnq  7757  recexnq  7758  recmulnqg  7759  ltanqg  7768  ltmnqg  7769  ltexnqq  7776  enq0ref  7801  enq0tr  7802  addcmpblnq0  7811  mulnnnq0  7818  addclnq0  7819  mulclnq0  7820  distrnq0  7827  mulcomnq0  7828  addassnq0  7830  prarloclemlo  7862  prarloclem3  7865  prarloclem5  7868  prarloclemcalc  7870  genipv  7877  genpassl  7892  genpassu  7893  addlocprlemeq  7901  distrlem4prl  7952  distrlem4pru  7953  ltexprlemdisj  7974  ltexprlemloc  7975  ltexprlemrl  7978  ltexprlemru  7980  prplnqu  7988  cauappcvgprlemm  8013  cauappcvgprlemopl  8014  cauappcvgprlemlol  8015  cauappcvgprlemdisj  8019  cauappcvgprlemloc  8020  cauappcvgprlemladdfl  8023  cauappcvgprlemladdru  8024  cauappcvgprlemladdrl  8025  cauappcvgprlem1  8027  cauappcvgprlemlim  8029  cauappcvgpr  8030  caucvgprlemm  8036  caucvgprlemopl  8037  caucvgprlemlol  8038  caucvgprlemdisj  8042  caucvgprlemloc  8043  caucvgprlemladdrl  8046  caucvgprlem1  8047  caucvgpr  8050  caucvgprprlemell  8053  caucvgprprlemml  8062  caucvgprpr  8080  mulcmpblnrlemg  8108  addclsr  8121  mulclsr  8122  0idsr  8135  1idsr  8136  00sr  8137  ltasrg  8138  recexgt0sr  8141  mulgt0sr  8146  mulextsr1  8149  prsrriota  8156  caucvgsrlemgt1  8163  caucvgsrlemoffres  8168  pitonn  8216  peano2nnnn  8221  axaddrcl  8233  axmulrcl  8235  axaddcom  8238  ax1rid  8245  ax0id  8246  axprecex  8248  axcnre  8249  axpre-ltadd  8254  axpre-mulgt0  8255  axpre-mulext  8256  rereceu  8257  peano5nnnn  8260  axcaucvglemcau  8266  axcaucvglemres  8267  mulrid  8324  cnegexlem1  8503  cnegexlem2  8504  cnegex  8506  addcan2  8509  subval  8520  addlsub  8698  apreim  8934  recexap  8984  receuap  9002  divvalap  9007  cju  9294  peano2nn  9319  nn1m1nn  9325  nn1suc  9326  nnsub  9346  fv0p1e1  9422  nnm1nn0  9609  zdiv  9739  zneo  9752  nneoor  9753  zeo  9756  peano5uzti  9759  nn0ind-raph  9768  uzind4s  10000  uzind4s2  10001  qmulz  10033  elpq  10060  cnref1o  10062  nn0ledivnn  10179  xaddnemnf  10270  xaddnepnf  10271  xaddcom  10274  xaddid1  10275  xnn0xadd0  10280  xaddass  10282  xpncan  10284  xleadd1a  10286  xltadd1  10289  xlt2add  10293  xsubge0  10294  xposdif  10295  xlesubadd  10296  xleaddadd  10300  fzsuc2  10497  fzm1  10518  fzoval  10566  exbtwnzlemstep  10693  exbtwnzlemshrink  10694  exbtwnzlemex  10695  exbtwnz  10696  rebtwn2zlemstep  10698  rebtwn2zlemshrink  10699  rebtwn2z  10700  flqlelt  10723  flaplelt  10724  flqbi  10740  fldiv4p1lem1div2  10755  fldiv4lem1div2  10757  modqval  10776  modqadd1  10813  modqmuladd  10818  modqmuladdnn0  10820  modqm1p1mod0  10827  modqmul1  10829  modfzo0difsn  10847  addmodlteq  10850  frec2uzzd  10852  frec2uzsucd  10853  frec2uzrand  10857  frecuzrdgrrn  10860  frec2uzrdg  10861  frecuzrdgrcl  10862  frecuzrdgsuc  10866  frecuzrdgrclt  10867  frecuzrdgg  10868  frecuzrdgdom  10870  frecuzrdgfun  10872  frecuzrdgsuctlem  10875  frecuzrdgsuct  10876  uzsinds  10896  iseqvalcbv  10911  seq3val  10912  seqvalcd  10913  seqf  10916  seq3p1  10917  seqovcd  10919  seqp1cd  10922  seq3fveq2  10927  seqfveq2g  10929  seq3shft2  10933  seqshft2g  10934  monoord  10937  monoord2  10938  seq3split  10940  seqsplitg  10941  seq3caopr3  10943  seqcaopr3g  10944  seq3caopr2  10945  seqcaopr2g  10946  iseqf1olemqval  10952  iseqf1olemqk  10959  seqf1oglem2a  10970  seqf1oglem2  10972  seq3id2  10978  seq3homo  10979  seq3z  10980  seqhomog  10982  seqfeq4g  10983  seq3distr  10984  m1expcl2  11013  mulexp  11030  expadd  11033  expmul  11036  sq0i  11083  qsqeqor  11102  resq01  11110  sqoddm1div8  11146  facp1  11184  faclbnd  11195  faclbnd3  11197  bcval  11203  bcn1  11212  bcval5  11217  bcpasc  11220  bccl  11221  hashfz1  11238  omgadd  11258  hashfzo  11279  hashfzp1  11281  hashxp  11283  hashmap  11284  hashf1lem2  11302  seq3coll  11310  lsw1  11370  ccats1val2  11424  ccatw2s1p2  11430  pfxsuff1eqwrdeq  11487  swrdswrd  11493  ccats1pfxeq  11502  ccatopth  11504  wrdind  11510  wrd2ind  11511  swrdccatin2  11517  pfxccatin12lem2  11519  swrdccat3blem  11527  ccats1pfxeqbi  11530  swrdccatin2d  11532  reuccatpfxs1  11535  shftlem  11597  shftfvalg  11599  shftfibg  11601  shftfval  11602  shftfib  11604  shftfn  11605  shftf  11611  2shfti  11612  shftvalg  11617  shftval4g  11618  cjval  11626  imval  11631  cjexp  11674  sq01  11676  cnrecnv  11692  cvg1nlemcau  11766  cvg1nlemres  11767  resqrexlemcalc3  11798  resqrexlemex  11807  rsqrmo  11809  resqrtcl  11811  rersqrtthlem  11812  sqrtsq  11826  absexp  11862  recan  11892  climshft  12089  climcn1  12093  climcn2  12094  subcn2  12096  fsumshft  12230  fisum0diag2  12233  fsumiun  12263  binomlem  12269  binom  12270  bcxmas  12275  isumsplit  12277  arisum2  12285  trireciplem  12286  trirecip  12287  geolim  12297  cvgratnnlemnexp  12310  cvgratnnlemmn  12311  clim2prod  12325  prodfrecap  12332  fprodcl2lem  12391  fprodfac  12401  fprodshft  12404  ef0lem  12446  efval  12447  efne0  12464  efexp  12468  demoivreALT  12560  dvdsval2  12576  p1modz1  12580  dvds0lem  12587  dvds1lem  12588  dvds2lem  12589  dvdsmulc  12605  divconjdvds  12635  odd2np1lem  12658  odd2np1  12659  ltoddhalfle  12679  halfleoddlt  12680  nn0o1gt2  12691  nn0o  12693  divalglemnn  12704  divalglemeunn  12707  divalglemex  12708  divalglemeuneg  12709  flodddiv4  12722  bitsinv1  12748  gcdabs1  12785  gcddiv  12815  dvdssqim  12820  rpmulgcd  12822  bezoutr1  12829  uzwodc  12833  dvdslcm  12866  lcmeq0  12868  lcmdvds  12876  divgcdcoprm0  12898  prmind2  12917  isprm5lem  12939  isprm6  12945  rpexp  12951  sqrt2irr  12960  pwbdvdslemn  12963  pwbdvdseu  12966  nnmaxpwlemxy  12967  nn0gcdsq  12999  nn0sqdcq  13007  phicl2  13015  phibndlem  13017  hashdvds  13022  crth  13025  phimullem  13026  eulerthlem1  13028  eulerthlemfi  13029  eulerthlemrprm  13030  eulerthlemth  13033  eulerth  13034  hashgcdlem  13039  phisum  13042  odzval  13043  modprm0  13056  nnnn0modprm0  13057  pythagtriplem1  13067  pythagtriplem6  13072  pythagtriplem7  13073  pythagtriplem12  13077  pythagtriplem14  13079  pythagtriplem18  13083  pythagtriplem19  13084  pceulem  13096  pceu  13097  pcval  13098  pczpre  13099  pcdiv  13104  pcqmul  13105  pcqcl  13108  pcexp  13111  pcaddlem  13141  pcadd  13142  pcmpt  13145  pcprod  13148  pcfac  13152  expnprm  13155  prmpwdvds  13157  pockthi  13160  1arithlem2  13166  4sqlem2  13191  4sqlem3  13192  4sqlem11  13203  4sqlem12  13204  4sqlem13m  13205  4sqlem17  13209  4sqlem18  13210  4sqlem19  13211  ballotfilemfc0  13284  ballotfilemfcc  13285  ennnfonelemr  13366  ctinfom  13371  infpn2  13399  ercpbl  13705  mgm1  13743  mgmidmo  13745  ismgmid  13750  mgmlrid  13752  ismgmid2  13753  lidrideqd  13754  lidrididd  13755  mgmidsssn0  13757  grprida  13760  gzsumfzval  13764  gzsumress  13765  gzsumval2  13767  isnsgrp  13774  sgrpass  13776  sgrp1  13779  sgrpidmndm  13786  ismndd  13803  mndinvmod  13811  imasmnd2  13812  mnd1  13815  mnd1id  13816  mhmpropd  13826  insubm  13845  mhmima  13851  gsumvallem2  13853  grppropd  13875  isgrpd2  13879  isgrpd  13881  dfgrp2  13885  grprcan  13895  grpinveu  13896  grpsubval  13904  grplinv  13908  grpinvid2  13911  isgrpinv  13912  grplrinv  13915  grpidinv2  13916  grpidinv  13917  grpidssd  13934  grpinvssd  13935  dfgrp3mlem  13956  dfgrp3m  13957  grplactfval  13959  grp1  13964  imasgrp2  13966  mhmmnd  13972  ghmgrp  13974  mulgnn0gzsum  13984  mulgnn0p1  13989  mulgnn0subcl  13991  mulgaddcom  14002  mulginvcom  14003  mulgnn0z  14005  mulgneg2  14012  mulgnnass  14013  mulgnn0ass  14014  mhmmulg  14019  issubg  14029  subgex  14032  issubg2m  14045  issubg4m  14049  isnsg2  14059  nsgbi  14060  isnsg3  14063  elnmz  14064  nmzbi  14065  ghmrn  14113  ghmnsgima  14124  elcntz  14148  cntzsnval  14150  elcntzsn  14151  cntzi  14156  cntzmhm  14167  gzsumconst  14227  gzsumshift  14233  gsumvalfi  14236  rngdi  14323  rngdir  14324  srgrz  14372  srgmulgass  14377  srgpcomp  14378  srgrmhm  14382  ringid  14415  ringinvnzdiv  14439  mulgass2  14447  ring1  14448  ringrghm  14451  imasring  14453  dvdsrmuld  14487  dvdsrmul1  14493  dvdsr01  14495  dvreq1  14533  rhmdvdsr  14566  lringuplu  14587  issubrng  14591  issubrng2  14602  issubrg  14613  issubrg2  14633  isrrg  14655  domneq0  14665  lmodlema  14712  islmodd  14713  lmodvsmmulgdi  14744  rmodislmodlem  14771  rmodislmod  14772  lssclg  14785  lss1d  14804  lspsn  14837  sraval  14858  rnglidlmcl  14901  quscrng  14954  cnfldmulg  14997  cnfldexp  14998  gsumfsum  15007  cnfldui  15008  expghmap  15026  mulgghm2  15027  mulgrhm  15028  zrhmulg  15039  zlmval  15046  znunit  15078  assalem  15087  asclvald  15106  assamulgscmlem2  15126  assamulgscm  15127  cnmptcom  15490  psmettri2  15520  isxmet2d  15540  xmeteq0  15551  xmettri2  15553  metrest  15698  mpomulcn  15758  expcn  15761  cncfval  15764  mulc1cncf  15781  addccncf  15792  mulcncf  15800  expcncf  15801  hovera  15839  hoverb  15840  hoverlt1  15841  hovergt0  15842  ivthdich  15845  limccnp2lem  15868  dvcnp2cntop  15891  dvcoapbr  15899  dvexp  15903  dvrecap  15905  dvef  15919  plyadd  15943  plymul  15944  plycoeid3  15949  plyco  15951  plycjlemc  15952  plycj  15953  plyrecj  15955  dvply1  15957  dvply2g  15958  sincn  15961  coscn  15962  ptolemy  16017  sincosq1eq  16032  rpcxpmul2  16110  logbgcd1irr  16164  logbgcd1irraplemexp  16165  2irrexpq  16173  2irrexpqap  16175  pellexlem3  16192  mpodvdsmulf1o  16245  fsumdvdsmul  16246  sgmppw  16247  sgmmul  16251  ppiqub  16254  perfect  16262  bposlem3  16274  bposlem5  16276  bposlem6  16277  bposlem8  16279  lgslem4  16288  lgsval  16289  lgsfvalg  16290  lgsval2lem  16295  lgsdir2lem4  16316  lgsdir  16320  lgsdilem2  16321  lgsdi  16322  lgsne0  16323  lgsmodeq  16330  lgsdirnn0  16332  lgsdinn0  16333  gausslemma2dlem0i  16342  gausslemma2dlem1a  16343  gausslemma2dlem1f1o  16345  gausslemma2dlem2  16347  gausslemma2dlem3  16348  gausslemma2dlem4  16349  lgseisenlem2  16356  lgsquadlem2  16363  lgsquadlem3  16364  lgsquad  16365  lgsquad2lem2  16367  2lgslem1a  16373  2lgslem1b  16374  2lgslem1c  16375  2lgslem3a  16378  2lgslem3b  16379  2lgslem3c  16380  2lgslem3d  16381  2lgslem3a1  16382  2lgslem3b1  16383  2lgslem3c1  16384  2lgslem3d1  16385  2lgs  16389  2lgsoddprmlem1  16390  2lgsoddprmlem3  16396  2sqlem2  16400  2sqlem6  16405  2sqlem8  16408  2sqlem9  16409  wlklenvm1  16748  wlklenvm1g  16749  wlkl1loop  16765  2wlklem  16783  clwwlknnn  16819  clwwlknp  16824  clwwlkn1  16825  clwwlkn2  16828  clwwlkext2edg  16829  umgr2cwwk2dif  16831  clwwlknon  16836  clwwlk0on0  16838  clwwlknonex2lem1  16844  clwwlknonex2lem2  16845  clwwlknonex2  16846  qdencn  17238  isomninn  17246  trirec0  17260  iswomninn  17267  ismkvnn  17270