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

Theorem reseq1i 5118
Description: Equality inference for restrictions. (Contributed by NM, 21-Oct-2014.)
Hypothesis
Ref Expression
reseqi.1  |-  A  =  B
Assertion
Ref Expression
reseq1i  |-  ( A  |`  C )  =  ( B  |`  C )

Proof of Theorem reseq1i
StepHypRef Expression
1 reseqi.1 . 2  |-  A  =  B
2 reseq1 5116 . 2  |-  ( A  =  B  ->  ( A  |`  C )  =  ( B  |`  C ) )
31, 2ax-mp 5 1  |-  ( A  |`  C )  =  ( B  |`  C )
Colors of variables: wff setvar class
Syntax hints:    = wceq 1438    |` cres 4853
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1666  ax-4 1679  ax-5 1749  ax-6 1795  ax-7 1840  ax-10 1888  ax-11 1893  ax-12 1906  ax-13 2054  ax-ext 2401
This theorem depends on definitions:  df-bi 189  df-an 373  df-tru 1441  df-ex 1661  df-nf 1665  df-sb 1788  df-clab 2409  df-cleq 2415  df-clel 2418  df-nfc 2573  df-v 3084  df-in 3444  df-res 4863
This theorem is referenced by:  reseq12i  5120  resindm  5166  resmpt  5171  resmpt3  5172  opabresid  5175  rescnvcnv  5315  coires1  5370  fresaunres1  5771  fcoi1  5772  fninfp  6104  fvsnun1  6112  fvsnun2  6113  resoprab  6404  resmpt2  6406  elrnmpt2res  6422  ofmres  6801  f1stres  6827  f2ndres  6828  df1st2  6891  df2nd2  6892  dftpos2  6996  wfrlem14  7055  tfr2a  7119  tfr2b  7120  rdgseg  7146  frsucmpt2  7163  seqomlem2  7174  seqomlem3  7175  seqomlem4  7176  domss2  7735  dffi3  7949  fpwwe2lem13  9069  seqval  12225  hashgval  12519  hashinf  12521  pgrpsubgsymg  17042  gsumzunsnd  17581  ablfac1b  17696  zzngim  19115  pmatcollpw3lem  19799  cnmptid  20668  txflf  21013  xmsxmet2  21466  msmet2  21467  tmsxpsmopn  21544  isngp2  21603  subgnm  21633  tngngp2  21652  cnfldms  21788  msdcn  21851  oprpiece1res1  21971  oprpiece1res2  21972  cncms  22314  cnfldcusp  22316  reust  22332  minveclem3a  22361  minveclem3aOLD  22373  dvreslem  22856  dvres2lem  22857  dvcmulf  22891  mdegfval  23003  psercn  23373  abelth  23388  efcvx  23396  efifo  23488  dfrelog  23507  dvrelog  23574  dvlog  23588  efopnlem2  23594  dvatan  23853  dchrisumlem1  24319  constr3pthlem1  25375  resmptf  28253  df1stres  28280  df2ndres  28281  padct  28307  ressplusf  28412  ressnm  28413  gsummpt2d  28545  qqhcn  28797  cnrrext  28816  rrhre  28827  esumcvg  28909  dya2icoseg2  29102  eulerpartgbij  29207  trpred0  30478  neibastop2  31016  mptsnunlem  31698  icorempt2  31712  poimirlem3  31901  mbfposadd  31946  ftc1anclem3  31977  dvasin  31986  dvacos  31987  prdsbnd2  32085  repwsmet  32124  rrnequiv  32125  diophin  35578  eldioph4b  35617  dnnumch1  35866  aomclem6  35881  radcnvrat  36565  lhe4.4ex1a  36580  dvsid  36582  dvsef  36583  elicores  37509  dvcosre  37645  dvmptresicc  37655  itgsinexplem1  37694  fourierdlem40  37874  fourierdlem57  37891  fourierdlem58  37892  fourierdlem62  37896  fourierdlem74  37908  fourierdlem75  37909  fourierdlem76  37910  fourierdlem80  37914  fourierdlem84  37918  fourierdlem85  37919  fourierdlem101  37935  fourierdlem102  37936  fourierdlem111  37945  fourierdlem114  37948  fouriersw  37959  fouriercn  37960  volicorescl  38194  fdmdifeqresdif  39467  aacllem  39884
  Copyright terms: Public domain W3C validator