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

Theorem reseq2d 5366
Description: Equality deduction for restrictions. (Contributed by Paul Chapman, 22-Jun-2011.)
Hypothesis
Ref Expression
reseqd.1 (𝜑𝐴 = 𝐵)
Assertion
Ref Expression
reseq2d (𝜑 → (𝐶𝐴) = (𝐶𝐵))

Proof of Theorem reseq2d
StepHypRef Expression
1 reseqd.1 . 2 (𝜑𝐴 = 𝐵)
2 reseq2 5361 . 2 (𝐴 = 𝐵 → (𝐶𝐴) = (𝐶𝐵))
31, 2syl 17 1 (𝜑 → (𝐶𝐴) = (𝐶𝐵))
Colors of variables: wff setvar class
Syntax hints:  wi 4   = wceq 1480  cres 5086
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1719  ax-4 1734  ax-5 1836  ax-6 1885  ax-7 1932  ax-9 1996  ax-10 2016  ax-11 2031  ax-12 2044  ax-13 2245  ax-ext 2601
This theorem depends on definitions:  df-bi 197  df-or 385  df-an 386  df-tru 1483  df-ex 1702  df-nf 1707  df-sb 1878  df-clab 2608  df-cleq 2614  df-clel 2617  df-nfc 2750  df-v 3192  df-in 3567  df-opab 4684  df-xp 5090  df-res 5096
This theorem is referenced by:  reseq12d  5367  resima2OLD  5402  resresdm  5595  relresfld  5631  f1orescnv  6119  fococnv2  6129  fvn0ssdmfun  6316  fnressn  6390  fnsnsplit  6415  oprssov  6768  curry1  7229  curry2  7232  dftpos2  7329  wrecseq123  7368  wfr3g  7373  wfrlem1  7374  wfrlem4  7378  wfrlem14  7388  wfr2a  7392  dfrecs3  7429  tfrlem16  7449  tfr2ALT  7457  tfr3ALT  7458  sbthlem4  8033  mapunen  8089  hartogslem1  8407  axdc3lem2  9233  fseq1p1m1  12371  resunimafz0  13183  hashf1lem1  13193  relexp0g  13712  relexp0  13713  relexpsucnnr  13715  dfrtrcl2  13752  bpolylem  14723  setsval  15828  idfuval  16476  idfu2nd  16477  resf1st  16494  setcid  16676  catcisolem  16696  estrcid  16714  funcestrcsetclem5  16724  funcsetcestrclem5  16739  funcsetcestrclem7  16741  1stfval  16771  1stf2  16773  2ndfval  16774  2ndf2  16776  1stfcl  16777  2ndfcl  16778  curf2ndf  16827  hofcl  16839  isps  17142  cnvps  17152  isdir  17172  dirref  17175  tsrdir  17178  frmdval  17328  frmdplusg  17331  gsum2dlem2  18310  dprd2da  18381  dpjval  18395  ablfac1eulem  18411  ablfac1eu  18412  psrplusg  19321  opsrtoslem2  19425  mdetunilem3  20360  mdetunilem4  20361  mdetunilem9  20366  imacmp  21140  ptuncnv  21550  tgphaus  21860  tsmsres  21887  tsmsxplem1  21896  tsmsxplem2  21897  trust  21973  metreslem  22107  imasdsf1olem  22118  xmspropd  22218  mspropd  22219  imasf1oxms  22234  imasf1oms  22235  nmpropd2  22339  isngp2  22341  ngppropd  22381  tngngp2  22396  cmspropd  23086  mbfres2  23352  limciun  23598  dvmptres3  23659  dvmptres2  23665  dvmptntr  23674  dvlipcn  23695  dvlip2  23696  c1liplem1  23697  dvgt0lem1  23703  lhop1lem  23714  dvcnvrelem1  23718  dvcvx  23721  ftc2ditglem  23746  wilthlem2  24729  dchrval  24893  dchrelbas2  24896  egrsubgr  26096  pthdlem1  26565  eupthvdres  26995  eupth2lem3  26996  eupth2  26999  eucrct2eupth  27005  hhssablo  28008  hhssnvt  28010  hhsssh  28014  resf1o  29389  gsummpt2d  29608  qtophaus  29727  esumcvg  29971  eulerpartlemn  30266  sseqp1  30280  signsvtn0  30469  ftc2re  30492  breprsuc  30501  bnj1385  30664  bnj1326  30855  bnj1321  30856  bnj1442  30878  bnj1450  30879  bnj1463  30884  bnj1529  30899  cvmliftlem5  31032  cvmliftlem7  31034  cvmliftlem10  31037  cvmliftlem11  31038  cvmliftlem15  31041  cvmlift2lem11  31056  cvmlift2lem12  31057  eldm3  31413  funsseq  31423  frr3g  31533  frrlem1  31534  frrlem4  31537  noreslege  31624  nosino  31628  nosifv  31629  nosires  31630  finixpnum  33065  poimirlem3  33083  poimirlem4  33084  poimirlem9  33089  sdclem2  33209  prdsbnd2  33265  isdivrngo  33420  drngoi  33421  dibffval  35948  hdmapffval  36637  hdmapfval  36638  eldiophb  36839  diophrw  36841  diophin  36855  rclexi  37442  rtrclex  37444  rtrclexi  37448  cnvrcl0  37452  dfrtrcl5  37456  dfrcl2  37486  fvmptiunrelexplb0da  37497  sblpnf  38030  fresin2  38861  limsupresuz  39371  limsupvaluz  39376  limsupvaluz2  39406  supcnvlimsup  39408  cncfuni  39434  dvresntr  39468  dvbdfbdioolem1  39480  itgiccshift  39533  itgperiod  39534  dirkercncflem2  39658  fourierdlem46  39706  fourierdlem48  39708  fourierdlem49  39709  fourierdlem58  39718  fourierdlem72  39732  fourierdlem74  39734  fourierdlem75  39735  fourierdlem81  39741  fourierdlem88  39748  fourierdlem89  39749  fourierdlem90  39750  fourierdlem91  39751  fourierdlem92  39752  fourierdlem103  39763  fourierdlem104  39764  fourierdlem112  39772  fouriersw  39785  voncmpl  40172  funcoressn  40541  idfusubc0  41183  idfusubc  41184  rngcval  41280  rnghmsubcsetclem1  41293  rngccat  41296  rngcid  41297  rngcidALTV  41309  rngcifuestrc  41315  funcrngcsetc  41316  funcrngcsetcALT  41317  ringcval  41326  rhmsubcsetclem1  41339  ringccat  41342  ringcid  41343  rhmsubcrngclem1  41345  rhmsubcrngc  41347  funcringcsetc  41353  funcringcsetcALTV2lem5  41358  ringcidALTV  41372  funcringcsetclem5ALTV  41381  rhmsubc  41408  rhmsubcALTVlem3  41424  aacllem  41880
  Copyright terms: Public domain W3C validator