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

Theorem reseq2d 5534
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 5529 . 2 (𝐴 = 𝐵 → (𝐶𝐴) = (𝐶𝐵))
31, 2syl 17 1 (𝜑 → (𝐶𝐴) = (𝐶𝐵))
Colors of variables: wff setvar class
Syntax hints:  wi 4   = wceq 1631  cres 5251
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1870  ax-4 1885  ax-5 1991  ax-6 2057  ax-7 2093  ax-9 2154  ax-10 2174  ax-11 2190  ax-12 2203  ax-13 2408  ax-ext 2751
This theorem depends on definitions:  df-bi 197  df-an 383  df-or 835  df-tru 1634  df-ex 1853  df-nf 1858  df-sb 2050  df-clab 2758  df-cleq 2764  df-clel 2767  df-nfc 2902  df-v 3353  df-in 3730  df-opab 4847  df-xp 5255  df-res 5261
This theorem is referenced by:  reseq12d  5535  resima2OLD  5574  resresdm  5770  relresfld  5806  f1orescnv  6293  fococnv2  6303  fvn0ssdmfun  6493  fnressn  6568  fnsnsplit  6594  oprssov  6950  curry1  7420  curry2  7423  dftpos2  7521  wrecseq123  7560  wfr3g  7565  wfrlem1  7566  wfrlem4  7570  wfrlem4OLD  7571  wfrlem14  7581  wfr2a  7585  dfrecs3  7622  tfrlem16  7642  tfr2ALT  7650  tfr3ALT  7651  sbthlem4  8229  mapunen  8285  hartogslem1  8603  axdc3lem2  9475  fseq1p1m1  12621  resunimafz0  13431  hashf1lem1  13441  relexp0g  13970  relexp0  13971  relexpsucnnr  13973  dfrtrcl2  14010  bpolylem  14985  setsval  16095  idfuval  16743  idfu2nd  16744  resf1st  16761  setcid  16943  catcisolem  16963  estrcid  16981  funcestrcsetclem5  16992  funcsetcestrclem5  17007  funcsetcestrclem7  17009  1stfval  17039  1stf2  17041  2ndfval  17042  2ndf2  17044  1stfcl  17045  2ndfcl  17046  curf2ndf  17095  hofcl  17107  isps  17410  cnvps  17420  isdir  17440  dirref  17443  tsrdir  17446  frmdval  17596  frmdplusg  17599  gsum2dlem2  18577  dprd2da  18649  dpjval  18663  ablfac1eulem  18679  ablfac1eu  18680  psrplusg  19596  opsrtoslem2  19700  mdetunilem3  20638  mdetunilem4  20639  mdetunilem9  20644  imacmp  21421  ptuncnv  21831  tgphaus  22140  tsmsres  22167  tsmsxplem1  22176  tsmsxplem2  22177  trust  22253  metreslem  22387  imasdsf1olem  22398  xmspropd  22498  mspropd  22499  imasf1oxms  22514  imasf1oms  22515  nmpropd2  22619  isngp2  22621  ngppropd  22661  tngngp2  22676  cmspropd  23365  mbfres2  23632  limciun  23878  dvmptres3  23939  dvmptres2  23945  dvmptntr  23954  dvlipcn  23977  dvlip2  23978  c1liplem1  23979  dvgt0lem1  23985  lhop1lem  23996  dvcnvrelem1  24000  dvcvx  24003  ftc2ditglem  24028  wilthlem2  25016  dchrval  25180  dchrelbas2  25183  egrsubgr  26392  pthdlem1  26897  eupthvdres  27415  eupth2lem3  27416  eupth2  27419  eucrct2eupth  27425  dlwwlknondlwlknonf1oOLD  27556  hhssablo  28460  hhssnvt  28462  hhsssh  28466  fnunres1  29755  resf1o  29845  gsummpt2d  30121  qtophaus  30243  esumcvg  30488  eulerpartlemn  30783  sseqp1  30797  signsvtn0  30987  ftc2re  31016  reprsuc  31033  bnj1385  31241  bnj1326  31432  bnj1321  31433  bnj1442  31455  bnj1450  31456  bnj1463  31461  bnj1529  31476  cvmliftlem5  31609  cvmliftlem7  31611  cvmliftlem10  31614  cvmliftlem11  31615  cvmliftlem15  31618  cvmlift2lem11  31633  cvmlift2lem12  31634  eldm3  31989  funsseq  32004  frecseq123  32114  frr3g  32116  frrlem1  32117  frrlem4  32120  noresle  32183  nosupno  32186  nosupdm  32187  nosupfv  32189  nosupres  32190  nosupbnd1lem1  32191  nosupbnd1lem3  32193  nosupbnd1lem5  32195  nosupbnd1  32197  nosupbnd2  32199  noeta  32205  finixpnum  33727  poimirlem3  33745  poimirlem4  33746  poimirlem9  33751  sdclem2  33870  prdsbnd2  33926  isdivrngo  34081  drngoi  34082  elrefsymrels2  34657  dibffval  36950  hdmapffval  37636  hdmapfval  37637  eldiophb  37846  diophrw  37848  diophin  37862  rclexi  38448  rtrclex  38450  rtrclexi  38454  cnvrcl0  38458  dfrtrcl5  38462  dfrcl2  38492  fvmptiunrelexplb0da  38503  sblpnf  39035  fresin2  39872  limsupresuz  40453  limsupvaluz  40458  limsupvaluz2  40488  supcnvlimsup  40490  climrescn  40498  liminfresuz  40534  cncfuni  40617  dvresntr  40650  dvbdfbdioolem1  40661  itgiccshift  40713  itgperiod  40714  dirkercncflem2  40838  fourierdlem46  40886  fourierdlem48  40888  fourierdlem49  40889  fourierdlem58  40898  fourierdlem72  40912  fourierdlem74  40914  fourierdlem75  40915  fourierdlem81  40921  fourierdlem88  40928  fourierdlem89  40929  fourierdlem90  40930  fourierdlem91  40931  fourierdlem92  40932  fourierdlem103  40943  fourierdlem104  40944  fourierdlem112  40952  fouriersw  40965  voncmpl  41355  funcoressn  41727  f1oresf1orab  41831  idfusubc0  42393  idfusubc  42394  rngcval  42490  rnghmsubcsetclem1  42503  rngccat  42506  rngcid  42507  rngcidALTV  42519  rngcifuestrc  42525  funcrngcsetc  42526  funcrngcsetcALT  42527  ringcval  42536  rhmsubcsetclem1  42549  ringccat  42552  ringcid  42553  rhmsubcrngclem1  42555  rhmsubcrngc  42557  funcringcsetc  42563  funcringcsetcALTV2lem5  42568  ringcidALTV  42582  funcringcsetclem5ALTV  42591  rhmsubc  42618  rhmsubcALTVlem3  42634  aacllem  43078
  Copyright terms: Public domain W3C validator