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

Theorem reseq2d 5385
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 5380 . 2 (𝐴 = 𝐵 → (𝐶𝐴) = (𝐶𝐵))
31, 2syl 17 1 (𝜑 → (𝐶𝐴) = (𝐶𝐵))
Colors of variables: wff setvar class
Syntax hints:  wi 4   = wceq 1481  cres 5106
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1720  ax-4 1735  ax-5 1837  ax-6 1886  ax-7 1933  ax-9 1997  ax-10 2017  ax-11 2032  ax-12 2045  ax-13 2244  ax-ext 2600
This theorem depends on definitions:  df-bi 197  df-or 385  df-an 386  df-tru 1484  df-ex 1703  df-nf 1708  df-sb 1879  df-clab 2607  df-cleq 2613  df-clel 2616  df-nfc 2751  df-v 3197  df-in 3574  df-opab 4704  df-xp 5110  df-res 5116
This theorem is referenced by:  reseq12d  5386  resima2OLD  5421  resresdm  5614  relresfld  5650  f1orescnv  6139  fococnv2  6149  fvn0ssdmfun  6336  fnressn  6410  fnsnsplit  6435  oprssov  6788  curry1  7254  curry2  7257  dftpos2  7354  wrecseq123  7393  wfr3g  7398  wfrlem1  7399  wfrlem4  7403  wfrlem14  7413  wfr2a  7417  dfrecs3  7454  tfrlem16  7474  tfr2ALT  7482  tfr3ALT  7483  sbthlem4  8058  mapunen  8114  hartogslem1  8432  axdc3lem2  9258  fseq1p1m1  12398  resunimafz0  13212  hashf1lem1  13222  relexp0g  13743  relexp0  13744  relexpsucnnr  13746  dfrtrcl2  13783  bpolylem  14760  setsval  15869  idfuval  16517  idfu2nd  16518  resf1st  16535  setcid  16717  catcisolem  16737  estrcid  16755  funcestrcsetclem5  16765  funcsetcestrclem5  16780  funcsetcestrclem7  16782  1stfval  16812  1stf2  16814  2ndfval  16815  2ndf2  16817  1stfcl  16818  2ndfcl  16819  curf2ndf  16868  hofcl  16880  isps  17183  cnvps  17193  isdir  17213  dirref  17216  tsrdir  17219  frmdval  17369  frmdplusg  17372  gsum2dlem2  18351  dprd2da  18422  dpjval  18436  ablfac1eulem  18452  ablfac1eu  18453  psrplusg  19362  opsrtoslem2  19466  mdetunilem3  20401  mdetunilem4  20402  mdetunilem9  20407  imacmp  21181  ptuncnv  21591  tgphaus  21901  tsmsres  21928  tsmsxplem1  21937  tsmsxplem2  21938  trust  22014  metreslem  22148  imasdsf1olem  22159  xmspropd  22259  mspropd  22260  imasf1oxms  22275  imasf1oms  22276  nmpropd2  22380  isngp2  22382  ngppropd  22422  tngngp2  22437  cmspropd  23127  mbfres2  23393  limciun  23639  dvmptres3  23700  dvmptres2  23706  dvmptntr  23715  dvlipcn  23738  dvlip2  23739  c1liplem1  23740  dvgt0lem1  23746  lhop1lem  23757  dvcnvrelem1  23761  dvcvx  23764  ftc2ditglem  23789  wilthlem2  24776  dchrval  24940  dchrelbas2  24943  egrsubgr  26150  pthdlem1  26643  eupthvdres  27075  eupth2lem3  27076  eupth2  27079  eucrct2eupth  27085  hhssablo  28090  hhssnvt  28092  hhsssh  28096  fnunres1  29389  resf1o  29479  gsummpt2d  29755  qtophaus  29877  esumcvg  30122  eulerpartlemn  30417  sseqp1  30431  signsvtn0  30621  ftc2re  30650  reprsuc  30667  bnj1385  30877  bnj1326  31068  bnj1321  31069  bnj1442  31091  bnj1450  31092  bnj1463  31097  bnj1529  31112  cvmliftlem5  31245  cvmliftlem7  31247  cvmliftlem10  31250  cvmliftlem11  31251  cvmliftlem15  31254  cvmlift2lem11  31269  cvmlift2lem12  31270  eldm3  31627  funsseq  31642  frr3g  31753  frrlem1  31754  frrlem4  31757  noresle  31820  nosupno  31823  nosupdm  31824  nosupfv  31826  nosupres  31827  nosupbnd1lem1  31828  nosupbnd1lem3  31830  nosupbnd1lem5  31832  nosupbnd1  31834  nosupbnd2  31836  noeta  31842  finixpnum  33365  poimirlem3  33383  poimirlem4  33384  poimirlem9  33389  sdclem2  33509  prdsbnd2  33565  isdivrngo  33720  drngoi  33721  dibffval  36248  hdmapffval  36937  hdmapfval  36938  eldiophb  37139  diophrw  37141  diophin  37155  rclexi  37741  rtrclex  37743  rtrclexi  37747  cnvrcl0  37751  dfrtrcl5  37755  dfrcl2  37785  fvmptiunrelexplb0da  37796  sblpnf  38329  fresin2  39168  limsupresuz  39735  limsupvaluz  39740  limsupvaluz2  39770  supcnvlimsup  39772  liminfresuz  39810  cncfuni  39862  dvresntr  39895  dvbdfbdioolem1  39906  itgiccshift  39959  itgperiod  39960  dirkercncflem2  40084  fourierdlem46  40132  fourierdlem48  40134  fourierdlem49  40135  fourierdlem58  40144  fourierdlem72  40158  fourierdlem74  40160  fourierdlem75  40161  fourierdlem81  40167  fourierdlem88  40174  fourierdlem89  40175  fourierdlem90  40176  fourierdlem91  40177  fourierdlem92  40178  fourierdlem103  40189  fourierdlem104  40190  fourierdlem112  40198  fouriersw  40211  voncmpl  40598  funcoressn  40970  idfusubc0  41630  idfusubc  41631  rngcval  41727  rnghmsubcsetclem1  41740  rngccat  41743  rngcid  41744  rngcidALTV  41756  rngcifuestrc  41762  funcrngcsetc  41763  funcrngcsetcALT  41764  ringcval  41773  rhmsubcsetclem1  41786  ringccat  41789  ringcid  41790  rhmsubcrngclem1  41792  rhmsubcrngc  41794  funcringcsetc  41800  funcringcsetcALTV2lem5  41805  ringcidALTV  41819  funcringcsetclem5ALTV  41828  rhmsubc  41855  rhmsubcALTVlem3  41871  aacllem  42312
  Copyright terms: Public domain W3C validator