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

Theorem reseq1i 5258
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 5256 . 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 1398    |` cres 4990
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1623  ax-4 1636  ax-5 1709  ax-6 1752  ax-7 1795  ax-10 1842  ax-11 1847  ax-12 1859  ax-13 2004  ax-ext 2432
This theorem depends on definitions:  df-bi 185  df-an 369  df-tru 1401  df-ex 1618  df-nf 1622  df-sb 1745  df-clab 2440  df-cleq 2446  df-clel 2449  df-nfc 2604  df-v 3108  df-in 3468  df-res 5000
This theorem is referenced by:  reseq12i  5260  resindm  5306  resmpt  5311  resmpt3  5312  opabresid  5315  rescnvcnv  5453  coires1  5508  fresaunres1  5740  fcoi1  5741  fninfp  6074  fvsnun1  6082  fvsnun2  6083  resoprab  6371  resmpt2  6373  elrnmpt2res  6389  ofmres  6769  f1stres  6795  f2ndres  6796  df1st2  6859  df2nd2  6860  dftpos2  6964  tfr2a  7056  tfr2b  7057  rdgseg  7080  frsucmpt2  7097  seqomlem2  7108  seqomlem3  7109  seqomlem4  7110  domss2  7669  dffi3  7883  fpwwe2lem13  9009  seqval  12100  hashgval  12390  hashinf  12392  pgrpsubgsymg  16632  gsumzunsnd  17178  ablfac1b  17316  zzngim  18764  pmatcollpw3lem  19451  cnmptid  20328  txflf  20673  xmsxmet2  21128  msmet2  21129  tmsxpsmopn  21206  isngp2  21283  subgnm  21313  tngngp2  21332  cnfldms  21449  msdcn  21512  oprpiece1res1  21617  oprpiece1res2  21618  cncms  21961  cnfldcusp  21963  reust  21979  minveclem3a  22008  dvreslem  22479  dvres2lem  22480  dvcmulf  22514  mdegfval  22626  psercn  22987  abelth  23002  efcvx  23010  efifo  23100  dfrelog  23119  dvrelog  23186  dvlog  23200  efopnlem2  23206  dvatan  23463  dchrisumlem1  23872  constr3pthlem1  24857  resmptf  27719  df1stres  27750  df2ndres  27751  padct  27776  ressplusf  27872  ressnm  27873  gsummpt2d  28006  qqhcn  28206  cnrrext  28225  rrhre  28233  esumcvg  28315  dya2icoseg2  28486  eulerpartgbij  28575  trpred0  29559  wfrlem14  29596  mbfposadd  30302  ftc1anclem3  30332  dvasin  30343  dvacos  30344  neibastop2  30419  prdsbnd2  30531  repwsmet  30570  rrnequiv  30571  diophin  30945  eldioph4b  30984  dnnumch1  31229  aomclem6  31244  radcnvrat  31436  lhe4.4ex1a  31475  dvsid  31477  dvsef  31478  dvcosre  31945  dvmptresicc  31955  itgsinexplem1  31991  fourierdlem40  32168  fourierdlem57  32185  fourierdlem58  32186  fourierdlem62  32190  fourierdlem74  32202  fourierdlem75  32203  fourierdlem76  32204  fourierdlem80  32208  fourierdlem84  32212  fourierdlem85  32213  fourierdlem101  32229  fourierdlem102  32230  fourierdlem111  32239  fourierdlem114  32242  fouriersw  32253  fouriercn  32254  fdmdifeqresdif  33185  aacllem  33604
  Copyright terms: Public domain W3C validator