Theorem resmpt 5333

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

Syntax hints:   -> wi 4   /\ wa 369   = wceq 1395   e. wcel 1819   C_ wss 3471   {copab 4514   |-> cmpt 4515   |` cres 5010

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1619  ax-4 1632  ax-5 1705  ax-6 1748  ax-7 1791  ax-9 1823  ax-10 1838  ax-11 1843  ax-12 1855  ax-13 2000  ax-ext 2435  ax-sep 4578  ax-nul 4586  ax-pr 4695

This theorem depends on definitions:  df-bi 185  df-or 370  df-an 371  df-3an 975  df-tru 1398  df-ex 1614  df-nf 1618  df-sb 1741  df-clab 2443  df-cleq 2449  df-clel 2452  df-nfc 2607  df-ne 2654  df-ral 2812  df-rex 2813  df-rab 2816  df-v 3111  df-dif 3474  df-un 3476  df-in 3478  df-ss 3485  df-nul 3794  df-if 3945  df-sn 4033  df-pr 4035  df-op 4039  df-opab 4516  df-mpt 4517  df-xp 5014  df-rel 5015  df-res 5020

This theorem is referenced by:  resmpt3  5334  resmptd  5335  fvresex  6772  f1stres  6821  f2ndres  6822  tposss  6974  dftpos2  6990  dftpos4  6992  resixpfo  7526  rlimresb  13400  lo1eq  13403  rlimeq  13404  fsumss  13559  isumclim3  13586  fprodss  13767  iprodclim3  13805  fprodefsum  13842  bitsf1ocnv  14106  conjsubg  16425  psgnunilem5  16646  odf1o2  16720  sylow1lem2  16746  sylow2blem1  16767  gsumzres  17041  gsumzresOLD  17045  gsumzsplit  17071  gsumzsplitOLD  17072  gsumsplit2OLD  17076  gsumzunsnd  17109  gsum2dlem2  17125  gsum2dOLD  17127  gsummptnn0fz  17141  dmdprdsplitlemOLD  17212  dprd2da  17218  dpjidcl  17234  dpjidclOLD  17241  ablfac1b  17248  psrass1lem  18156  psrlidmOLD  18184  psrridmOLD  18186  mplcoe2OLD  18260  coe1mul2lem2  18436  frlmsplit2  18930  ofco2  19080  mdetralt  19237  mdetunilem9  19249  tgrest  19787  cmpfi  20035  cnmptid  20288  fmss  20573  txflf  20633  tmdgsum  20720  tgpconcomp  20737  tsmssplit  20780  iscmet3lem3  21855  mbfss  22179  mbfadd  22194  mbfsub  22195  mbflimsup  22199  mbfmul  22259  itg2cnlem1  22294  ellimc2  22407  dvreslem  22439  dvres2lem  22440  dvidlem  22445  dvcnp2  22449  dvmulbr  22468  dvcobr  22475  dvrec  22484  dvmptntr  22500  dvcnvlem  22503  lhop1lem  22540  lhop2  22542  itgparts  22574  itgsubstlem  22575  tdeglem4  22584  plypf1  22735  taylthlem2  22895  pserdvlem2  22949  abelth  22962  pige3  23036  efifo  23060  eff1olem  23061  dvlog2  23160  resqrtcn  23249  sqrtcn  23250  dvatan  23392  rlimcnp2  23422  xrlimcnp  23424  efrlim  23425  cxp2lim  23432  chpo1ub  23791  dchrisum0lem2a  23828  pnt2  23924  pnt  23925  resmptf  27646  ressnm  27799  gsummpt2d  27932  rmulccn  28071  xrge0mulc1cn  28084  gsumesum  28231  esumsnf  28236  esumcvg  28258  omsmon  28442  eulerpartlem1  28503  eulerpartgbij  28508  gsumnunsn  28690  elmsubrn  29085  divcnvshft  29335  divcnvlin  29336  mbfposadd  30267  itggt0cn  30292  ftc1anclem3  30297  ftc1anclem8  30302  dvasin  30308  dvacos  30309  areacirc  30317  sdclem2  30440  cncfres  30466  pwssplit4  31239  pwfi2f1o  31248  hbtlem6  31282  itgpowd  31386  areaquad  31388  hashnzfzclim  31431  lhe4.4ex1a  31438  dvcosre  31909  dvmptresicc  31919  itgsinexplem1  31955  itgcoscmulx  31971  dirkeritg  32087  dirkercncflem2  32089  fourierdlem16  32108  fourierdlem21  32113  fourierdlem22  32114  fourierdlem57  32149  fourierdlem58  32150  fourierdlem62  32154  fourierdlem83  32175  fourierdlem111  32203  fouriersw  32217  gsumpr  33094