Theorem resmpt 5176

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 5175	. 2 |- ( B C_ A -> ( { <. x , y >. | ( x e. A /\ y = C ) } |` B ) = { <. x , y >. | ( x e. B /\ y = C ) } )
2		df-mpt 4479	. . 3 |- ( x e. A |-> C ) = { <. x , y >. | ( x e. A /\ y = C ) }
3	2	reseq1i 5123	. 2 |- ( ( x e. A |-> C ) |` B ) = ( { <. x , y >. | ( x e. A /\ y = C ) } |` B )
4		df-mpt 4479	. 2 |- ( x e. B |-> C ) = { <. x , y >. | ( x e. B /\ y = C ) }
5	1, 3, 4	3eqtr4g 2521	1 |- ( B C_ A -> ( ( x e. A |-> C ) |` B ) = ( x e. B |-> C ) )

Syntax hints:   -> wi 4   /\ wa 375   = wceq 1455   e. wcel 1898   C_ wss 3416   {copab 4476   |-> cmpt 4477   |` cres 4858

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1680  ax-4 1693  ax-5 1769  ax-6 1816  ax-7 1862  ax-9 1907  ax-10 1926  ax-11 1931  ax-12 1944  ax-13 2102  ax-ext 2442  ax-sep 4541  ax-nul 4550  ax-pr 4656

This theorem depends on definitions:  df-bi 190  df-or 376  df-an 377  df-3an 993  df-tru 1458  df-ex 1675  df-nf 1679  df-sb 1809  df-clab 2449  df-cleq 2455  df-clel 2458  df-nfc 2592  df-ne 2635  df-ral 2754  df-rex 2755  df-rab 2758  df-v 3059  df-dif 3419  df-un 3421  df-in 3423  df-ss 3430  df-nul 3744  df-if 3894  df-sn 3981  df-pr 3983  df-op 3987  df-opab 4478  df-mpt 4479  df-xp 4862  df-rel 4863  df-res 4868

This theorem is referenced by:  resmpt3  5177  resmptd  5178  fvresex  6798  f1stres  6847  f2ndres  6848  tposss  7005  dftpos2  7021  dftpos4  7023  resixpfo  7591  rlimresb  13684  lo1eq  13687  rlimeq  13688  fsumss  13846  isumclim3  13875  divcnvshft  13968  fprodss  14057  iprodclim3  14108  fprodefsum  14204  bitsf1ocnv  14473  conjsubg  16969  psgnunilem5  17190  odf1o2  17277  sylow1lem2  17306  sylow2blem1  17327  gsumzres  17598  gsumzsplit  17615  gsumzunsnd  17643  gsum2dlem2  17658  gsummptnn0fz  17670  dprd2da  17730  dpjidcl  17746  ablfac1b  17758  psrass1lem  18656  coe1mul2lem2  18916  frlmsplit2  19386  ofco2  19531  mdetralt  19688  mdetunilem9  19700  tgrest  20230  cmpfi  20478  cnmptid  20731  fmss  21016  txflf  21076  tmdgsum  21165  tgpconcomp  21182  tsmssplit  21221  iscmet3lem3  22315  mbfss  22658  mbfadd  22673  mbfsub  22674  mbflimsup  22679  mbflimsupOLD  22680  mbfmul  22740  itg2cnlem1  22775  ellimc2  22888  dvreslem  22920  dvres2lem  22921  dvidlem  22926  dvcnp2  22930  dvmulbr  22949  dvcobr  22956  dvrec  22965  dvmptntr  22981  dvcnvlem  22984  lhop1lem  23021  lhop2  23023  itgparts  23055  itgsubstlem  23056  tdeglem4  23065  plypf1  23222  taylthlem2  23385  pserdvlem2  23439  abelth  23452  pige3  23528  efifo  23552  eff1olem  23553  dvlog2  23654  resqrtcn  23745  sqrtcn  23746  dvatan  23917  rlimcnp2  23948  xrlimcnp  23950  efrlim  23951  cxp2lim  23958  chpo1ub  24374  dchrisum0lem2a  24411  pnt2  24507  pnt  24508  resmptf  28310  ressnm  28464  gsummpt2d  28595  rmulccn  28785  xrge0mulc1cn  28798  gsumesum  28931  esumsnf  28936  esumcvg  28958  omsmon  29176  omsmonOLD  29180  carsggect  29200  eulerpartlem1  29250  eulerpartgbij  29255  gsumnunsn  29475  elmsubrn  30216  divcnvlin  30417  mptsnunlem  31786  dissneqlem  31788  broucube  32020  mbfposadd  32034  itggt0cn  32060  ftc1anclem3  32065  ftc1anclem8  32070  dvasin  32074  dvacos  32075  areacirc  32083  sdclem2  32117  cncfres  32143  pwssplit4  35993  pwfi2f1o  36000  hbtlem6  36034  itgpowd  36145  areaquad  36147  hashnzfzclim  36716  lhe4.4ex1a  36723  resmpti  37499  mptss  37509  dvcosre  37867  dvmptresicc  37877  itgsinexplem1  37916  itgcoscmulx  37932  dirkeritg  38065  dirkercncflem2  38067  fourierdlem16  38086  fourierdlem21  38091  fourierdlem22  38092  fourierdlem57  38128  fourierdlem58  38129  fourierdlem62  38133  fourierdlem83  38154  fourierdlem111  38182  fouriersw  38196  0ome  38458  gsumpr  40511