Theorem resmpt 6041

Description: Restriction of the mapping operation. (Contributed by Mario Carneiro, 15-Jul-2013.)

Assertion

Ref	Expression
resmpt	⊢ (𝐵 ⊆ 𝐴 → ((𝑥 ∈ 𝐴 ↦ 𝐶) ↾ 𝐵) = (𝑥 ∈ 𝐵 ↦ 𝐶))

Distinct variable groups:   𝑥,𝐴   𝑥,𝐵

Allowed substitution hint:   𝐶(𝑥)

Proof of Theorem resmpt

Dummy variable 𝑦 is distinct from all other variables.

Step	Hyp	Ref	Expression
1		resopab2 6040	. 2 ⊢ (𝐵 ⊆ 𝐴 → ({⟨𝑥, 𝑦⟩ ∣ (𝑥 ∈ 𝐴 ∧ 𝑦 = 𝐶)} ↾ 𝐵) = {⟨𝑥, 𝑦⟩ ∣ (𝑥 ∈ 𝐵 ∧ 𝑦 = 𝐶)})
2		df-mpt 5194	. . 3 ⊢ (𝑥 ∈ 𝐴 ↦ 𝐶) = {⟨𝑥, 𝑦⟩ ∣ (𝑥 ∈ 𝐴 ∧ 𝑦 = 𝐶)}
3	2	reseq1i 5976	. 2 ⊢ ((𝑥 ∈ 𝐴 ↦ 𝐶) ↾ 𝐵) = ({⟨𝑥, 𝑦⟩ ∣ (𝑥 ∈ 𝐴 ∧ 𝑦 = 𝐶)} ↾ 𝐵)
4		df-mpt 5194	. 2 ⊢ (𝑥 ∈ 𝐵 ↦ 𝐶) = {⟨𝑥, 𝑦⟩ ∣ (𝑥 ∈ 𝐵 ∧ 𝑦 = 𝐶)}
5	1, 3, 4	3eqtr4g 2823	1 ⊢ (𝐵 ⊆ 𝐴 → ((𝑥 ∈ 𝐴 ↦ 𝐶) ↾ 𝐵) = (𝑥 ∈ 𝐵 ↦ 𝐶))

Syntax hints:   → wi 4   ∧ wa 400   = wceq 1570   ∈ wcel 2143   ⊆ wss 3906  {copab 5174   ↦ cmpt 5193   ↾ cres 5665

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1825  ax-4 1839  ax-5 1940  ax-6 1997  ax-7 2038  ax-8 2145  ax-9 2153  ax-10 2176  ax-12 2213  ax-ext 2735  ax-sep 5258  ax-pr 5406

This theorem depends on definitions:  df-bi 210  df-an 401  df-or 861  df-3an 1105  df-tru 1573  df-fal 1583  df-ex 1810  df-nf 1814  df-sb 2097  df-clab 2742  df-cleq 2755  df-clel 2838  df-rab 3417  df-v 3457  df-dif 3909  df-un 3911  df-in 3913  df-ss 3923  df-nul 4288  df-if 4489  df-sn 4591  df-pr 4593  df-op 4597  df-opab 5175  df-mpt 5194  df-xp 5669  df-rel 5670  df-res 5675

This theorem is referenced by:  resmpt3  6042  resmptf  6043  resmptd  6044  mptss  6046  elimampt  6047  fvresex  7958  f1stres  8011  f2ndres  8012  tposss  8224  dftpos2  8240  dftpos4  8242  resixpfo  8935  rlimresb  15618  lo1eq  15621  rlimeq  15622  fsumss  15778  isumclim3  15812  divcnvshft  15911  fprodss  16004  iprodclim3  16056  fprodefsum  16150  bitsf1ocnv  16503  conjsubg  19321  odf1o2  19644  sylow1lem2  19670  sylow2blem1  19691  gsumzres  19980  gsumzsplit  19998  gsumpr  20026  gsumzunsnd  20027  gsum2dlem2  20042  gsummptnn0fz  20057  dprd2da  20115  dpjidcl  20131  ablfac1b  20143  frlmsplit2  21904  psrass1lem  22064  coe1mul2lem2  22410  ofco2  22589  mdetralt  22746  mdetunilem9  22758  tgrest  23297  cmpfi  23546  fmss  24084  txflf  24144  tmdgsum  24233  tgpconncomp  24251  tsmssplit  24290  iscmet3lem3  25430  mbfss  25786  mbfadd  25801  mbfsub  25802  mbflimsup  25806  mbfmul  25866  itg2cnlem1  25901  ellimc2  26017  dvreslem  26049  dvres2lem  26050  dvidlem  26055  dvmptresicc  26056  dvcnp2  26060  dvmulbr  26079  dvcobr  26086  dvrec  26095  dvmptntr  26111  dvcnvlem  26116  lhop1lem  26153  lhop2  26155  itgparts  26187  itgsubstlem  26188  itgpowd  26190  plypf1  26350  taylthlem2  26515  pserdvlem2  26569  abelth  26582  pige3ALT  26663  efifo  26690  eff1olem  26691  dvlog2  26796  resqrtcn  26892  sqrtcn  26893  dvatan  27078  rlimcnp2  27109  xrlimcnp  27111  efrlim  27112  cxp2lim  27119  chpo1ub  27622  dchrisum0lem2a  27659  pnt2  27755  pnt  27756  wlknwwlksnbij  30215  ressnm  33262  gsummpt2d  33347  rmulccn  34296  xrge0mulc1cn  34309  gsumesum  34427  esumsnf  34432  esumcvg  34454  omsmon  34666  carsggect  34686  eulerpartlem1  34735  eulerpartgbij  34740  gsumnunsn  34909  cxpcncf1  34960  itgexpif  34971  reprpmtf1o  34991  elmsubrn  35998  divcnvlin  36203  mptsnunlem  37962  dissneqlem  37964  broucube  38283  mbfposadd  38296  itggt0cn  38319  ftc1anclem3  38324  ftc1anclem8  38329  dvasin  38333  dvacos  38334  areacirc  38342  sdclem2  38371  cncfres  38394  resopunitintvd  42771  resclunitintvd  42772  lcmineqlem2  42775  evlsbagval  43298  pwssplit4  43796  pwfi2f1o  43803  hbtlem6  43836  areaquad  43923  hashnzfzclim  45012  lhe4.4ex1a  45019  resmpti  45876  climresmpt  46353  dvcosre  46606  itgsinexplem1  46648  itgcoscmulx  46663  dirkeritg  46796  dirkercncflem2  46798  fourierdlem16  46817  fourierdlem21  46822  fourierdlem22  46823  fourierdlem57  46857  fourierdlem58  46858  fourierdlem62  46862  fourierdlem83  46883  fourierdlem111  46911  fouriersw  46925  0ome  47223