Theorem resmpt 6055

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

Syntax hints:   → wi 4   ∧ wa 395   = wceq 1540   ∈ wcel 2108   ⊆ wss 3951  {copab 5205   ↦ cmpt 5225   ↾ cres 5687

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 2007  ax-8 2110  ax-9 2118  ax-10 2141  ax-12 2177  ax-ext 2708  ax-sep 5296  ax-nul 5306  ax-pr 5432

This theorem depends on definitions:  df-bi 207  df-an 396  df-or 849  df-3an 1089  df-tru 1543  df-fal 1553  df-ex 1780  df-nf 1784  df-sb 2065  df-clab 2715  df-cleq 2729  df-clel 2816  df-rab 3437  df-v 3482  df-dif 3954  df-un 3956  df-in 3958  df-ss 3968  df-nul 4334  df-if 4526  df-sn 4627  df-pr 4629  df-op 4633  df-opab 5206  df-mpt 5226  df-xp 5691  df-rel 5692  df-res 5697

This theorem is referenced by:  resmpt3  6056  resmptf  6057  resmptd  6058  mptss  6060  elimampt  6061  fvresex  7984  f1stres  8038  f2ndres  8039  tposss  8252  dftpos2  8268  dftpos4  8270  resixpfo  8976  rlimresb  15601  lo1eq  15604  rlimeq  15605  fsumss  15761  isumclim3  15795  divcnvshft  15891  fprodss  15984  iprodclim3  16036  fprodefsum  16131  bitsf1ocnv  16481  conjsubg  19268  odf1o2  19591  sylow1lem2  19617  sylow2blem1  19638  gsumzres  19927  gsumzsplit  19945  gsumpr  19973  gsumzunsnd  19974  gsum2dlem2  19989  gsummptnn0fz  20004  dprd2da  20062  dpjidcl  20078  ablfac1b  20090  frlmsplit2  21793  psrass1lem  21952  coe1mul2lem2  22271  ofco2  22457  mdetralt  22614  mdetunilem9  22626  tgrest  23167  cmpfi  23416  fmss  23954  txflf  24014  tmdgsum  24103  tgpconncomp  24121  tsmssplit  24160  iscmet3lem3  25324  mbfss  25681  mbfadd  25696  mbfsub  25697  mbflimsup  25701  mbfmul  25761  itg2cnlem1  25796  ellimc2  25912  dvreslem  25944  dvres2lem  25945  dvidlem  25950  dvmptresicc  25951  dvcnp2  25955  dvcnp2OLD  25956  dvmulbr  25975  dvmulbrOLD  25976  dvcobr  25983  dvcobrOLD  25984  dvrec  25993  dvmptntr  26009  dvcnvlem  26014  lhop1lem  26052  lhop2  26054  itgparts  26088  itgsubstlem  26089  itgpowd  26091  plypf1  26251  taylthlem2  26416  taylthlem2OLD  26417  pserdvlem2  26472  abelth  26485  pige3ALT  26562  efifo  26589  eff1olem  26590  dvlog2  26695  resqrtcn  26792  sqrtcn  26793  dvatan  26978  rlimcnp2  27009  xrlimcnp  27011  efrlim  27012  efrlimOLD  27013  cxp2lim  27020  chpo1ub  27524  dchrisum0lem2a  27561  pnt2  27657  pnt  27658  wlknwwlksnbij  29908  ressnm  32949  gsummpt2d  33052  rmulccn  33927  xrge0mulc1cn  33940  gsumesum  34060  esumsnf  34065  esumcvg  34087  omsmon  34300  carsggect  34320  eulerpartlem1  34369  eulerpartgbij  34374  gsumnunsn  34556  cxpcncf1  34610  itgexpif  34621  reprpmtf1o  34641  elmsubrn  35533  divcnvlin  35733  mptsnunlem  37339  dissneqlem  37341  broucube  37661  mbfposadd  37674  itggt0cn  37697  ftc1anclem3  37702  ftc1anclem8  37707  dvasin  37711  dvacos  37712  areacirc  37720  sdclem2  37749  cncfres  37772  resopunitintvd  42027  resclunitintvd  42028  lcmineqlem2  42031  evlsbagval  42576  pwssplit4  43101  pwfi2f1o  43108  hbtlem6  43141  areaquad  43228  hashnzfzclim  44341  lhe4.4ex1a  44348  resmpti  45183  climresmpt  45674  dvcosre  45927  itgsinexplem1  45969  itgcoscmulx  45984  dirkeritg  46117  dirkercncflem2  46119  fourierdlem16  46138  fourierdlem21  46143  fourierdlem22  46144  fourierdlem57  46178  fourierdlem58  46179  fourierdlem62  46183  fourierdlem83  46204  fourierdlem111  46232  fouriersw  46246  0ome  46544