Theorem resmpt 5144

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

Syntax hints:   -> wi 4   /\ wa 369   = wceq 1362   e. wcel 1755   C_ wss 3316   {copab 4337   e. cmpt 4338   |` cres 4829

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1594  ax-4 1605  ax-5 1669  ax-6 1707  ax-7 1727  ax-9 1759  ax-10 1774  ax-11 1779  ax-12 1791  ax-13 1942  ax-ext 2414  ax-sep 4401  ax-nul 4409  ax-pr 4519

This theorem depends on definitions:  df-bi 185  df-or 370  df-an 371  df-3an 960  df-tru 1365  df-ex 1590  df-nf 1593  df-sb 1700  df-clab 2420  df-cleq 2426  df-clel 2429  df-nfc 2558  df-ne 2598  df-ral 2710  df-rex 2711  df-rab 2714  df-v 2964  df-dif 3319  df-un 3321  df-in 3323  df-ss 3330  df-nul 3626  df-if 3780  df-sn 3866  df-pr 3868  df-op 3872  df-opab 4339  df-mpt 4340  df-xp 4833  df-rel 4834  df-res 4839

This theorem is referenced by:  resmpt3  5145  fvresex  6539  f1stres  6587  f2ndres  6588  tposss  6735  dftpos2  6751  dftpos4  6753  oacomf1olem  6991  resixpfo  7289  cantnfres  7873  rlimres2  13022  lo1res2  13023  o1res2  13024  rlimresb  13026  lo1eq  13029  rlimeq  13030  fsumss  13185  isumclim3  13209  bitsf1ocnv  13622  conjsubg  15757  conjsubgen  15758  psgnunilem5  15979  odf1o2  16051  sylow1lem2  16077  sylow2blem1  16098  gsumzres  16367  gsumzresOLD  16371  gsumzsplit  16397  gsumzsplitOLD  16398  gsumsplit2  16401  gsumsplit2OLD  16402  gsum2dlem2  16435  gsum2d  16436  gsum2dOLD  16437  dmdprdsplitlem  16507  dmdprdsplitlemOLD  16508  dprd2dlem1  16513  dprd2da  16514  dpjidcl  16530  dpjidclOLD  16537  ablfac1b  16544  psrass1lem  17380  psrlidm  17407  psrlidmOLD  17408  psrridm  17409  psrridmOLD  17410  mplmonmul  17476  mplcoe1  17477  mplcoe2  17480  mplcoe2OLD  17481  coe1mul2lem2  17619  frlmsplit2  18038  ofco2  18173  mdetralt  18255  mdetunilem9  18267  tgrest  18604  cmpfi  18852  ptpjopn  19026  xkoptsub  19068  xkopjcn  19070  cnmptid  19075  cnmpt1res  19090  fmss  19360  txflf  19420  tmdgsum  19507  subgntr  19518  opnsubg  19519  clsnsg  19521  tgpconcomp  19524  snclseqg  19527  tsmssplit  19567  tsmsxplem1  19568  imasdsf1olem  19789  subgnm  20060  iscmet3lem3  20642  mbfss  20965  mbfadd  20980  mbfsub  20981  mbflimsup  20985  mbfmullem2  21043  mbfmul  21045  itg2cnlem1  21080  iblss  21123  ellimc2  21193  limcres  21202  dvreslem  21225  dvres2lem  21226  dvidlem  21231  dvcnp2  21235  dvaddbr  21253  dvmulbr  21254  dvcmulf  21260  dvcobr  21261  dvrec  21270  dvmptres3  21271  dvmptres2  21277  dvmptntr  21286  dvcnvlem  21289  lhop1lem  21326  lhop2  21328  lhop  21329  dvfsumle  21334  dvfsumabs  21336  dvfsumlem2  21340  ftc2ditglem  21358  itgparts  21360  itgsubstlem  21361  evlsval2  21371  tdeglem4  21413  mdegfval  21415  plypf1  21564  taylthlem2  21723  psercn2  21772  psercn  21775  pserdvlem2  21777  abelth  21790  abelth2  21791  pige3  21863  efifo  21887  eff1olem  21888  dvlog2  21982  resqrcn  22071  sqrcn  22072  dvatan  22214  rlimcnp2  22244  xrlimcnp  22246  efrlim  22247  cxp2lim  22254  jensenlem2  22265  chpo1ub  22613  dchrisum0lem2a  22650  pntrsumo1  22698  pnt2  22746  pnt  22747  efghgrp  23682  resmptf  25797  ressnm  25934  gsummptun  26099  rmulccn  26211  xrge0mulc1cn  26224  gsumesum  26363  esumsn  26368  esumcvg  26388  eulerpartlem1  26597  eulerpartgbij  26602  gsumnunsn  26784  lgamcvg2  26888  divcnvshft  27244  divcnvlin  27245  fprodss  27307  fprodefsum  27331  iprodclim3  27346  mbfposadd  28280  itggt0cn  28305  ftc1anclem3  28310  ftc1anclem8  28315  ftc2nc  28317  dvasin  28321  dvacos  28322  areacirclem2  28326  areacirc  28330  sdclem2  28479  cncfres  28505  pwssplit4  29284  pwfi2f1o  29293  hbtlem6  29327  itgpowd  29432  areaquad  29434  lhe4.4ex1a  29445  cncfmptss  29610  dvcosre  29631  itgsinexplem1  29637  fdmdifeqresdif  30573  gsumpr  30589