Theorem resmpt 5314

Description: Restriction of the mapping operation. (Contributed by Mario Carneiro, 15-Jul-2013.)

Assertion

Ref	Expression
resmpt	|- ( B C_ A -> ( ( x e. A |-> C ) |` B ) = ( x e. B |-> C ) )

Distinct variable groups:   x, A   x, B

Allowed substitution hint:   C( x)

Proof of Theorem resmpt

Dummy variable y is distinct from all other variables.

Step	Hyp	Ref	Expression
1		resopab2 5313	. 2 |- ( B C_ A -> ( { <. x , y >. | ( x e. A /\ y = C ) } |` B ) = { <. x , y >. | ( x e. B /\ y = C ) } )
2		df-mpt 4500	. . 3 |- ( x e. A |-> C ) = { <. x , y >. | ( x e. A /\ y = C ) }
3	2	reseq1i 5260	. 2 |- ( ( x e. A |-> C ) |` B ) = ( { <. x , y >. | ( x e. A /\ y = C ) } |` B )
4		df-mpt 4500	. 2 |- ( x e. B |-> C ) = { <. x , y >. | ( x e. B /\ y = C ) }
5	1, 3, 4	3eqtr4g 2526	1 |- ( B C_ A -> ( ( x e. A |-> C ) |` B ) = ( x e. B |-> C ) )

Syntax hints:   -> wi 4   /\ wa 369   = wceq 1374   e. wcel 1762   C_ wss 3469   {copab 4497   |-> cmpt 4498   |` cres 4994

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1596  ax-4 1607  ax-5 1675  ax-6 1714  ax-7 1734  ax-9 1766  ax-10 1781  ax-11 1786  ax-12 1798  ax-13 1961  ax-ext 2438  ax-sep 4561  ax-nul 4569  ax-pr 4679

This theorem depends on definitions:  df-bi 185  df-or 370  df-an 371  df-3an 970  df-tru 1377  df-ex 1592  df-nf 1595  df-sb 1707  df-clab 2446  df-cleq 2452  df-clel 2455  df-nfc 2610  df-ne 2657  df-ral 2812  df-rex 2813  df-rab 2816  df-v 3108  df-dif 3472  df-un 3474  df-in 3476  df-ss 3483  df-nul 3779  df-if 3933  df-sn 4021  df-pr 4023  df-op 4027  df-opab 4499  df-mpt 4500  df-xp 4998  df-rel 4999  df-res 5004

This theorem is referenced by:  resmpt3  5315  resmptd  5316  fvresex  6747  f1stres  6796  f2ndres  6797  tposss  6946  dftpos2  6962  dftpos4  6964  oacomf1olem  7203  resixpfo  7497  cantnfres  8085  rlimres2  13333  lo1res2  13334  o1res2  13335  rlimresb  13337  lo1eq  13340  rlimeq  13341  fsumss  13496  isumclim3  13523  bitsf1ocnv  13942  conjsubg  16086  conjsubgen  16087  psgnunilem5  16308  odf1o2  16382  sylow1lem2  16408  sylow2blem1  16429  gsumzres  16698  gsumzresOLD  16702  gsumzsplit  16728  gsumzsplitOLD  16729  gsumsplit2  16732  gsumsplit2OLD  16733  gsumzunsnd  16766  gsum2dlem2  16782  gsum2d  16783  gsum2dOLD  16784  gsummptnn0fz  16798  dmdprdsplitlem  16867  dmdprdsplitlemOLD  16868  dprd2dlem1  16873  dprd2da  16874  dpjidcl  16890  dpjidclOLD  16897  ablfac1b  16904  psrass1lem  17793  psrlidm  17820  psrlidmOLD  17821  psrridm  17822  psrridmOLD  17823  mplmonmul  17890  mplcoe1  17891  mplcoe5  17895  mplcoe2OLD  17897  evlsval2  17953  coe1mul2lem2  18073  frlmsplit2  18563  ofco2  18713  mdetralt  18870  mdetunilem9  18882  tgrest  19419  cmpfi  19667  ptpjopn  19841  xkoptsub  19883  xkopjcn  19885  cnmptid  19890  cnmpt1res  19905  fmss  20175  txflf  20235  tmdgsum  20322  subgntr  20333  opnsubg  20334  clsnsg  20336  tgpconcomp  20339  snclseqg  20342  tsmssplit  20382  tsmsxplem1  20383  imasdsf1olem  20604  subgnm  20875  iscmet3lem3  21457  mbfss  21781  mbfadd  21796  mbfsub  21797  mbflimsup  21801  mbfmullem2  21859  mbfmul  21861  itg2cnlem1  21896  iblss  21939  ellimc2  22009  limcres  22018  dvreslem  22041  dvres2lem  22042  dvidlem  22047  dvcnp2  22051  dvaddbr  22069  dvmulbr  22070  dvcmulf  22076  dvcobr  22077  dvrec  22086  dvmptres3  22087  dvmptres2  22093  dvmptntr  22102  dvcnvlem  22105  lhop1lem  22142  lhop2  22144  lhop  22145  dvfsumle  22150  dvfsumabs  22152  dvfsumlem2  22156  ftc2ditglem  22174  itgparts  22176  itgsubstlem  22177  tdeglem4  22186  mdegfval  22188  plypf1  22337  taylthlem2  22496  psercn2  22545  psercn  22548  pserdvlem2  22550  abelth  22563  abelth2  22564  pige3  22636  efifo  22660  eff1olem  22661  dvlog2  22755  resqrcn  22844  sqrcn  22845  dvatan  22987  rlimcnp2  23017  xrlimcnp  23019  efrlim  23020  cxp2lim  23027  jensenlem2  23038  chpo1ub  23386  dchrisum0lem2a  23423  pntrsumo1  23471  pnt2  23519  pnt  23520  efghgrp  24901  resmptf  27019  ressnm  27151  rmulccn  27396  xrge0mulc1cn  27409  gsumesum  27557  esumsn  27562  esumcvg  27582  omsmon  27757  eulerpartlem1  27796  eulerpartgbij  27801  gsumnunsn  27983  lgamcvg2  28087  divcnvshft  28444  divcnvlin  28445  fprodss  28507  fprodefsum  28531  iprodclim3  28546  mbfposadd  29490  itggt0cn  29515  ftc1anclem3  29520  ftc1anclem8  29525  ftc2nc  29527  dvasin  29531  dvacos  29532  areacirclem2  29536  areacirc  29540  sdclem2  29689  cncfres  29715  pwssplit4  30492  pwfi2f1o  30501  hbtlem6  30535  itgpowd  30640  areaquad  30642  lhe4.4ex1a  30653  cncfmptss  30956  dvcosre  31058  dvmptresicc  31068  itgsinexplem1  31090  iblsplit  31103  itgcoscmulx  31106  itgiccshift  31117  itgperiod  31118  itgsbtaddcnst  31119  dirkeritg  31221  dirkercncflem2  31223  dirkercncflem4  31225  fourierdlem16  31242  fourierdlem21  31247  fourierdlem22  31248  fourierdlem28  31254  fourierdlem57  31283  fourierdlem58  31284  fourierdlem62  31288  fourierdlem74  31300  fourierdlem75  31301  fourierdlem78  31304  fourierdlem81  31307  fourierdlem83  31309  fourierdlem85  31311  fourierdlem90  31316  fourierdlem93  31319  fourierdlem101  31327  fourierdlem111  31337  fouriersw  31351  fdmdifeqresdif  31870  gsumpr  31889  gsumsplit2f  31894