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

Theorem resmptd 5602
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 5599 . 2 (𝐵𝐴 → ((𝑥𝐴𝐶) ↾ 𝐵) = (𝑥𝐵𝐶))
31, 2syl 17 1 (𝜑 → ((𝑥𝐴𝐶) ↾ 𝐵) = (𝑥𝐵𝐶))
Colors of variables: wff setvar class
Syntax hints:  wi 4   = wceq 1624  wss 3707  cmpt 4873  cres 5260
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1863  ax-4 1878  ax-5 1980  ax-6 2046  ax-7 2082  ax-9 2140  ax-10 2160  ax-11 2175  ax-12 2188  ax-13 2383  ax-ext 2732  ax-sep 4925  ax-nul 4933  ax-pr 5047
This theorem depends on definitions:  df-bi 197  df-or 384  df-an 385  df-3an 1074  df-tru 1627  df-ex 1846  df-nf 1851  df-sb 2039  df-clab 2739  df-cleq 2745  df-clel 2748  df-nfc 2883  df-rab 3051  df-v 3334  df-dif 3710  df-un 3712  df-in 3714  df-ss 3721  df-nul 4051  df-if 4223  df-sn 4314  df-pr 4316  df-op 4320  df-opab 4857  df-mpt 4874  df-xp 5264  df-rel 5265  df-res 5270
This theorem is referenced by:  oacomf1olem  7805  cantnfres  8739  rlimres2  14483  lo1res2  14484  o1res2  14485  fsumss  14647  fprodss  14869  conjsubgen  17886  gsumsplit2  18521  gsum2d  18563  dmdprdsplitlem  18628  dprd2dlem1  18632  psrlidm  19597  psrridm  19598  mplmonmul  19658  mplcoe1  19659  mplcoe5  19662  evlsval2  19714  mdetunilem9  20620  cmpfi  21405  ptpjopn  21609  xkoptsub  21651  xkopjcn  21653  cnmpt1res  21673  subgntr  22103  opnsubg  22104  clsnsg  22106  snclseqg  22112  tsmsxplem1  22149  imasdsf1olem  22371  subgnm  22630  mbfss  23604  mbflimsup  23624  mbfmullem2  23682  iblss  23762  limcres  23841  dvaddbr  23892  dvmulbr  23893  dvcmulf  23899  dvmptres3  23910  dvmptres2  23916  dvmptntr  23925  lhop2  23969  lhop  23970  dvfsumle  23975  dvfsumabs  23977  dvfsumlem2  23981  ftc2ditglem  23999  itgsubstlem  24002  mdegfval  24013  psercn2  24368  psercn  24371  abelth  24386  abelth2  24387  efrlim  24887  jensenlem2  24905  lgamcvg2  24972  pntrsumo1  25445  eucrct2eupth  27389  rabfodom  29643  poimirlem16  33730  poimirlem19  33733  poimirlem30  33744  ftc1anclem8  33797  ftc2nc  33799  areacirclem2  33806  hbtlem6  38193  itgpowd  38294  radcnvrat  39007  disjf1o  39869  cncfmptss  40314  limsupvaluzmpt  40444  supcnvlimsupmpt  40468  dvmptresicc  40629  dvnprodlem1  40656  iblsplit  40677  itgcoscmulx  40680  itgiccshift  40691  itgperiod  40692  itgsbtaddcnst  40693  dirkercncflem2  40816  dirkercncflem4  40818  fourierdlem28  40847  fourierdlem40  40859  fourierdlem58  40876  fourierdlem74  40892  fourierdlem75  40893  fourierdlem76  40894  fourierdlem78  40896  fourierdlem80  40898  fourierdlem81  40899  fourierdlem84  40902  fourierdlem85  40903  fourierdlem90  40908  fourierdlem93  40911  fourierdlem101  40919  fourierdlem111  40929  sge0lessmpt  41111  sge0gerpmpt  41114  sge0resrnlem  41115  sge0ssrempt  41117  sge0ltfirpmpt  41120  sge0iunmptlemre  41127  sge0lefimpt  41135  sge0ltfirpmpt2  41138  sge0pnffigtmpt  41152  ismeannd  41179  omeiunltfirp  41231  caratheodorylem2  41239  sssmfmpt  41457  funcrngcsetc  42500  funcrngcsetcALT  42501  funcringcsetc  42537  fdmdifeqresdif  42622  gsumsplit2f  42645
  Copyright terms: Public domain W3C validator