MPE Home Metamath Proof Explorer < Previous   Next >
Nearby theorems
Mirrors  >  Home  >  MPE Home  >  Th. List  >  resmpt Unicode version

Theorem resmpt 5158
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.
StepHypRef Expression
1 resopab2 5157 . 2  |-  ( B 
C_  A  ->  ( { <. x ,  y
>.  |  ( x  e.  A  /\  y  =  C ) }  |`  B )  =  { <. x ,  y >.  |  ( x  e.  B  /\  y  =  C ) } )
2 df-mpt 4236 . . 3  |-  ( x  e.  A  |->  C )  =  { <. x ,  y >.  |  ( x  e.  A  /\  y  =  C ) }
32reseq1i 5109 . 2  |-  ( ( x  e.  A  |->  C )  |`  B )  =  ( { <. x ,  y >.  |  ( x  e.  A  /\  y  =  C ) }  |`  B )
4 df-mpt 4236 . 2  |-  ( x  e.  B  |->  C )  =  { <. x ,  y >.  |  ( x  e.  B  /\  y  =  C ) }
51, 3, 43eqtr4g 2469 1  |-  ( B 
C_  A  ->  (
( x  e.  A  |->  C )  |`  B )  =  ( x  e.  B  |->  C ) )
Colors of variables: wff set class
Syntax hints:    -> wi 4    /\ wa 359    = wceq 1649    e. wcel 1721    C_ wss 3288   {copab 4233    e. cmpt 4234    |` cres 4847
This theorem is referenced by:  resmpt3  5159  fvresex  5949  f1stres  6335  f2ndres  6336  tposss  6447  dftpos2  6463  dftpos4  6465  oacomf1olem  6774  resixpfo  7067  cantnfres  7597  rlimres2  12318  lo1res2  12319  o1res2  12320  rlimresb  12322  lo1eq  12325  rlimeq  12326  fsumss  12482  isumclim3  12506  bitsf1ocnv  12919  conjsubg  15000  conjsubgen  15001  odf1o2  15170  sylow1lem2  15196  sylow2blem1  15217  gsumzres  15480  gsumzsplit  15492  gsumsplit2  15494  gsum2d  15509  dmdprdsplitlem  15558  dprd2dlem1  15562  dprd2da  15563  dpjidcl  15579  ablfac1b  15591  psrass1lem  16405  psrlidm  16430  psrridm  16431  mplmonmul  16490  mplcoe1  16491  mplcoe2  16493  coe1mul2lem2  16624  tgrest  17185  cmpfi  17433  ptpjopn  17605  xkoptsub  17647  xkopjcn  17649  cnmptid  17654  cnmpt1res  17669  fmss  17939  txflf  17999  tmdgsum  18086  subgntr  18097  opnsubg  18098  clsnsg  18100  tgpconcomp  18103  snclseqg  18106  tsmssplit  18142  tsmsxplem1  18143  imasdsf1olem  18364  subgnm  18635  iscmet3lem3  19204  mbfss  19499  mbfadd  19514  mbfsub  19515  mbflimsup  19519  mbfmullem2  19577  mbfmul  19579  itg2cnlem1  19614  iblss  19657  ellimc2  19725  limcres  19734  dvreslem  19757  dvres2lem  19758  dvidlem  19763  dvcnp2  19767  dvaddbr  19785  dvmulbr  19786  dvcmulf  19792  dvcobr  19793  dvrec  19802  dvmptres3  19803  dvmptres2  19809  dvmptntr  19818  dvcnvlem  19821  lhop1lem  19858  lhop2  19860  lhop  19861  dvfsumle  19866  dvfsumabs  19868  dvfsumlem2  19872  ftc2ditglem  19890  itgparts  19892  itgsubstlem  19893  evlsval2  19902  tdeglem4  19944  mdegfval  19946  plypf1  20092  taylthlem2  20251  psercn2  20300  psercn  20303  pserdvlem2  20305  abelth  20318  abelth2  20319  pige3  20386  efifo  20410  eff1olem  20411  dvlog2  20505  resqrcn  20594  sqrcn  20595  dvatan  20736  rlimcnp2  20766  xrlimcnp  20768  efrlim  20769  cxp2lim  20776  jensenlem2  20787  chpo1ub  21135  dchrisum0lem2a  21172  pntrsumo1  21220  pnt2  21268  pnt  21269  efghgrp  21922  resmptf  24032  ressnm  24145  rmulccn  24275  xrge0mulc1cn  24288  gsumesum  24412  esumsn  24417  esumcvg  24437  lgamcvg2  24800  divcnvshft  25172  divcnvlin  25173  fprodss  25235  fprodefsum  25259  iprodclim3  25274  itggt0cn  26184  areacirclem4  26191  sdclem2  26344  cncfres  26372  pwssplit4  27067  frlmsplit2  27119  pwfi2f1o  27136  hbtlem6  27209  psgnunilem5  27293  lhe4.4ex1a  27422  cncfmptss  27592  dvcosre  27616  itgsinexplem1  27623
This theorem was proved from axioms:  ax-1 5  ax-2 6  ax-3 7  ax-mp 8  ax-gen 1552  ax-5 1563  ax-17 1623  ax-9 1662  ax-8 1683  ax-14 1725  ax-6 1740  ax-7 1745  ax-11 1757  ax-12 1946  ax-ext 2393  ax-sep 4298  ax-nul 4306  ax-pr 4371
This theorem depends on definitions:  df-bi 178  df-or 360  df-an 361  df-3an 938  df-tru 1325  df-ex 1548  df-nf 1551  df-sb 1656  df-clab 2399  df-cleq 2405  df-clel 2408  df-nfc 2537  df-ne 2577  df-ral 2679  df-rex 2680  df-rab 2683  df-v 2926  df-dif 3291  df-un 3293  df-in 3295  df-ss 3302  df-nul 3597  df-if 3708  df-sn 3788  df-pr 3789  df-op 3791  df-opab 4235  df-mpt 4236  df-xp 4851  df-rel 4852  df-res 4857
  Copyright terms: Public domain W3C validator