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

Theorem reseq1i 4951
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 4949 . 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 1623    |` cres 4691
This theorem is referenced by:  reseq12i  4953  resmpt  5000  resmpt3  5001  opabresid  5003  rescnvcnv  5135  coires1  5190  fresaunres1  5414  fcoi1  5415  fvsnun1  5715  fvsnun2  5716  resoprab  5940  resmpt2  5942  ofmres  6116  f1stres  6141  f2ndres  6142  df1st2  6205  df2nd2  6206  dftpos2  6251  tfr2a  6411  tfr2b  6412  rdgseg  6435  frsucmpt2  6452  seqomlem2  6463  seqomlem3  6464  seqomlem4  6465  domss2  7020  dffi3  7184  fpwwe2lem13  8264  seqval  11057  hashgval  11340  hashinf  11342  ablfac1b  15305  zzngim  16506  cnmptid  17355  txflf  17701  xmsxmet2  18005  msmet2  18006  tmsxpsmopn  18083  isngp2  18119  subgnm  18149  tngngp2  18168  cnfldms  18285  msdcn  18346  oprpiece1res1  18449  oprpiece1res2  18450  cncms  18774  minveclem3a  18791  dvreslem  19259  dvres2lem  19260  dvcmulf  19294  mdegfval  19448  psercn  19802  abelth  19817  efcvx  19825  efifo  19909  dfrelog  19923  dvrelog  19984  dvlog  19998  efopnlem2  20004  dvatan  20231  dchrisumlem1  20638  resmptf  23223  df1stres  23243  df2ndres  23244  ressplusf  23298  esumcvg  23454  trpred0  24239  wfrlem14  24269  prsubrtr  25399  neibastop2  26310  prdsbnd2  26519  repwsmet  26558  rrnequiv  26559  fninfp  26754  diophin  26852  eldioph4b  26894  dnnumch1  27141  aomclem6  27156  lhe4.4ex1a  27546  dvsid  27548  dvsef  27549  dvcosre  27741  itgsinexplem1  27748
This theorem was proved from axioms:  ax-1 5  ax-2 6  ax-3 7  ax-mp 8  ax-gen 1533  ax-5 1544  ax-17 1603  ax-9 1635  ax-8 1643  ax-6 1703  ax-7 1708  ax-11 1715  ax-12 1866  ax-ext 2264
This theorem depends on definitions:  df-bi 177  df-or 359  df-an 360  df-tru 1310  df-ex 1529  df-nf 1532  df-sb 1630  df-clab 2270  df-cleq 2276  df-clel 2279  df-nfc 2408  df-v 2790  df-in 3159  df-res 4701
  Copyright terms: Public domain W3C validator