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

Theorem resmpt 5191
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 5190 . 2  |-  ( B 
C_  A  ->  ( { <. x ,  y
>.  |  ( x  e.  A  /\  y  =  C ) }  |`  B )  =  { <. x ,  y >.  |  ( x  e.  B  /\  y  =  C ) } )
2 df-mpt 4268 . . 3  |-  ( x  e.  A  |->  C )  =  { <. x ,  y >.  |  ( x  e.  A  /\  y  =  C ) }
32reseq1i 5142 . 2  |-  ( ( x  e.  A  |->  C )  |`  B )  =  ( { <. x ,  y >.  |  ( x  e.  A  /\  y  =  C ) }  |`  B )
4 df-mpt 4268 . 2  |-  ( x  e.  B  |->  C )  =  { <. x ,  y >.  |  ( x  e.  B  /\  y  =  C ) }
51, 3, 43eqtr4g 2493 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 1652    e. wcel 1725    C_ wss 3320   {copab 4265    e. cmpt 4266    |` cres 4880
This theorem is referenced by:  resmpt3  5192  fvresex  5982  f1stres  6368  f2ndres  6369  tposss  6480  dftpos2  6496  dftpos4  6498  oacomf1olem  6807  resixpfo  7100  cantnfres  7633  rlimres2  12355  lo1res2  12356  o1res2  12357  rlimresb  12359  lo1eq  12362  rlimeq  12363  fsumss  12519  isumclim3  12543  bitsf1ocnv  12956  conjsubg  15037  conjsubgen  15038  odf1o2  15207  sylow1lem2  15233  sylow2blem1  15254  gsumzres  15517  gsumzsplit  15529  gsumsplit2  15531  gsum2d  15546  dmdprdsplitlem  15595  dprd2dlem1  15599  dprd2da  15600  dpjidcl  15616  ablfac1b  15628  psrass1lem  16442  psrlidm  16467  psrridm  16468  mplmonmul  16527  mplcoe1  16528  mplcoe2  16530  coe1mul2lem2  16661  tgrest  17223  cmpfi  17471  ptpjopn  17644  xkoptsub  17686  xkopjcn  17688  cnmptid  17693  cnmpt1res  17708  fmss  17978  txflf  18038  tmdgsum  18125  subgntr  18136  opnsubg  18137  clsnsg  18139  tgpconcomp  18142  snclseqg  18145  tsmssplit  18181  tsmsxplem1  18182  imasdsf1olem  18403  subgnm  18674  iscmet3lem3  19243  mbfss  19538  mbfadd  19553  mbfsub  19554  mbflimsup  19558  mbfmullem2  19616  mbfmul  19618  itg2cnlem1  19653  iblss  19696  ellimc2  19764  limcres  19773  dvreslem  19796  dvres2lem  19797  dvidlem  19802  dvcnp2  19806  dvaddbr  19824  dvmulbr  19825  dvcmulf  19831  dvcobr  19832  dvrec  19841  dvmptres3  19842  dvmptres2  19848  dvmptntr  19857  dvcnvlem  19860  lhop1lem  19897  lhop2  19899  lhop  19900  dvfsumle  19905  dvfsumabs  19907  dvfsumlem2  19911  ftc2ditglem  19929  itgparts  19931  itgsubstlem  19932  evlsval2  19941  tdeglem4  19983  mdegfval  19985  plypf1  20131  taylthlem2  20290  psercn2  20339  psercn  20342  pserdvlem2  20344  abelth  20357  abelth2  20358  pige3  20425  efifo  20449  eff1olem  20450  dvlog2  20544  resqrcn  20633  sqrcn  20634  dvatan  20775  rlimcnp2  20805  xrlimcnp  20807  efrlim  20808  cxp2lim  20815  jensenlem2  20826  chpo1ub  21174  dchrisum0lem2a  21211  pntrsumo1  21259  pnt2  21307  pnt  21308  efghgrp  21961  resmptf  24071  ressnm  24184  rmulccn  24314  xrge0mulc1cn  24327  gsumesum  24451  esumsn  24456  esumcvg  24476  lgamcvg2  24839  divcnvshft  25211  divcnvlin  25212  fprodss  25274  fprodefsum  25298  iprodclim3  25313  itggt0cn  26277  ftc1anclem3  26282  ftc1anclem8  26287  ftc2nc  26289  areacirclem2  26293  areacirc  26297  sdclem2  26446  cncfres  26474  pwssplit4  27168  frlmsplit2  27220  pwfi2f1o  27237  hbtlem6  27310  psgnunilem5  27394  lhe4.4ex1a  27523  cncfmptss  27693  dvcosre  27717  itgsinexplem1  27724
This theorem was proved from axioms:  ax-1 5  ax-2 6  ax-3 7  ax-mp 8  ax-gen 1555  ax-5 1566  ax-17 1626  ax-9 1666  ax-8 1687  ax-14 1729  ax-6 1744  ax-7 1749  ax-11 1761  ax-12 1950  ax-ext 2417  ax-sep 4330  ax-nul 4338  ax-pr 4403
This theorem depends on definitions:  df-bi 178  df-or 360  df-an 361  df-3an 938  df-tru 1328  df-ex 1551  df-nf 1554  df-sb 1659  df-clab 2423  df-cleq 2429  df-clel 2432  df-nfc 2561  df-ne 2601  df-ral 2710  df-rex 2711  df-rab 2714  df-v 2958  df-dif 3323  df-un 3325  df-in 3327  df-ss 3334  df-nul 3629  df-if 3740  df-sn 3820  df-pr 3821  df-op 3823  df-opab 4267  df-mpt 4268  df-xp 4884  df-rel 4885  df-res 4890
  Copyright terms: Public domain W3C validator