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

Theorem resmptd 5671
Description: Restriction of the mapping operation, deduction form. (Contributed by Glauco Siliprandi, 11-Dec-2019.)
Hypothesis
Ref Expression
resmptd.b (𝜑𝐵𝐴)
Assertion
Ref Expression
resmptd (𝜑 → ((𝑥𝐴𝐶) ↾ 𝐵) = (𝑥𝐵𝐶))
Distinct variable groups:   𝑥,𝐴   𝑥,𝐵
Allowed substitution hints:   𝜑(𝑥)   𝐶(𝑥)

Proof of Theorem resmptd
StepHypRef Expression
1 resmptd.b . 2 (𝜑𝐵𝐴)
2 resmpt 5668 . 2 (𝐵𝐴 → ((𝑥𝐴𝐶) ↾ 𝐵) = (𝑥𝐵𝐶))
31, 2syl 17 1 (𝜑 → ((𝑥𝐴𝐶) ↾ 𝐵) = (𝑥𝐵𝐶))
Colors of variables: wff setvar class
Syntax hints:  wi 4   = wceq 1637  wss 3780  cmpt 4934  cres 5326
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1877  ax-4 1894  ax-5 2001  ax-6 2069  ax-7 2105  ax-9 2166  ax-10 2186  ax-11 2202  ax-12 2215  ax-13 2422  ax-ext 2795  ax-sep 4988  ax-nul 4996  ax-pr 5109
This theorem depends on definitions:  df-bi 198  df-an 385  df-or 866  df-3an 1102  df-tru 1641  df-ex 1860  df-nf 1864  df-sb 2062  df-clab 2804  df-cleq 2810  df-clel 2813  df-nfc 2948  df-rab 3116  df-v 3404  df-dif 3783  df-un 3785  df-in 3787  df-ss 3794  df-nul 4128  df-if 4291  df-sn 4382  df-pr 4384  df-op 4388  df-opab 4918  df-mpt 4935  df-xp 5330  df-rel 5331  df-res 5336
This theorem is referenced by:  f1ossf1o  6628  oacomf1olem  7891  cantnfres  8831  rlimres2  14535  lo1res2  14536  o1res2  14537  fsumss  14699  fprodss  14919  conjsubgen  17915  gsumsplit2  18550  gsum2d  18592  dmdprdsplitlem  18658  dprd2dlem1  18662  psrlidm  19632  psrridm  19633  mplmonmul  19693  mplcoe1  19694  mplcoe5  19697  evlsval2  19748  mdetunilem9  20658  cmpfi  21446  ptpjopn  21650  xkoptsub  21692  xkopjcn  21694  cnmpt1res  21714  subgntr  22144  opnsubg  22145  clsnsg  22147  snclseqg  22153  tsmsxplem1  22190  imasdsf1olem  22412  subgnm  22671  cphsscph  23283  mbfss  23650  mbflimsup  23670  mbfmullem2  23728  iblss  23808  limcres  23887  dvaddbr  23938  dvmulbr  23939  dvcmulf  23945  dvmptres3  23956  dvmptres2  23962  dvmptntr  23971  lhop2  24015  lhop  24016  dvfsumle  24021  dvfsumabs  24023  dvfsumlem2  24027  ftc2ditglem  24045  itgsubstlem  24048  mdegfval  24059  psercn2  24414  psercn  24417  abelth  24432  abelth2  24433  efrlim  24933  jensenlem2  24951  lgamcvg2  25018  pntrsumo1  25491  eucrct2eupth  27441  rabfodom  29692  poimirlem16  33757  poimirlem19  33760  poimirlem30  33771  ftc1anclem8  33823  ftc2nc  33825  areacirclem2  33832  hbtlem6  38218  itgpowd  38318  radcnvrat  39031  disjf1o  39885  cncfmptss  40317  limsupvaluzmpt  40447  supcnvlimsupmpt  40471  dvmptresicc  40632  dvnprodlem1  40659  iblsplit  40679  itgcoscmulx  40682  itgiccshift  40693  itgperiod  40694  itgsbtaddcnst  40695  dirkercncflem2  40818  dirkercncflem4  40820  fourierdlem28  40849  fourierdlem40  40861  fourierdlem58  40878  fourierdlem74  40894  fourierdlem75  40895  fourierdlem76  40896  fourierdlem78  40898  fourierdlem80  40900  fourierdlem81  40901  fourierdlem84  40904  fourierdlem85  40905  fourierdlem90  40910  fourierdlem93  40913  fourierdlem101  40921  fourierdlem111  40931  sge0lessmpt  41113  sge0gerpmpt  41116  sge0resrnlem  41117  sge0ssrempt  41119  sge0ltfirpmpt  41122  sge0iunmptlemre  41129  sge0lefimpt  41137  sge0ltfirpmpt2  41140  sge0pnffigtmpt  41154  ismeannd  41181  omeiunltfirp  41233  caratheodorylem2  41241  sssmfmpt  41459  funcrngcsetc  42584  funcrngcsetcALT  42585  funcringcsetc  42621  fdmdifeqresdif  42706  gsumsplit2f  42729
  Copyright terms: Public domain W3C validator