Theorem resmpt 5254

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

Syntax hints:   -> wi 4   /\ wa 369   = wceq 1370   e. wcel 1758   C_ wss 3426   {copab 4447   |-> cmpt 4448   |` cres 4940

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1592  ax-4 1603  ax-5 1671  ax-6 1710  ax-7 1730  ax-9 1762  ax-10 1777  ax-11 1782  ax-12 1794  ax-13 1952  ax-ext 2430  ax-sep 4511  ax-nul 4519  ax-pr 4629

This theorem depends on definitions:  df-bi 185  df-or 370  df-an 371  df-3an 967  df-tru 1373  df-ex 1588  df-nf 1591  df-sb 1703  df-clab 2437  df-cleq 2443  df-clel 2446  df-nfc 2601  df-ne 2646  df-ral 2800  df-rex 2801  df-rab 2804  df-v 3070  df-dif 3429  df-un 3431  df-in 3433  df-ss 3440  df-nul 3736  df-if 3890  df-sn 3976  df-pr 3978  df-op 3982  df-opab 4449  df-mpt 4450  df-xp 4944  df-rel 4945  df-res 4950

This theorem is referenced by:  resmpt3  5255  fvresex  6650  f1stres  6698  f2ndres  6699  tposss  6846  dftpos2  6862  dftpos4  6864  oacomf1olem  7103  resixpfo  7401  cantnfres  7986  rlimres2  13141  lo1res2  13142  o1res2  13143  rlimresb  13145  lo1eq  13148  rlimeq  13149  fsumss  13304  isumclim3  13328  bitsf1ocnv  13742  conjsubg  15880  conjsubgen  15881  psgnunilem5  16102  odf1o2  16176  sylow1lem2  16202  sylow2blem1  16223  gsumzres  16492  gsumzresOLD  16496  gsumzsplit  16522  gsumzsplitOLD  16523  gsumsplit2  16526  gsumsplit2OLD  16527  gsumzunsnd  16556  gsum2dlem2  16567  gsum2d  16568  gsum2dOLD  16569  dmdprdsplitlem  16639  dmdprdsplitlemOLD  16640  dprd2dlem1  16645  dprd2da  16646  dpjidcl  16662  dpjidclOLD  16669  ablfac1b  16676  psrass1lem  17553  psrlidm  17580  psrlidmOLD  17581  psrridm  17582  psrridmOLD  17583  mplmonmul  17650  mplcoe1  17651  mplcoe5  17655  mplcoe2OLD  17657  evlsval2  17713  coe1mul2lem2  17829  frlmsplit2  18306  ofco2  18443  mdetralt  18530  mdetunilem9  18542  tgrest  18879  cmpfi  19127  ptpjopn  19301  xkoptsub  19343  xkopjcn  19345  cnmptid  19350  cnmpt1res  19365  fmss  19635  txflf  19695  tmdgsum  19782  subgntr  19793  opnsubg  19794  clsnsg  19796  tgpconcomp  19799  snclseqg  19802  tsmssplit  19842  tsmsxplem1  19843  imasdsf1olem  20064  subgnm  20335  iscmet3lem3  20917  mbfss  21240  mbfadd  21255  mbfsub  21256  mbflimsup  21260  mbfmullem2  21318  mbfmul  21320  itg2cnlem1  21355  iblss  21398  ellimc2  21468  limcres  21477  dvreslem  21500  dvres2lem  21501  dvidlem  21506  dvcnp2  21510  dvaddbr  21528  dvmulbr  21529  dvcmulf  21535  dvcobr  21536  dvrec  21545  dvmptres3  21546  dvmptres2  21552  dvmptntr  21561  dvcnvlem  21564  lhop1lem  21601  lhop2  21603  lhop  21604  dvfsumle  21609  dvfsumabs  21611  dvfsumlem2  21615  ftc2ditglem  21633  itgparts  21635  itgsubstlem  21636  tdeglem4  21645  mdegfval  21647  plypf1  21796  taylthlem2  21955  psercn2  22004  psercn  22007  pserdvlem2  22009  abelth  22022  abelth2  22023  pige3  22095  efifo  22119  eff1olem  22120  dvlog2  22214  resqrcn  22303  sqrcn  22304  dvatan  22446  rlimcnp2  22476  xrlimcnp  22478  efrlim  22479  cxp2lim  22486  jensenlem2  22497  chpo1ub  22845  dchrisum0lem2a  22882  pntrsumo1  22930  pnt2  22978  pnt  22979  efghgrp  23995  resmptf  26108  ressnm  26246  gsummptun  26382  rmulccn  26492  xrge0mulc1cn  26505  gsumesum  26644  esumsn  26649  esumcvg  26669  omsmon  26845  eulerpartlem1  26884  eulerpartgbij  26889  gsumnunsn  27071  lgamcvg2  27175  divcnvshft  27532  divcnvlin  27533  fprodss  27595  fprodefsum  27619  iprodclim3  27634  mbfposadd  28577  itggt0cn  28602  ftc1anclem3  28607  ftc1anclem8  28612  ftc2nc  28614  dvasin  28618  dvacos  28619  areacirclem2  28623  areacirc  28627  sdclem2  28776  cncfres  28802  pwssplit4  29580  pwfi2f1o  29589  hbtlem6  29623  itgpowd  29728  areaquad  29730  lhe4.4ex1a  29741  cncfmptss  29906  dvcosre  29926  itgsinexplem1  29932  fdmdifeqresdif  30870  gsumpr  30896  gsumsplit2f  30902  gsummptnn0fz  30947