Theorem resmpt 5369

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

Syntax hints:   → wi 4   ∧ wa 383   = wceq 1475   ∈ wcel 1977   ⊆ wss 3540  {copab 4642   ↦ cmpt 4643   ↾ cres 5040

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1713  ax-4 1728  ax-5 1827  ax-6 1875  ax-7 1922  ax-9 1986  ax-10 2006  ax-11 2021  ax-12 2034  ax-13 2234  ax-ext 2590  ax-sep 4709  ax-nul 4717  ax-pr 4833

This theorem depends on definitions:  df-bi 196  df-or 384  df-an 385  df-3an 1033  df-tru 1478  df-ex 1696  df-nf 1701  df-sb 1868  df-clab 2597  df-cleq 2603  df-clel 2606  df-nfc 2740  df-rab 2905  df-v 3175  df-dif 3543  df-un 3545  df-in 3547  df-ss 3554  df-nul 3875  df-if 4037  df-sn 4126  df-pr 4128  df-op 4132  df-opab 4644  df-mpt 4645  df-xp 5044  df-rel 5045  df-res 5050

This theorem is referenced by:  resmpt3  5370  resmptd  5371  mptss  5373  fvresex  7032  f1stres  7081  f2ndres  7082  tposss  7240  dftpos2  7256  dftpos4  7258  resixpfo  7832  rlimresb  14144  lo1eq  14147  rlimeq  14148  fsumss  14303  isumclim3  14332  divcnvshft  14426  fprodss  14517  iprodclim3  14570  fprodefsum  14664  bitsf1ocnv  15004  conjsubg  17515  psgnunilem5  17737  odf1o2  17811  sylow1lem2  17837  sylow2blem1  17858  gsumzres  18133  gsumzsplit  18150  gsumzunsnd  18178  gsum2dlem2  18193  gsummptnn0fz  18205  dprd2da  18264  dpjidcl  18280  ablfac1b  18292  psrass1lem  19198  coe1mul2lem2  19459  frlmsplit2  19931  ofco2  20076  mdetralt  20233  mdetunilem9  20245  tgrest  20773  cmpfi  21021  cnmptid  21274  fmss  21560  txflf  21620  tmdgsum  21709  tgpconcomp  21726  tsmssplit  21765  iscmet3lem3  22896  mbfss  23219  mbfadd  23234  mbfsub  23235  mbflimsup  23239  mbfmul  23299  itg2cnlem1  23334  ellimc2  23447  dvreslem  23479  dvres2lem  23480  dvidlem  23485  dvcnp2  23489  dvmulbr  23508  dvcobr  23515  dvrec  23524  dvmptntr  23540  dvcnvlem  23543  lhop1lem  23580  lhop2  23582  itgparts  23614  itgsubstlem  23615  tdeglem4  23624  plypf1  23772  taylthlem2  23932  pserdvlem2  23986  abelth  23999  pige3  24073  efifo  24097  eff1olem  24098  dvlog2  24199  resqrtcn  24290  sqrtcn  24291  dvatan  24462  rlimcnp2  24493  xrlimcnp  24495  efrlim  24496  cxp2lim  24503  chpo1ub  24969  dchrisum0lem2a  25006  pnt2  25102  pnt  25103  resmptf  28838  ressnm  28982  gsummpt2d  29112  rmulccn  29302  xrge0mulc1cn  29315  gsumesum  29448  esumsnf  29453  esumcvg  29475  omsmon  29687  carsggect  29707  eulerpartlem1  29756  eulerpartgbij  29761  gsumnunsn  29942  elmsubrn  30679  divcnvlin  30871  mptsnunlem  32361  dissneqlem  32363  broucube  32613  mbfposadd  32627  itggt0cn  32652  ftc1anclem3  32657  ftc1anclem8  32662  dvasin  32666  dvacos  32667  areacirc  32675  sdclem2  32708  cncfres  32734  pwssplit4  36677  pwfi2f1o  36684  hbtlem6  36718  itgpowd  36819  areaquad  36821  hashnzfzclim  37543  lhe4.4ex1a  37550  resmpti  38354  climresmpt  38726  dvcosre  38799  dvmptresicc  38809  itgsinexplem1  38845  itgcoscmulx  38861  dirkeritg  38995  dirkercncflem2  38997  fourierdlem16  39016  fourierdlem21  39021  fourierdlem22  39022  fourierdlem57  39056  fourierdlem58  39057  fourierdlem62  39061  fourierdlem83  39082  fourierdlem111  39110  fouriersw  39124  0ome  39419  gsumpr  41932