Theorem resmpt 5173

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

Syntax hints:   -> wi 4   /\ wa 370   = wceq 1437   e. wcel 1872   C_ wss 3436   {copab 4481   |-> cmpt 4482   |` cres 4855

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1663  ax-4 1676  ax-5 1752  ax-6 1798  ax-7 1843  ax-9 1876  ax-10 1891  ax-11 1896  ax-12 1909  ax-13 2057  ax-ext 2401  ax-sep 4546  ax-nul 4555  ax-pr 4660

This theorem depends on definitions:  df-bi 188  df-or 371  df-an 372  df-3an 984  df-tru 1440  df-ex 1658  df-nf 1662  df-sb 1791  df-clab 2408  df-cleq 2414  df-clel 2417  df-nfc 2568  df-ne 2616  df-ral 2776  df-rex 2777  df-rab 2780  df-v 3082  df-dif 3439  df-un 3441  df-in 3443  df-ss 3450  df-nul 3762  df-if 3912  df-sn 3999  df-pr 4001  df-op 4005  df-opab 4483  df-mpt 4484  df-xp 4859  df-rel 4860  df-res 4865

This theorem is referenced by:  resmpt3  5174  resmptd  5175  fvresex  6780  f1stres  6829  f2ndres  6830  tposss  6985  dftpos2  7001  dftpos4  7003  resixpfo  7571  rlimresb  13628  lo1eq  13631  rlimeq  13632  fsumss  13790  isumclim3  13819  divcnvshft  13912  fprodss  14001  iprodclim3  14052  fprodefsum  14148  bitsf1ocnv  14417  conjsubg  16913  psgnunilem5  17134  odf1o2  17221  sylow1lem2  17250  sylow2blem1  17271  gsumzres  17542  gsumzsplit  17559  gsumzunsnd  17587  gsum2dlem2  17602  gsummptnn0fz  17614  dprd2da  17674  dpjidcl  17690  ablfac1b  17702  psrass1lem  18600  coe1mul2lem2  18860  frlmsplit2  19329  ofco2  19474  mdetralt  19631  mdetunilem9  19643  tgrest  20173  cmpfi  20421  cnmptid  20674  fmss  20959  txflf  21019  tmdgsum  21108  tgpconcomp  21125  tsmssplit  21164  iscmet3lem3  22258  mbfss  22600  mbfadd  22615  mbfsub  22616  mbflimsup  22621  mbflimsupOLD  22622  mbfmul  22682  itg2cnlem1  22717  ellimc2  22830  dvreslem  22862  dvres2lem  22863  dvidlem  22868  dvcnp2  22872  dvmulbr  22891  dvcobr  22898  dvrec  22907  dvmptntr  22923  dvcnvlem  22926  lhop1lem  22963  lhop2  22965  itgparts  22997  itgsubstlem  22998  tdeglem4  23007  plypf1  23164  taylthlem2  23327  pserdvlem2  23381  abelth  23394  pige3  23470  efifo  23494  eff1olem  23495  dvlog2  23596  resqrtcn  23687  sqrtcn  23688  dvatan  23859  rlimcnp2  23890  xrlimcnp  23892  efrlim  23893  cxp2lim  23900  chpo1ub  24316  dchrisum0lem2a  24353  pnt2  24449  pnt  24450  resmptf  28259  ressnm  28419  gsummpt2d  28551  rmulccn  28742  xrge0mulc1cn  28755  gsumesum  28888  esumsnf  28893  esumcvg  28915  omsmon  29134  omsmonOLD  29138  carsggect  29158  eulerpartlem1  29208  eulerpartgbij  29213  gsumnunsn  29433  elmsubrn  30174  divcnvlin  30374  mptsnunlem  31704  dissneqlem  31706  broucube  31938  mbfposadd  31952  itggt0cn  31978  ftc1anclem3  31983  ftc1anclem8  31988  dvasin  31992  dvacos  31993  areacirc  32001  sdclem2  32035  cncfres  32061  pwssplit4  35917  pwfi2f1o  35924  hbtlem6  35958  itgpowd  36069  areaquad  36071  hashnzfzclim  36641  lhe4.4ex1a  36648  resmpti  37406  mptss  37416  dvcosre  37721  dvmptresicc  37731  itgsinexplem1  37770  itgcoscmulx  37786  dirkeritg  37904  dirkercncflem2  37906  fourierdlem16  37925  fourierdlem21  37930  fourierdlem22  37931  fourierdlem57  37967  fourierdlem58  37968  fourierdlem62  37972  fourierdlem83  37993  fourierdlem111  38021  fouriersw  38035  0ome  38258  gsumpr  39763