Theorem resmpt 5143

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

Syntax hints:   -> wi 4   /\ wa 367   = wceq 1405   e. wcel 1842   C_ wss 3414   {copab 4452   |-> cmpt 4453   |` cres 4825

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1639  ax-4 1652  ax-5 1725  ax-6 1771  ax-7 1814  ax-9 1846  ax-10 1861  ax-11 1866  ax-12 1878  ax-13 2026  ax-ext 2380  ax-sep 4517  ax-nul 4525  ax-pr 4630

This theorem depends on definitions:  df-bi 185  df-or 368  df-an 369  df-3an 976  df-tru 1408  df-ex 1634  df-nf 1638  df-sb 1764  df-clab 2388  df-cleq 2394  df-clel 2397  df-nfc 2552  df-ne 2600  df-ral 2759  df-rex 2760  df-rab 2763  df-v 3061  df-dif 3417  df-un 3419  df-in 3421  df-ss 3428  df-nul 3739  df-if 3886  df-sn 3973  df-pr 3975  df-op 3979  df-opab 4454  df-mpt 4455  df-xp 4829  df-rel 4830  df-res 4835

This theorem is referenced by:  resmpt3  5144  resmptd  5145  fvresex  6757  f1stres  6806  f2ndres  6807  tposss  6959  dftpos2  6975  dftpos4  6977  resixpfo  7545  rlimresb  13537  lo1eq  13540  rlimeq  13541  fsumss  13696  isumclim3  13725  divcnvshft  13818  fprodss  13907  iprodclim3  13945  fprodefsum  14039  bitsf1ocnv  14303  conjsubg  16622  psgnunilem5  16843  odf1o2  16917  sylow1lem2  16943  sylow2blem1  16964  gsumzres  17238  gsumzresOLD  17242  gsumzsplit  17268  gsumzsplitOLD  17269  gsumzunsnd  17303  gsum2dlem2  17319  gsum2dOLD  17321  gsummptnn0fz  17334  dmdprdsplitlemOLD  17405  dprd2da  17411  dpjidcl  17427  dpjidclOLD  17434  ablfac1b  17441  psrass1lem  18349  psrlidmOLD  18377  psrridmOLD  18379  mplcoe2OLD  18453  coe1mul2lem2  18629  frlmsplit2  19099  ofco2  19245  mdetralt  19402  mdetunilem9  19414  tgrest  19953  cmpfi  20201  cnmptid  20454  fmss  20739  txflf  20799  tmdgsum  20886  tgpconcomp  20903  tsmssplit  20946  iscmet3lem3  22021  mbfss  22345  mbfadd  22360  mbfsub  22361  mbflimsup  22365  mbfmul  22425  itg2cnlem1  22460  ellimc2  22573  dvreslem  22605  dvres2lem  22606  dvidlem  22611  dvcnp2  22615  dvmulbr  22634  dvcobr  22641  dvrec  22650  dvmptntr  22666  dvcnvlem  22669  lhop1lem  22706  lhop2  22708  itgparts  22740  itgsubstlem  22741  tdeglem4  22750  plypf1  22901  taylthlem2  23061  pserdvlem2  23115  abelth  23128  pige3  23202  efifo  23226  eff1olem  23227  dvlog2  23328  resqrtcn  23419  sqrtcn  23420  dvatan  23591  rlimcnp2  23622  xrlimcnp  23624  efrlim  23625  cxp2lim  23632  chpo1ub  24046  dchrisum0lem2a  24083  pnt2  24179  pnt  24180  resmptf  27939  ressnm  28091  gsummpt2d  28223  rmulccn  28363  xrge0mulc1cn  28376  gsumesum  28506  esumsnf  28511  esumcvg  28533  omsmon  28746  carsggect  28766  eulerpartlem1  28812  eulerpartgbij  28817  gsumnunsn  28999  elmsubrn  29740  divcnvlin  29940  mptsnunlem  31254  dissneqlem  31256  mbfposadd  31434  itggt0cn  31460  ftc1anclem3  31465  ftc1anclem8  31470  dvasin  31474  dvacos  31475  areacirc  31483  sdclem2  31517  cncfres  31543  pwssplit4  35397  pwfi2f1o  35406  pwfi2f1oOLD  35407  hbtlem6  35442  itgpowd  35546  areaquad  35548  hashnzfzclim  36075  lhe4.4ex1a  36082  dvcosre  37074  dvmptresicc  37084  itgsinexplem1  37120  itgcoscmulx  37136  dirkeritg  37252  dirkercncflem2  37254  fourierdlem16  37273  fourierdlem21  37278  fourierdlem22  37279  fourierdlem57  37314  fourierdlem58  37315  fourierdlem62  37319  fourierdlem83  37340  fourierdlem111  37368  fouriersw  37382  gsumpr  38461