Theorem resmpt 6041

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

This proof depends on syntax axioms:   → wi 4   ∧ wa 401   = wceq 1570   ∈ wcel 2147   ⊆ wss 3900  {copab 5170   ↦ cmpt 5189   ↾ cres 5657

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 1945  ax-6 2002  ax-7 2043  ax-8 2149  ax-9 2157  ax-10 2180  ax-12 2216  ax-ext 2735  ax-sep 5252  ax-pr 5395

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 2102  df-clab 2742  df-cleq 2755  df-clel 2839  df-rab 3417  df-v 3456  df-ss 3901  df-dif 4050  df-in 4094  df-un 4154  df-nul 4282  df-if 4486  df-sn 4589  df-pr 4591  df-op 4839  df-opab 5171  df-mpt 5190  df-xp 5661  df-rel 5662  df-res 5667

This theorem is used by:  resmpt3  6042  resmptf  6043  resmptd  6044  mptss  6046  elimampt  6047  fvresex  7996  f1stres  8049  f2ndres  8050  tposss  8272  dftpos2  8288  dftpos4  8290  resixpfo  8992  rlimresb  15761  lo1eq  15764  rlimeq  15765  fsumss  15920  isumclim3  15954  divcnvshft  16053  fprodss  16144  iprodclim3  16196  fprodefsum  16290  bitsf1ocnv  16643  conjsubg  19493  odf1o2  19817  sylow1lem2  19843  sylow2blem1  19864  gsumzres  20153  gsumzsplit  20171  gsumpr  20199  gsumzunsnd  20200  gsum2dlem2  20215  gsummptnn0fz  20230  dprd2da  20288  dpjidcl  20304  ablfac1b  20316  frlmsplit2  22109  psrass1lem  22271  coe1mul2lem2  22617  ofco2  22796  mdetralt  22953  mdetunilem9  22965  tgrest  23507  cmpfi  23756  fmss  24295  txflf  24355  tmdgsum  24444  tgpconncomp  24462  tsmssplit  24501  iscmet3lem3  25641  mbfss  25997  mbfadd  26012  mbfsub  26013  mbflimsup  26017  mbfmul  26077  itg2cnlem1  26112  ellimc2  26227  dvreslem  26259  dvres2lem  26260  dvidlem  26265  dvmptresicc  26266  dvcnp2  26270  dvmulbr  26289  dvcobr  26296  dvrec  26305  dvmptntr  26321  dvcnvlem  26326  lhop1lem  26363  lhop2  26365  itgparts  26397  itgsubstlem  26398  itgpowd  26400  plypf1  26561  taylthlem2  26731  pserdvlem2  26785  abelth  26798  pige3ALT  26878  efifo  26905  eff1olem  26906  dvlog2  27011  resqrtcn  27107  sqrtcn  27108  dvatan  27293  rlimcnp2  27324  xrlimcnp  27326  efrlim  27327  cxp2lim  27334  chpo1ub  27837  dchrisum0lem2a  27874  pnt2  27970  pnt  27971  wlknwwlksnbij  30507  ressnm  33595  gsummpt2d  33680  rmulccn  34630  xrge0mulc1cn  34643  gsumesum  34761  esumsnf  34766  esumcvg  34788  omsmon  35000  carsggect  35020  eulerpartlem1  35069  eulerpartgbij  35074  gsumnunsn  35243  cxpcncf1  35294  itgexpif  35305  reprpmtf1o  35325  elmsubrn  36460  divcnvlin  36676  mptsnunlem  38453  dissneqlem  38455  broucube  38764  mbfposadd  38777  itggt0cn  38800  ftc1anclem3  38805  ftc1anclem8  38810  dvasin  38814  dvacos  38815  areacirc  38823  sdclem2  38868  cncfres  38891  resopunitintvd  43268  resclunitintvd  43269  lcmineqlem2  43272  evlsbagval  43807  pwssplit4  44284  pwfi2f1o  44291  hbtlem6  44323  areaquad  44410  hashnzfzclim  45498  lhe4.4ex1a  45505  resmpti  46398  climresmpt  46874  dvcosre  47127  itgsinexplem1  47169  itgcoscmulx  47184  dirkeritg  47317  dirkercncflem2  47319  fourierdlem16  47338  fourierdlem21  47343  fourierdlem22  47344  fourierdlem57  47378  fourierdlem58  47379  fourierdlem62  47383  fourierdlem83  47404  fourierdlem111  47432  fouriersw  47446  0ome  47744