Theorem resmpt 5151

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

Syntax hints:   -> wi 4   /\ wa 369   = wceq 1369   e. wcel 1756   C_ wss 3323   {copab 4344   e. cmpt 4345   |` cres 4837

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1591  ax-4 1602  ax-5 1670  ax-6 1708  ax-7 1728  ax-9 1760  ax-10 1775  ax-11 1780  ax-12 1792  ax-13 1943  ax-ext 2419  ax-sep 4408  ax-nul 4416  ax-pr 4526

This theorem depends on definitions:  df-bi 185  df-or 370  df-an 371  df-3an 967  df-tru 1372  df-ex 1587  df-nf 1590  df-sb 1701  df-clab 2425  df-cleq 2431  df-clel 2434  df-nfc 2563  df-ne 2603  df-ral 2715  df-rex 2716  df-rab 2719  df-v 2969  df-dif 3326  df-un 3328  df-in 3330  df-ss 3337  df-nul 3633  df-if 3787  df-sn 3873  df-pr 3875  df-op 3879  df-opab 4346  df-mpt 4347  df-xp 4841  df-rel 4842  df-res 4847

This theorem is referenced by:  resmpt3  5152  fvresex  6545  f1stres  6593  f2ndres  6594  tposss  6741  dftpos2  6757  dftpos4  6759  oacomf1olem  6995  resixpfo  7293  cantnfres  7877  rlimres2  13031  lo1res2  13032  o1res2  13033  rlimresb  13035  lo1eq  13038  rlimeq  13039  fsumss  13194  isumclim3  13218  bitsf1ocnv  13632  conjsubg  15769  conjsubgen  15770  psgnunilem5  15991  odf1o2  16063  sylow1lem2  16089  sylow2blem1  16110  gsumzres  16379  gsumzresOLD  16383  gsumzsplit  16409  gsumzsplitOLD  16410  gsumsplit2  16413  gsumsplit2OLD  16414  gsumzunsnd  16441  gsum2dlem2  16452  gsum2d  16453  gsum2dOLD  16454  dmdprdsplitlem  16524  dmdprdsplitlemOLD  16525  dprd2dlem1  16530  dprd2da  16531  dpjidcl  16547  dpjidclOLD  16554  ablfac1b  16561  psrass1lem  17427  psrlidm  17454  psrlidmOLD  17455  psrridm  17456  psrridmOLD  17457  mplmonmul  17523  mplcoe1  17524  mplcoe5  17528  mplcoe2OLD  17530  evlsval2  17586  coe1mul2lem2  17702  frlmsplit2  18177  ofco2  18312  mdetralt  18394  mdetunilem9  18406  tgrest  18743  cmpfi  18991  ptpjopn  19165  xkoptsub  19207  xkopjcn  19209  cnmptid  19214  cnmpt1res  19229  fmss  19499  txflf  19559  tmdgsum  19646  subgntr  19657  opnsubg  19658  clsnsg  19660  tgpconcomp  19663  snclseqg  19666  tsmssplit  19706  tsmsxplem1  19707  imasdsf1olem  19928  subgnm  20199  iscmet3lem3  20781  mbfss  21104  mbfadd  21119  mbfsub  21120  mbflimsup  21124  mbfmullem2  21182  mbfmul  21184  itg2cnlem1  21219  iblss  21262  ellimc2  21332  limcres  21341  dvreslem  21364  dvres2lem  21365  dvidlem  21370  dvcnp2  21374  dvaddbr  21392  dvmulbr  21393  dvcmulf  21399  dvcobr  21400  dvrec  21409  dvmptres3  21410  dvmptres2  21416  dvmptntr  21425  dvcnvlem  21428  lhop1lem  21465  lhop2  21467  lhop  21468  dvfsumle  21473  dvfsumabs  21475  dvfsumlem2  21479  ftc2ditglem  21497  itgparts  21499  itgsubstlem  21500  tdeglem4  21509  mdegfval  21511  plypf1  21660  taylthlem2  21819  psercn2  21868  psercn  21871  pserdvlem2  21873  abelth  21886  abelth2  21887  pige3  21959  efifo  21983  eff1olem  21984  dvlog2  22078  resqrcn  22167  sqrcn  22168  dvatan  22310  rlimcnp2  22340  xrlimcnp  22342  efrlim  22343  cxp2lim  22350  jensenlem2  22361  chpo1ub  22709  dchrisum0lem2a  22746  pntrsumo1  22794  pnt2  22842  pnt  22843  efghgrp  23828  resmptf  25942  ressnm  26080  gsummptun  26216  rmulccn  26327  xrge0mulc1cn  26340  gsumesum  26479  esumsn  26484  esumcvg  26504  omsmon  26680  eulerpartlem1  26719  eulerpartgbij  26724  gsumnunsn  26906  lgamcvg2  27010  divcnvshft  27367  divcnvlin  27368  fprodss  27430  fprodefsum  27454  iprodclim3  27469  mbfposadd  28410  itggt0cn  28435  ftc1anclem3  28440  ftc1anclem8  28445  ftc2nc  28447  dvasin  28451  dvacos  28452  areacirclem2  28456  areacirc  28460  sdclem2  28609  cncfres  28635  pwssplit4  29413  pwfi2f1o  29422  hbtlem6  29456  itgpowd  29561  areaquad  29563  lhe4.4ex1a  29574  cncfmptss  29739  dvcosre  29759  itgsinexplem1  29765  fdmdifeqresdif  30702  gsumpr  30727  gsumsplit2f  30733  gsummptnn0fz  30775