Theorem resmpt 6029

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

Syntax hints:   → wi 4   ∧ wa 395   = wceq 1540   ∈ wcel 2109   ⊆ wss 3931  {copab 5186   ↦ cmpt 5206   ↾ cres 5661

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1795  ax-4 1809  ax-5 1910  ax-6 1967  ax-7 2008  ax-8 2111  ax-9 2119  ax-10 2142  ax-12 2178  ax-ext 2708  ax-sep 5271  ax-nul 5281  ax-pr 5407

This theorem depends on definitions:  df-bi 207  df-an 396  df-or 848  df-3an 1088  df-tru 1543  df-fal 1553  df-ex 1780  df-nf 1784  df-sb 2066  df-clab 2715  df-cleq 2728  df-clel 2810  df-rab 3421  df-v 3466  df-dif 3934  df-un 3936  df-in 3938  df-ss 3948  df-nul 4314  df-if 4506  df-sn 4607  df-pr 4609  df-op 4613  df-opab 5187  df-mpt 5207  df-xp 5665  df-rel 5666  df-res 5671

This theorem is referenced by:  resmpt3  6030  resmptf  6031  resmptd  6032  mptss  6034  elimampt  6035  fvresex  7963  f1stres  8017  f2ndres  8018  tposss  8231  dftpos2  8247  dftpos4  8249  resixpfo  8955  rlimresb  15586  lo1eq  15589  rlimeq  15590  fsumss  15746  isumclim3  15780  divcnvshft  15876  fprodss  15969  iprodclim3  16021  fprodefsum  16116  bitsf1ocnv  16468  conjsubg  19238  odf1o2  19559  sylow1lem2  19585  sylow2blem1  19606  gsumzres  19895  gsumzsplit  19913  gsumpr  19941  gsumzunsnd  19942  gsum2dlem2  19957  gsummptnn0fz  19972  dprd2da  20030  dpjidcl  20046  ablfac1b  20058  frlmsplit2  21738  psrass1lem  21897  coe1mul2lem2  22210  ofco2  22394  mdetralt  22551  mdetunilem9  22563  tgrest  23102  cmpfi  23351  fmss  23889  txflf  23949  tmdgsum  24038  tgpconncomp  24056  tsmssplit  24095  iscmet3lem3  25247  mbfss  25604  mbfadd  25619  mbfsub  25620  mbflimsup  25624  mbfmul  25684  itg2cnlem1  25719  ellimc2  25835  dvreslem  25867  dvres2lem  25868  dvidlem  25873  dvmptresicc  25874  dvcnp2  25878  dvcnp2OLD  25879  dvmulbr  25898  dvmulbrOLD  25899  dvcobr  25906  dvcobrOLD  25907  dvrec  25916  dvmptntr  25932  dvcnvlem  25937  lhop1lem  25975  lhop2  25977  itgparts  26011  itgsubstlem  26012  itgpowd  26014  plypf1  26174  taylthlem2  26339  taylthlem2OLD  26340  pserdvlem2  26395  abelth  26408  pige3ALT  26486  efifo  26513  eff1olem  26514  dvlog2  26619  resqrtcn  26716  sqrtcn  26717  dvatan  26902  rlimcnp2  26933  xrlimcnp  26935  efrlim  26936  efrlimOLD  26937  cxp2lim  26944  chpo1ub  27448  dchrisum0lem2a  27485  pnt2  27581  pnt  27582  wlknwwlksnbij  29875  ressnm  32945  gsummpt2d  33048  rmulccn  33964  xrge0mulc1cn  33977  gsumesum  34095  esumsnf  34100  esumcvg  34122  omsmon  34335  carsggect  34355  eulerpartlem1  34404  eulerpartgbij  34409  gsumnunsn  34578  cxpcncf1  34632  itgexpif  34643  reprpmtf1o  34663  elmsubrn  35555  divcnvlin  35755  mptsnunlem  37361  dissneqlem  37363  broucube  37683  mbfposadd  37696  itggt0cn  37719  ftc1anclem3  37724  ftc1anclem8  37729  dvasin  37733  dvacos  37734  areacirc  37742  sdclem2  37771  cncfres  37794  resopunitintvd  42044  resclunitintvd  42045  lcmineqlem2  42048  evlsbagval  42564  pwssplit4  43088  pwfi2f1o  43095  hbtlem6  43128  areaquad  43215  hashnzfzclim  44321  lhe4.4ex1a  44328  resmpti  45182  climresmpt  45668  dvcosre  45921  itgsinexplem1  45963  itgcoscmulx  45978  dirkeritg  46111  dirkercncflem2  46113  fourierdlem16  46132  fourierdlem21  46137  fourierdlem22  46138  fourierdlem57  46172  fourierdlem58  46173  fourierdlem62  46177  fourierdlem83  46198  fourierdlem111  46226  fouriersw  46240  0ome  46538