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

Theorem resmpt 5016
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 5015 . 2  |-  ( B 
C_  A  ->  ( { <. x ,  y
>.  |  ( x  e.  A  /\  y  =  C ) }  |`  B )  =  { <. x ,  y >.  |  ( x  e.  B  /\  y  =  C ) } )
2 df-mpt 4095 . . 3  |-  ( x  e.  A  |->  C )  =  { <. x ,  y >.  |  ( x  e.  A  /\  y  =  C ) }
32reseq1i 4967 . 2  |-  ( ( x  e.  A  |->  C )  |`  B )  =  ( { <. x ,  y >.  |  ( x  e.  A  /\  y  =  C ) }  |`  B )
4 df-mpt 4095 . 2  |-  ( x  e.  B  |->  C )  =  { <. x ,  y >.  |  ( x  e.  B  /\  y  =  C ) }
51, 3, 43eqtr4g 2353 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 1632    e. wcel 1696    C_ wss 3165   {copab 4092    e. cmpt 4093    |` cres 4707
This theorem is referenced by:  resmpt3  5017  fvresex  5778  f1stres  6157  f2ndres  6158  tposss  6251  dftpos2  6267  dftpos4  6269  oacomf1olem  6578  resixpfo  6870  cantnfres  7395  rlimres2  12051  lo1res2  12052  o1res2  12053  rlimresb  12055  lo1eq  12058  rlimeq  12059  fsumss  12214  isumclim3  12238  bitsf1ocnv  12651  conjsubg  14730  conjsubgen  14731  odf1o2  14900  sylow1lem2  14926  sylow2blem1  14947  gsumzres  15210  gsumzsplit  15222  gsumsplit2  15224  gsum2d  15239  dmdprdsplitlem  15288  dprd2dlem1  15292  dprd2da  15293  dpjidcl  15309  ablfac1b  15321  psrass1lem  16139  psrlidm  16164  psrridm  16165  mplmonmul  16224  mplcoe1  16225  mplcoe2  16227  coe1mul2lem2  16361  tgrest  16906  cmpfi  17151  ptpjopn  17322  xkoptsub  17364  xkopjcn  17366  cnmptid  17371  cnmpt1res  17386  fmss  17657  txflf  17717  tmdgsum  17794  subgntr  17805  opnsubg  17806  clsnsg  17808  tgpconcomp  17811  snclseqg  17814  tsmssplit  17850  tsmsxplem1  17851  imasdsf1olem  17953  subgnm  18165  iscmet3lem3  18732  mbfss  19017  mbfadd  19032  mbfsub  19033  mbflimsup  19037  mbfmullem2  19095  mbfmul  19097  itg2cnlem1  19132  iblss  19175  ellimc2  19243  limcres  19252  dvreslem  19275  dvres2lem  19276  dvidlem  19281  dvcnp2  19285  dvaddbr  19303  dvmulbr  19304  dvcmulf  19310  dvcobr  19311  dvrec  19320  dvmptres3  19321  dvmptres2  19327  dvmptntr  19336  dvcnvlem  19339  lhop1lem  19376  lhop2  19378  lhop  19379  dvfsumle  19384  dvfsumabs  19386  dvfsumlem2  19390  ftc2ditglem  19408  itgparts  19410  itgsubstlem  19411  evlsval2  19420  tdeglem4  19462  mdegfval  19464  plypf1  19610  taylthlem2  19769  psercn2  19815  psercn  19818  pserdvlem2  19820  abelth  19833  abelth2  19834  pige3  19901  efifo  19925  eff1olem  19926  dvlog2  20016  resqrcn  20105  sqrcn  20106  dvatan  20247  rlimcnp2  20277  xrlimcnp  20279  efrlim  20280  cxp2lim  20287  jensenlem2  20298  chpo1ub  20645  dchrisum0lem2a  20682  pntrsumo1  20730  pnt2  20778  pnt  20779  efghgrp  21056  resmptf  23238  rmulccn  23316  xrge0mulc1cn  23338  esumsn  23452  esumcvg  23469  itggt0cn  25023  areacirclem4  25030  prsubrtr  25502  sdclem2  26555  cncfres  26588  pwssplit4  27294  frlmsplit2  27346  pwfi2f1o  27363  hbtlem6  27436  psgnunilem5  27520  lhe4.4ex1a  27649  cncfmptss  27820  dvcosre  27844  itgsinexplem1  27851
This theorem was proved from axioms:  ax-1 5  ax-2 6  ax-3 7  ax-mp 8  ax-gen 1536  ax-5 1547  ax-17 1606  ax-9 1644  ax-8 1661  ax-14 1700  ax-6 1715  ax-7 1720  ax-11 1727  ax-12 1878  ax-ext 2277  ax-sep 4157  ax-nul 4165  ax-pr 4230
This theorem depends on definitions:  df-bi 177  df-or 359  df-an 360  df-3an 936  df-tru 1310  df-ex 1532  df-nf 1535  df-sb 1639  df-clab 2283  df-cleq 2289  df-clel 2292  df-nfc 2421  df-ne 2461  df-ral 2561  df-rex 2562  df-rab 2565  df-v 2803  df-dif 3168  df-un 3170  df-in 3172  df-ss 3179  df-nul 3469  df-if 3579  df-sn 3659  df-pr 3660  df-op 3662  df-opab 4094  df-mpt 4095  df-xp 4711  df-rel 4712  df-res 4717
  Copyright terms: Public domain W3C validator