Theorem resmpt 6037

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 6036	. 2 ⊢ (𝐵 ⊆ 𝐴 → ({⟨𝑥, 𝑦⟩ ∣ (𝑥 ∈ 𝐴 ∧ 𝑦 = 𝐶)} ↾ 𝐵) = {⟨𝑥, 𝑦⟩ ∣ (𝑥 ∈ 𝐵 ∧ 𝑦 = 𝐶)})
2		df-mpt 5191	. . 3 ⊢ (𝑥 ∈ 𝐴 ↦ 𝐶) = {⟨𝑥, 𝑦⟩ ∣ (𝑥 ∈ 𝐴 ∧ 𝑦 = 𝐶)}
3	2	reseq1i 5972	. 2 ⊢ ((𝑥 ∈ 𝐴 ↦ 𝐶) ↾ 𝐵) = ({⟨𝑥, 𝑦⟩ ∣ (𝑥 ∈ 𝐴 ∧ 𝑦 = 𝐶)} ↾ 𝐵)
4		df-mpt 5191	. 2 ⊢ (𝑥 ∈ 𝐵 ↦ 𝐶) = {⟨𝑥, 𝑦⟩ ∣ (𝑥 ∈ 𝐵 ∧ 𝑦 = 𝐶)}
5	1, 3, 4	3eqtr4g 2822	1 ⊢ (𝐵 ⊆ 𝐴 → ((𝑥 ∈ 𝐴 ↦ 𝐶) ↾ 𝐵) = (𝑥 ∈ 𝐵 ↦ 𝐶))

This proof depends on syntax axioms:   → wi 4   ∧ wa 401   = wceq 1570   ∈ wcel 2145   ⊆ wss 3902  {copab 5171   ↦ cmpt 5190   ↾ cres 5661

This proof depends on axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1828  ax-4 1842  ax-5 1943  ax-6 2000  ax-7 2041  ax-8 2147  ax-9 2155  ax-10 2178  ax-12 2215  ax-ext 2734  ax-sep 5255  ax-pr 5402

This proof depends on definitions:  df-bi 210  df-an 402  df-or 862  df-3an 1105  df-tru 1573  df-fal 1583  df-ex 1813  df-nf 1817  df-sb 2100  df-clab 2741  df-cleq 2754  df-clel 2837  df-rab 3415  df-v 3455  df-dif 3905  df-un 3907  df-in 3909  df-ss 3919  df-nul 4283  df-if 4486  df-sn 4588  df-pr 4590  df-op 4594  df-opab 5172  df-mpt 5191  df-xp 5665  df-rel 5666  df-res 5671

This theorem is used by:  resmpt3  6038  resmptf  6039  resmptd  6040  mptss  6042  elimampt  6043  fvresex  7961  f1stres  8014  f2ndres  8015  tposss  8229  dftpos2  8245  dftpos4  8247  resixpfo  8947  rlimresb  15656  lo1eq  15659  rlimeq  15660  fsumss  15815  isumclim3  15849  divcnvshft  15948  fprodss  16041  iprodclim3  16093  fprodefsum  16187  bitsf1ocnv  16540  conjsubg  19383  odf1o2  19706  sylow1lem2  19732  sylow2blem1  19753  gsumzres  20042  gsumzsplit  20060  gsumpr  20088  gsumzunsnd  20089  gsum2dlem2  20104  gsummptnn0fz  20119  dprd2da  20177  dpjidcl  20193  ablfac1b  20205  frlmsplit2  21992  psrass1lem  22154  coe1mul2lem2  22500  ofco2  22679  mdetralt  22836  mdetunilem9  22848  tgrest  23390  cmpfi  23639  fmss  24178  txflf  24238  tmdgsum  24327  tgpconncomp  24345  tsmssplit  24384  iscmet3lem3  25524  mbfss  25880  mbfadd  25895  mbfsub  25896  mbflimsup  25900  mbfmul  25960  itg2cnlem1  25995  ellimc2  26111  dvreslem  26143  dvres2lem  26144  dvidlem  26149  dvmptresicc  26150  dvcnp2  26154  dvmulbr  26173  dvcobr  26180  dvrec  26189  dvmptntr  26205  dvcnvlem  26210  lhop1lem  26247  lhop2  26249  itgparts  26281  itgsubstlem  26282  itgpowd  26284  plypf1  26445  taylthlem2  26617  pserdvlem2  26671  abelth  26684  pige3ALT  26765  efifo  26792  eff1olem  26793  dvlog2  26898  resqrtcn  26994  sqrtcn  26995  dvatan  27180  rlimcnp2  27211  xrlimcnp  27213  efrlim  27214  cxp2lim  27221  chpo1ub  27724  dchrisum0lem2a  27761  pnt2  27857  pnt  27858  wlknwwlksnbij  30364  ressnm  33412  gsummpt2d  33497  rmulccn  34446  xrge0mulc1cn  34459  gsumesum  34577  esumsnf  34582  esumcvg  34604  omsmon  34817  carsggect  34837  eulerpartlem1  34886  eulerpartgbij  34891  gsumnunsn  35060  cxpcncf1  35111  itgexpif  35122  reprpmtf1o  35142  elmsubrn  36115  divcnvlin  36320  mptsnunlem  38100  dissneqlem  38102  broucube  38411  mbfposadd  38424  itggt0cn  38447  ftc1anclem3  38452  ftc1anclem8  38457  dvasin  38461  dvacos  38462  areacirc  38470  sdclem2  38500  cncfres  38523  resopunitintvd  42900  resclunitintvd  42901  lcmineqlem2  42904  evlsbagval  43440  pwssplit4  43938  pwfi2f1o  43945  hbtlem6  43978  areaquad  44065  hashnzfzclim  45154  lhe4.4ex1a  45161  resmpti  46018  climresmpt  46495  dvcosre  46748  itgsinexplem1  46790  itgcoscmulx  46805  dirkeritg  46938  dirkercncflem2  46940  fourierdlem16  46959  fourierdlem21  46964  fourierdlem22  46965  fourierdlem57  46999  fourierdlem58  47000  fourierdlem62  47004  fourierdlem83  47025  fourierdlem111  47053  fouriersw  47067  0ome  47365