Theorem resmpt 5651

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

Syntax hints:   → wi 4   ∧ wa 384   = wceq 1637   ∈ wcel 2158   ⊆ wss 3766  {copab 4902   ↦ cmpt 4919   ↾ cres 5310

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1880  ax-4 1897  ax-5 2004  ax-6 2070  ax-7 2106  ax-9 2167  ax-10 2187  ax-11 2203  ax-12 2216  ax-13 2422  ax-ext 2784  ax-sep 4971  ax-nul 4980  ax-pr 5093

This theorem depends on definitions:  df-bi 198  df-an 385  df-or 866  df-3an 1102  df-tru 1641  df-ex 1860  df-nf 1865  df-sb 2063  df-clab 2792  df-cleq 2798  df-clel 2801  df-nfc 2936  df-rab 3104  df-v 3392  df-dif 3769  df-un 3771  df-in 3773  df-ss 3780  df-nul 4114  df-if 4277  df-sn 4368  df-pr 4370  df-op 4374  df-opab 4903  df-mpt 4920  df-xp 5314  df-rel 5315  df-res 5320

This theorem is referenced by:  resmpt3  5652  resmptf  5653  resmptd  5654  mptss  5656  fvresex  7366  f1stres  7419  f2ndres  7420  tposss  7585  dftpos2  7601  dftpos4  7603  resixpfo  8180  rlimresb  14515  lo1eq  14518  rlimeq  14519  fsumss  14675  isumclim3  14709  divcnvshft  14805  fprodss  14895  iprodclim3  14947  fprodefsum  15041  bitsf1ocnv  15381  conjsubg  17890  psgnunilem5  18111  odf1o2  18185  sylow1lem2  18211  sylow2blem1  18232  gsumzres  18507  gsumzsplit  18524  gsumzunsnd  18552  gsum2dlem2  18567  gsummptnn0fz  18579  gsummptnn0fzOLD  18580  dprd2da  18639  dpjidcl  18655  ablfac1b  18667  psrass1lem  19582  coe1mul2lem2  19842  frlmsplit2  20318  ofco2  20464  mdetralt  20621  mdetunilem9  20633  tgrest  21173  cmpfi  21421  cnmptid  21674  fmss  21959  txflf  22019  tmdgsum  22108  tgpconncomp  22125  tsmssplit  22164  iscmet3lem3  23296  mbfss  23623  mbfadd  23638  mbfsub  23639  mbflimsup  23643  mbfmul  23703  itg2cnlem1  23738  ellimc2  23851  dvreslem  23883  dvres2lem  23884  dvidlem  23889  dvcnp2  23893  dvmulbr  23912  dvcobr  23919  dvrec  23928  dvmptntr  23944  dvcnvlem  23949  lhop1lem  23986  lhop2  23988  itgparts  24020  itgsubstlem  24021  tdeglem4  24030  plypf1  24178  taylthlem2  24338  pserdvlem2  24392  abelth  24405  pige3  24480  efifo  24504  eff1olem  24505  dvlog2  24609  resqrtcn  24700  sqrtcn  24701  dvatan  24872  rlimcnp2  24903  xrlimcnp  24905  efrlim  24906  cxp2lim  24913  chpo1ub  25379  dchrisum0lem2a  25416  pnt2  25512  pnt  25513  wlknwwlksnbij  27015  clwlknf1oclwwlknlem3  27243  elimampt  29762  ressnm  29973  gsummpt2d  30103  rmulccn  30296  xrge0mulc1cn  30309  gsumesum  30443  esumsnf  30448  esumcvg  30470  omsmon  30682  carsggect  30702  eulerpartlem1  30751  eulerpartgbij  30756  gsumnunsn  30937  cxpcncf1  30995  itgexpif  31006  reprpmtf1o  31026  elmsubrn  31745  divcnvlin  31937  mptsnunlem  33499  dissneqlem  33501  broucube  33753  mbfposadd  33766  itggt0cn  33791  ftc1anclem3  33796  ftc1anclem8  33801  dvasin  33805  dvacos  33806  areacirc  33814  sdclem2  33846  cncfres  33872  pwssplit4  38157  pwfi2f1o  38164  hbtlem6  38197  itgpowd  38297  areaquad  38299  hashnzfzclim  39018  lhe4.4ex1a  39025  resmpti  39845  climresmpt  40368  dvcosre  40603  dvmptresicc  40611  itgsinexplem1  40646  itgcoscmulx  40661  dirkeritg  40795  dirkercncflem2  40797  fourierdlem16  40816  fourierdlem21  40821  fourierdlem22  40822  fourierdlem57  40856  fourierdlem58  40857  fourierdlem62  40861  fourierdlem83  40882  fourierdlem111  40910  fouriersw  40924  0ome  41222  gsumpr  42704