MPE Home Metamath Proof Explorer < Previous   Next >
Nearby theorems
Mirrors  >  Home  >  MPE Home  >  Th. List  >  reseq1i Structured version   Visualization version   GIF version

Theorem reseq1i 5300
Description: Equality inference for restrictions. (Contributed by NM, 21-Oct-2014.)
Hypothesis
Ref Expression
reseqi.1 𝐴 = 𝐵
Assertion
Ref Expression
reseq1i (𝐴𝐶) = (𝐵𝐶)

Proof of Theorem reseq1i
StepHypRef Expression
1 reseqi.1 . 2 𝐴 = 𝐵
2 reseq1 5298 . 2 (𝐴 = 𝐵 → (𝐴𝐶) = (𝐵𝐶))
31, 2ax-mp 5 1 (𝐴𝐶) = (𝐵𝐶)
Colors of variables: wff setvar class
Syntax hints:   = wceq 1474  cres 5030
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1712  ax-4 1727  ax-5 1826  ax-6 1874  ax-7 1921  ax-10 2005  ax-11 2020  ax-12 2032  ax-13 2232  ax-ext 2589
This theorem depends on definitions:  df-bi 195  df-or 383  df-an 384  df-tru 1477  df-ex 1695  df-nf 1700  df-sb 1867  df-clab 2596  df-cleq 2602  df-clel 2605  df-nfc 2739  df-v 3174  df-in 3546  df-res 5040
This theorem is referenced by:  reseq12i  5302  resindm  5351  resmpt  5356  resmpt3  5357  opabresid  5361  rescnvcnv  5501  coires1  5556  fresaunres1  5975  fcoi1  5976  fninfp  6323  fvsnun1  6331  fvsnun2  6332  resoprab  6632  resmpt2  6634  elrnmpt2res  6650  ofmres  7032  f1stres  7058  f2ndres  7059  df1st2  7127  df2nd2  7128  dftpos2  7233  wfrlem14  7292  tfr2a  7355  tfr2b  7356  rdgseg  7382  frsucmpt2  7399  seqomlem2  7410  seqomlem3  7411  seqomlem4  7412  domss2  7981  dffi3  8197  fpwwe2lem13  9320  seqval  12629  hashgval  12937  hashinf  12939  pgrpsubgsymg  17597  gsumzunsnd  18124  ablfac1b  18238  zzngim  19665  pmatcollpw3lem  20349  cnmptid  21216  txflf  21562  xmsxmet2  22015  msmet2  22016  tmsxpsmopn  22093  isngp2  22152  subgnm  22185  tngngp2  22204  cnfldms  22321  msdcn  22384  oprpiece1res1  22489  oprpiece1res2  22490  isncvsngp  22683  cncms  22876  cnfldcusp  22878  reust  22894  minveclem3a  22923  dvreslem  23396  dvres2lem  23397  dvcmulf  23431  mdegfval  23543  psercn  23901  abelth  23916  efcvx  23924  efifo  24014  dfrelog  24033  dvrelog  24100  dvlog  24114  efopnlem2  24120  dvatan  24379  dchrisumlem1  24895  constr3pthlem1  25949  resmptf  28644  df1stres  28670  df2ndres  28671  padct  28691  ressplusf  28787  ressnm  28788  gsummpt2d  28918  qqhcn  29169  cnrrext  29188  rrhre  29199  esumcvg  29281  dya2icoseg2  29473  eulerpartgbij  29567  trpred0  30786  neibastop2  31332  mptsnunlem  32164  icorempt2  32178  poimirlem3  32385  mbfposadd  32430  ftc1anclem3  32460  dvasin  32469  dvacos  32470  prdsbnd2  32567  repwsmet  32606  rrnequiv  32607  diophin  36157  eldioph4b  36196  dnnumch1  36435  aomclem6  36450  radcnvrat  37338  lhe4.4ex1a  37353  dvsid  37355  dvsef  37356  elicores  38411  climresmpt  38530  dvcosre  38603  dvmptresicc  38613  itgsinexplem1  38649  fourierdlem40  38844  fourierdlem57  38860  fourierdlem58  38861  fourierdlem62  38865  fourierdlem74  38877  fourierdlem75  38878  fourierdlem76  38879  fourierdlem80  38883  fourierdlem84  38887  fourierdlem85  38888  fourierdlem101  38904  fourierdlem102  38905  fourierdlem111  38914  fourierdlem114  38917  fouriersw  38928  fouriercn  38929  volicorescl  39247  fdmdifeqresdif  41915  aacllem  42319
  Copyright terms: Public domain W3C validator