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

Theorem reseq1i 5144
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 5142 . 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 1653    |` cres 4882
This theorem is referenced by:  reseq12i  5146  resmpt  5193  resmpt3  5194  opabresid  5196  rescnvcnv  5334  coires1  5389  fresaunres1  5618  fcoi1  5619  fvsnun1  5930  fvsnun2  5931  resoprab  6168  resmpt2  6170  ofmres  6345  f1stres  6370  f2ndres  6371  df1st2  6435  df2nd2  6436  dftpos2  6498  tfr2a  6658  tfr2b  6659  rdgseg  6682  frsucmpt2  6699  seqomlem2  6710  seqomlem3  6711  seqomlem4  6712  domss2  7268  dffi3  7438  fpwwe2lem13  8519  seqval  11336  hashgval  11623  hashinf  11625  ablfac1b  15630  zzngim  16835  cnmptid  17695  txflf  18040  xmsxmet2  18491  msmet2  18492  tmsxpsmopn  18569  isngp2  18646  subgnm  18676  tngngp2  18695  cnfldms  18812  msdcn  18874  oprpiece1res1  18978  oprpiece1res2  18979  cncms  19311  cnfldcusp  19313  minveclem3a  19330  dvreslem  19798  dvres2lem  19799  dvcmulf  19833  mdegfval  19987  psercn  20344  abelth  20359  efcvx  20367  efifo  20451  dfrelog  20465  dvrelog  20530  dvlog  20544  efopnlem2  20550  dvatan  20777  dchrisumlem1  21185  constr3pthlem1  21644  resmptf  24073  df1stres  24093  df2ndres  24094  ressplusf  24185  ressnm  24186  reust  24346  qqhcn  24377  rrhre  24389  esumcvg  24478  dya2icoseg2  24630  trpred0  25516  wfrlem14  25553  ftc1anclem3  26284  neibastop2  26392  prdsbnd2  26506  repwsmet  26545  rrnequiv  26546  fninfp  26737  diophin  26833  eldioph4b  26874  dnnumch1  27121  aomclem6  27136  lhe4.4ex1a  27525  dvsid  27527  dvsef  27528  dvcosre  27719  itgsinexplem1  27726
This theorem was proved from axioms:  ax-1 5  ax-2 6  ax-3 7  ax-mp 8  ax-gen 1556  ax-5 1567  ax-17 1627  ax-9 1667  ax-8 1688  ax-6 1745  ax-7 1750  ax-11 1762  ax-12 1951  ax-ext 2419
This theorem depends on definitions:  df-bi 179  df-or 361  df-an 362  df-tru 1329  df-ex 1552  df-nf 1555  df-sb 1660  df-clab 2425  df-cleq 2431  df-clel 2434  df-nfc 2563  df-v 2960  df-in 3329  df-res 4892
  Copyright terms: Public domain W3C validator