Theorem resmpt 5905

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

Syntax hints:   → wi 4   ∧ wa 398   = wceq 1537   ∈ wcel 2114   ⊆ wss 3936  {copab 5128   ↦ cmpt 5146   ↾ cres 5557

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1796  ax-4 1810  ax-5 1911  ax-6 1970  ax-7 2015  ax-8 2116  ax-9 2124  ax-10 2145  ax-11 2161  ax-12 2177  ax-ext 2793  ax-sep 5203  ax-nul 5210  ax-pr 5330

This theorem depends on definitions:  df-bi 209  df-an 399  df-or 844  df-3an 1085  df-tru 1540  df-ex 1781  df-nf 1785  df-sb 2070  df-clab 2800  df-cleq 2814  df-clel 2893  df-nfc 2963  df-rab 3147  df-v 3496  df-dif 3939  df-un 3941  df-in 3943  df-ss 3952  df-nul 4292  df-if 4468  df-sn 4568  df-pr 4570  df-op 4574  df-opab 5129  df-mpt 5147  df-xp 5561  df-rel 5562  df-res 5567

This theorem is referenced by:  resmpt3  5906  resmptf  5907  resmptd  5908  mptss  5910  fvresex  7661  f1stres  7713  f2ndres  7714  tposss  7893  dftpos2  7909  dftpos4  7911  resixpfo  8500  rlimresb  14922  lo1eq  14925  rlimeq  14926  fsumss  15082  isumclim3  15114  divcnvshft  15210  fprodss  15302  iprodclim3  15354  fprodefsum  15448  bitsf1ocnv  15793  conjsubg  18390  odf1o2  18698  sylow1lem2  18724  sylow2blem1  18745  gsumzres  19029  gsumzsplit  19047  gsumpr  19075  gsumzunsnd  19076  gsum2dlem2  19091  gsummptnn0fz  19106  dprd2da  19164  dpjidcl  19180  ablfac1b  19192  psrass1lem  20157  coe1mul2lem2  20436  frlmsplit2  20917  ofco2  21060  mdetralt  21217  mdetunilem9  21229  tgrest  21767  cmpfi  22016  fmss  22554  txflf  22614  tmdgsum  22703  tgpconncomp  22721  tsmssplit  22760  iscmet3lem3  23893  mbfss  24247  mbfadd  24262  mbfsub  24263  mbflimsup  24267  mbfmul  24327  itg2cnlem1  24362  ellimc2  24475  dvreslem  24507  dvres2lem  24508  dvidlem  24513  dvcnp2  24517  dvmulbr  24536  dvcobr  24543  dvrec  24552  dvmptntr  24568  dvcnvlem  24573  lhop1lem  24610  lhop2  24612  itgparts  24644  itgsubstlem  24645  tdeglem4  24654  plypf1  24802  taylthlem2  24962  pserdvlem2  25016  abelth  25029  pige3ALT  25105  efifo  25131  eff1olem  25132  dvlog2  25236  resqrtcn  25330  sqrtcn  25331  dvatan  25513  rlimcnp2  25544  xrlimcnp  25546  efrlim  25547  cxp2lim  25554  chpo1ub  26056  dchrisum0lem2a  26093  pnt2  26189  pnt  26190  wlknwwlksnbij  27666  elimampt  30383  ressnm  30638  gsummpt2d  30687  rmulccn  31171  xrge0mulc1cn  31184  gsumesum  31318  esumsnf  31323  esumcvg  31345  omsmon  31556  carsggect  31576  eulerpartlem1  31625  eulerpartgbij  31630  gsumnunsn  31811  cxpcncf1  31866  itgexpif  31877  reprpmtf1o  31897  elmsubrn  32775  divcnvlin  32964  mptsnunlem  34622  dissneqlem  34624  broucube  34941  mbfposadd  34954  itggt0cn  34979  ftc1anclem3  34984  ftc1anclem8  34989  dvasin  34993  dvacos  34994  areacirc  35002  sdclem2  35032  cncfres  35058  pwssplit4  39709  pwfi2f1o  39716  hbtlem6  39749  itgpowd  39841  areaquad  39843  hashnzfzclim  40674  lhe4.4ex1a  40681  resmpti  41454  climresmpt  41960  dvcosre  42216  dvmptresicc  42224  itgsinexplem1  42259  itgcoscmulx  42274  dirkeritg  42407  dirkercncflem2  42409  fourierdlem16  42428  fourierdlem21  42433  fourierdlem22  42434  fourierdlem57  42468  fourierdlem58  42469  fourierdlem62  42473  fourierdlem83  42494  fourierdlem111  42522  fouriersw  42536  0ome  42831