Theorem resmpt 6044

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

This proof depends on syntax axioms:   → wi 4   ∧ wa 401   = wceq 1570   ∈ wcel 2146   ⊆ wss 3908  {copab 5178   ↦ cmpt 5197   ↾ cres 5668

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 1943  ax-6 2000  ax-7 2041  ax-8 2148  ax-9 2156  ax-10 2179  ax-12 2216  ax-ext 2738  ax-sep 5262  ax-pr 5409

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 2100  df-clab 2745  df-cleq 2758  df-clel 2841  df-rab 3420  df-v 3460  df-dif 3911  df-un 3913  df-in 3915  df-ss 3925  df-nul 4290  df-if 4493  df-sn 4595  df-pr 4597  df-op 4601  df-opab 5179  df-mpt 5198  df-xp 5672  df-rel 5673  df-res 5678

This theorem is used by:  resmpt3  6045  resmptf  6046  resmptd  6047  mptss  6049  elimampt  6050  fvresex  7966  f1stres  8019  f2ndres  8020  tposss  8232  dftpos2  8248  dftpos4  8250  resixpfo  8943  rlimresb  15642  lo1eq  15645  rlimeq  15646  fsumss  15802  isumclim3  15836  divcnvshft  15935  fprodss  16028  iprodclim3  16080  fprodefsum  16174  bitsf1ocnv  16527  conjsubg  19351  odf1o2  19674  sylow1lem2  19700  sylow2blem1  19721  gsumzres  20010  gsumzsplit  20028  gsumpr  20056  gsumzunsnd  20057  gsum2dlem2  20072  gsummptnn0fz  20087  dprd2da  20145  dpjidcl  20161  ablfac1b  20173  frlmsplit2  21960  psrass1lem  22120  coe1mul2lem2  22466  ofco2  22645  mdetralt  22802  mdetunilem9  22814  tgrest  23353  cmpfi  23602  fmss  24140  txflf  24200  tmdgsum  24289  tgpconncomp  24307  tsmssplit  24346  iscmet3lem3  25486  mbfss  25842  mbfadd  25857  mbfsub  25858  mbflimsup  25862  mbfmul  25922  itg2cnlem1  25957  ellimc2  26073  dvreslem  26105  dvres2lem  26106  dvidlem  26111  dvmptresicc  26112  dvcnp2  26116  dvmulbr  26135  dvcobr  26142  dvrec  26151  dvmptntr  26167  dvcnvlem  26172  lhop1lem  26209  lhop2  26211  itgparts  26243  itgsubstlem  26244  itgpowd  26246  plypf1  26406  taylthlem2  26574  pserdvlem2  26628  abelth  26641  pige3ALT  26722  efifo  26749  eff1olem  26750  dvlog2  26855  resqrtcn  26951  sqrtcn  26952  dvatan  27137  rlimcnp2  27168  xrlimcnp  27170  efrlim  27171  cxp2lim  27178  chpo1ub  27681  dchrisum0lem2a  27718  pnt2  27814  pnt  27815  wlknwwlksnbij  30274  ressnm  33315  gsummpt2d  33400  rmulccn  34349  xrge0mulc1cn  34362  gsumesum  34480  esumsnf  34485  esumcvg  34507  omsmon  34720  carsggect  34740  eulerpartlem1  34789  eulerpartgbij  34794  gsumnunsn  34963  cxpcncf1  35014  itgexpif  35025  reprpmtf1o  35045  elmsubrn  36041  divcnvlin  36246  mptsnunlem  38025  dissneqlem  38027  broucube  38346  mbfposadd  38359  itggt0cn  38382  ftc1anclem3  38387  ftc1anclem8  38392  dvasin  38396  dvacos  38397  areacirc  38405  sdclem2  38434  cncfres  38457  resopunitintvd  42834  resclunitintvd  42835  lcmineqlem2  42838  evlsbagval  43359  pwssplit4  43857  pwfi2f1o  43864  hbtlem6  43897  areaquad  43984  hashnzfzclim  45073  lhe4.4ex1a  45080  resmpti  45937  climresmpt  46414  dvcosre  46667  itgsinexplem1  46709  itgcoscmulx  46724  dirkeritg  46857  dirkercncflem2  46859  fourierdlem16  46878  fourierdlem21  46883  fourierdlem22  46884  fourierdlem57  46918  fourierdlem58  46919  fourierdlem62  46923  fourierdlem83  46944  fourierdlem111  46972  fouriersw  46986  0ome  47284