Theorem resmpt 5309

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

Syntax hints:   -> wi 4   /\ wa 369   = wceq 1381   e. wcel 1802   C_ wss 3458   {copab 4490   |-> cmpt 4491   |` cres 4987

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1603  ax-4 1616  ax-5 1689  ax-6 1732  ax-7 1774  ax-9 1806  ax-10 1821  ax-11 1826  ax-12 1838  ax-13 1983  ax-ext 2419  ax-sep 4554  ax-nul 4562  ax-pr 4672

This theorem depends on definitions:  df-bi 185  df-or 370  df-an 371  df-3an 974  df-tru 1384  df-ex 1598  df-nf 1602  df-sb 1725  df-clab 2427  df-cleq 2433  df-clel 2436  df-nfc 2591  df-ne 2638  df-ral 2796  df-rex 2797  df-rab 2800  df-v 3095  df-dif 3461  df-un 3463  df-in 3465  df-ss 3472  df-nul 3768  df-if 3923  df-sn 4011  df-pr 4013  df-op 4017  df-opab 4492  df-mpt 4493  df-xp 4991  df-rel 4992  df-res 4997

This theorem is referenced by:  resmpt3  5310  resmptd  5311  fvresex  6754  f1stres  6803  f2ndres  6804  tposss  6954  dftpos2  6970  dftpos4  6972  resixpfo  7505  rlimresb  13362  lo1eq  13365  rlimeq  13366  fsumss  13521  isumclim3  13548  bitsf1ocnv  13966  conjsubg  16167  psgnunilem5  16388  odf1o2  16462  sylow1lem2  16488  sylow2blem1  16509  gsumzres  16783  gsumzresOLD  16787  gsumzsplit  16813  gsumzsplitOLD  16814  gsumsplit2OLD  16818  gsumzunsnd  16851  gsum2dlem2  16867  gsum2dOLD  16869  gsummptnn0fz  16883  dmdprdsplitlemOLD  16953  dprd2da  16959  dpjidcl  16975  dpjidclOLD  16982  ablfac1b  16989  psrass1lem  17897  psrlidmOLD  17925  psrridmOLD  17927  mplcoe2OLD  18001  coe1mul2lem2  18177  frlmsplit2  18670  ofco2  18820  mdetralt  18977  mdetunilem9  18989  tgrest  19526  cmpfi  19774  cnmptid  20028  fmss  20313  txflf  20373  tmdgsum  20460  tgpconcomp  20477  tsmssplit  20520  iscmet3lem3  21595  mbfss  21919  mbfadd  21934  mbfsub  21935  mbflimsup  21939  mbfmul  21999  itg2cnlem1  22034  ellimc2  22147  dvreslem  22179  dvres2lem  22180  dvidlem  22185  dvcnp2  22189  dvmulbr  22208  dvcobr  22215  dvrec  22224  dvmptntr  22240  dvcnvlem  22243  lhop1lem  22280  lhop2  22282  itgparts  22314  itgsubstlem  22315  tdeglem4  22324  plypf1  22475  taylthlem2  22634  pserdvlem2  22688  abelth  22701  pige3  22775  efifo  22799  eff1olem  22800  dvlog2  22899  resqrtcn  22988  sqrtcn  22989  dvatan  23131  rlimcnp2  23161  xrlimcnp  23163  efrlim  23164  cxp2lim  23171  chpo1ub  23530  dchrisum0lem2a  23567  pnt2  23663  pnt  23664  resmptf  27362  ressnm  27505  rmulccn  27776  xrge0mulc1cn  27789  gsumesum  27933  esumsn  27938  esumcvg  27958  eulerpartlem1  28172  eulerpartgbij  28177  gsumnunsn  28359  elmsubrn  28754  divcnvshft  28985  divcnvlin  28986  fprodss  29048  fprodefsum  29072  iprodclim3  29087  mbfposadd  30030  itggt0cn  30055  ftc1anclem3  30060  ftc1anclem8  30065  dvasin  30071  dvacos  30072  areacirc  30080  sdclem2  30203  cncfres  30229  pwssplit4  31003  pwfi2f1o  31012  hbtlem6  31046  itgpowd  31151  areaquad  31153  hashnzfzclim  31196  lhe4.4ex1a  31203  dvcosre  31606  dvmptresicc  31616  itgsinexplem1  31638  itgcoscmulx  31654  dirkeritg  31769  dirkercncflem2  31771  fourierdlem16  31790  fourierdlem21  31795  fourierdlem22  31796  fourierdlem57  31831  fourierdlem58  31832  fourierdlem62  31836  fourierdlem83  31857  fourierdlem111  31885  fouriersw  31899  gsumpr  32658