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

Theorem resmpt 5000
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 4999 . 2  |-  ( B 
C_  A  ->  ( { <. x ,  y
>.  |  ( x  e.  A  /\  y  =  C ) }  |`  B )  =  { <. x ,  y >.  |  ( x  e.  B  /\  y  =  C ) } )
2 df-mpt 4079 . . 3  |-  ( x  e.  A  |->  C )  =  { <. x ,  y >.  |  ( x  e.  A  /\  y  =  C ) }
32reseq1i 4951 . 2  |-  ( ( x  e.  A  |->  C )  |`  B )  =  ( { <. x ,  y >.  |  ( x  e.  A  /\  y  =  C ) }  |`  B )
4 df-mpt 4079 . 2  |-  ( x  e.  B  |->  C )  =  { <. x ,  y >.  |  ( x  e.  B  /\  y  =  C ) }
51, 3, 43eqtr4g 2340 1  |-  ( B 
C_  A  ->  (
( x  e.  A  |->  C )  |`  B )  =  ( x  e.  B  |->  C ) )
Colors of variables: wff set class
Syntax hints:    -> wi 4    /\ wa 358    = wceq 1623    e. wcel 1684    C_ wss 3152   {copab 4076    e. cmpt 4077    |` cres 4691
This theorem is referenced by:  resmpt3  5001  fvresex  5762  f1stres  6141  f2ndres  6142  tposss  6235  dftpos2  6251  dftpos4  6253  oacomf1olem  6562  resixpfo  6854  cantnfres  7379  rlimres2  12035  lo1res2  12036  o1res2  12037  rlimresb  12039  lo1eq  12042  rlimeq  12043  fsumss  12198  isumclim3  12222  bitsf1ocnv  12635  conjsubg  14714  conjsubgen  14715  odf1o2  14884  sylow1lem2  14910  sylow2blem1  14931  gsumzres  15194  gsumzsplit  15206  gsumsplit2  15208  gsum2d  15223  dmdprdsplitlem  15272  dprd2dlem1  15276  dprd2da  15277  dpjidcl  15293  ablfac1b  15305  psrass1lem  16123  psrlidm  16148  psrridm  16149  mplmonmul  16208  mplcoe1  16209  mplcoe2  16211  coe1mul2lem2  16345  tgrest  16890  cmpfi  17135  ptpjopn  17306  xkoptsub  17348  xkopjcn  17350  cnmptid  17355  cnmpt1res  17370  fmss  17641  txflf  17701  tmdgsum  17778  subgntr  17789  opnsubg  17790  clsnsg  17792  tgpconcomp  17795  snclseqg  17798  tsmssplit  17834  tsmsxplem1  17835  imasdsf1olem  17937  subgnm  18149  iscmet3lem3  18716  mbfss  19001  mbfadd  19016  mbfsub  19017  mbflimsup  19021  mbfmullem2  19079  mbfmul  19081  itg2cnlem1  19116  iblss  19159  ellimc2  19227  limcres  19236  dvreslem  19259  dvres2lem  19260  dvidlem  19265  dvcnp2  19269  dvaddbr  19287  dvmulbr  19288  dvcmulf  19294  dvcobr  19295  dvrec  19304  dvmptres3  19305  dvmptres2  19311  dvmptntr  19320  dvcnvlem  19323  lhop1lem  19360  lhop2  19362  lhop  19363  dvfsumle  19368  dvfsumabs  19370  dvfsumlem2  19374  ftc2ditglem  19392  itgparts  19394  itgsubstlem  19395  evlsval2  19404  tdeglem4  19446  mdegfval  19448  plypf1  19594  taylthlem2  19753  psercn2  19799  psercn  19802  pserdvlem2  19804  abelth  19817  abelth2  19818  pige3  19885  efifo  19909  eff1olem  19910  dvlog2  20000  resqrcn  20089  sqrcn  20090  dvatan  20231  rlimcnp2  20261  xrlimcnp  20263  efrlim  20264  cxp2lim  20271  jensenlem2  20282  chpo1ub  20629  dchrisum0lem2a  20666  pntrsumo1  20714  pnt2  20762  pnt  20763  efghgrp  21040  resmptf  23223  rmulccn  23301  xrge0mulc1cn  23323  esumsn  23437  esumcvg  23454  areacirclem4  24927  prsubrtr  25399  sdclem2  26452  cncfres  26485  pwssplit4  27191  frlmsplit2  27243  pwfi2f1o  27260  hbtlem6  27333  psgnunilem5  27417  lhe4.4ex1a  27546  cncfmptss  27717  dvcosre  27741  itgsinexplem1  27748
This theorem was proved from axioms:  ax-1 5  ax-2 6  ax-3 7  ax-mp 8  ax-gen 1533  ax-5 1544  ax-17 1603  ax-9 1635  ax-8 1643  ax-14 1688  ax-6 1703  ax-7 1708  ax-11 1715  ax-12 1866  ax-ext 2264  ax-sep 4141  ax-nul 4149  ax-pr 4214
This theorem depends on definitions:  df-bi 177  df-or 359  df-an 360  df-3an 936  df-tru 1310  df-ex 1529  df-nf 1532  df-sb 1630  df-clab 2270  df-cleq 2276  df-clel 2279  df-nfc 2408  df-ne 2448  df-ral 2548  df-rex 2549  df-rab 2552  df-v 2790  df-dif 3155  df-un 3157  df-in 3159  df-ss 3166  df-nul 3456  df-if 3566  df-sn 3646  df-pr 3647  df-op 3649  df-opab 4078  df-mpt 4079  df-xp 4695  df-rel 4696  df-res 4701
  Copyright terms: Public domain W3C validator