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

Theorem reseq1i 4967
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 4965 . 2  |-  ( A  =  B  ->  ( A  |`  C )  =  ( B  |`  C ) )
31, 2ax-mp 8 1  |-  ( A  |`  C )  =  ( B  |`  C )
Colors of variables: wff set class
Syntax hints:    = wceq 1632    |` cres 4707
This theorem is referenced by:  reseq12i  4969  resmpt  5016  resmpt3  5017  opabresid  5019  rescnvcnv  5151  coires1  5206  fresaunres1  5430  fcoi1  5431  fvsnun1  5731  fvsnun2  5732  resoprab  5956  resmpt2  5958  ofmres  6132  f1stres  6157  f2ndres  6158  df1st2  6221  df2nd2  6222  dftpos2  6267  tfr2a  6427  tfr2b  6428  rdgseg  6451  frsucmpt2  6468  seqomlem2  6479  seqomlem3  6480  seqomlem4  6481  domss2  7036  dffi3  7200  fpwwe2lem13  8280  seqval  11073  hashgval  11356  hashinf  11358  ablfac1b  15321  zzngim  16522  cnmptid  17371  txflf  17717  xmsxmet2  18021  msmet2  18022  tmsxpsmopn  18099  isngp2  18135  subgnm  18165  tngngp2  18184  cnfldms  18301  msdcn  18362  oprpiece1res1  18465  oprpiece1res2  18466  cncms  18790  minveclem3a  18807  dvreslem  19275  dvres2lem  19276  dvcmulf  19310  mdegfval  19464  psercn  19818  abelth  19833  efcvx  19841  efifo  19925  dfrelog  19939  dvrelog  20000  dvlog  20014  efopnlem2  20020  dvatan  20247  dchrisumlem1  20654  resmptf  23238  df1stres  23258  df2ndres  23259  ressplusf  23313  esumcvg  23469  trpred0  24310  wfrlem14  24340  prsubrtr  25502  neibastop2  26413  prdsbnd2  26622  repwsmet  26661  rrnequiv  26662  fninfp  26857  diophin  26955  eldioph4b  26997  dnnumch1  27244  aomclem6  27259  lhe4.4ex1a  27649  dvsid  27651  dvsef  27652  dvcosre  27844  itgsinexplem1  27851  constr3pthlem1  28401
This theorem was proved from axioms:  ax-1 5  ax-2 6  ax-3 7  ax-mp 8  ax-gen 1536  ax-5 1547  ax-17 1606  ax-9 1644  ax-8 1661  ax-6 1715  ax-7 1720  ax-11 1727  ax-12 1878  ax-ext 2277
This theorem depends on definitions:  df-bi 177  df-or 359  df-an 360  df-tru 1310  df-ex 1532  df-nf 1535  df-sb 1639  df-clab 2283  df-cleq 2289  df-clel 2292  df-nfc 2421  df-v 2803  df-in 3172  df-res 4717
  Copyright terms: Public domain W3C validator