MPE Home Metamath Proof Explorer < Previous   Next >
Nearby theorems
Mirrors  >  Home  >  MPE Home  >  Th. List  >  reseq2i Structured version   Visualization version   GIF version

Theorem reseq2i 5819
Description: Equality inference for restrictions. (Contributed by Paul Chapman, 22-Jun-2011.)
Hypothesis
Ref Expression
reseqi.1 𝐴 = 𝐵
Assertion
Ref Expression
reseq2i (𝐶𝐴) = (𝐶𝐵)

Proof of Theorem reseq2i
StepHypRef Expression
1 reseqi.1 . 2 𝐴 = 𝐵
2 reseq2 5817 . 2 (𝐴 = 𝐵 → (𝐶𝐴) = (𝐶𝐵))
31, 2ax-mp 5 1 (𝐶𝐴) = (𝐶𝐵)
Colors of variables: wff setvar class
Syntax hints:   = wceq 1538  cres 5525
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1797  ax-4 1811  ax-5 1911  ax-6 1970  ax-7 2015  ax-8 2114  ax-9 2122  ax-12 2176  ax-ext 2773
This theorem depends on definitions:  df-bi 210  df-an 400  df-tru 1541  df-ex 1782  df-nf 1786  df-sb 2070  df-clab 2780  df-cleq 2794  df-clel 2873  df-rab 3118  df-in 3891  df-opab 5096  df-xp 5529  df-res 5535
This theorem is referenced by:  reseq12i  5820  rescom  5848  resdmdfsn  5872  idinxpresid  5886  rescnvcnv  6032  resdm2  6059  funcnvres  6406  resasplit  6526  fresaunres2  6528  fresaunres1  6529  resdif  6614  resin  6615  funcocnv2  6618  fvn0ssdmfun  6823  residpr  6886  wfrlem5  7946  domss2  8664  ordtypelem1  8970  ackbij2lem3  9656  facnn  13635  fac0  13636  hashresfn  13700  relexpcnv  14390  divcnvshft  15206  ruclem4  15583  fsets  16512  setsid  16534  meet0  17743  join0  17744  symgfixelsi  18559  psgnsn  18644  dprd2da  19161  ply1plusgfvi  20875  uptx  22234  txcn  22235  ressxms  23136  ressms  23137  iscmet3lem3  23898  volres  24136  dvlip  24600  dvne0  24618  lhop  24623  dflog2  25156  dfrelog  25161  dvlog  25246  wilthlem2  25658  0grsubgr  27072  0pth  27914  1pthdlem1  27924  eupth2lemb  28026  ex-fpar  28251  fressupp  30452  df1stres  30467  df2ndres  30468  ffsrn  30495  resf1o  30496  fpwrelmapffs  30500  cycpmconjv  30838  sitmcl  31723  eulerpartlemn  31753  bnj1326  32412  satfv1lem  32723  divcnvlin  33078  eqfunressuc  33119  fprlem1  33251  frrlem15  33256  nosupbnd2lem1  33329  poimirlem9  35065  zrdivrng  35390  isdrngo1  35393  cnvresrn  35764  eldioph4b  39749  diophren  39751  rclexi  40312  rtrclex  40314  cnvrcl0  40322  dfrtrcl5  40326  dfrcl2  40372  relexpiidm  40402  relexp01min  40411  relexpaddss  40416  seff  41010  sblpnf  41011  radcnvrat  41015  hashnzfzclim  41023  dvresioo  42560  fourierdlem72  42817  fourierdlem80  42825  fourierdlem94  42839  fourierdlem103  42848  fourierdlem104  42849  fourierdlem113  42858  fouriersw  42870  sge0split  43045  rngcidALTV  44612  ringcidALTV  44675
  Copyright terms: Public domain W3C validator