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

Theorem resmpt 5124
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 5123 . 2  |-  ( B 
C_  A  ->  ( { <. x ,  y
>.  |  ( x  e.  A  /\  y  =  C ) }  |`  B )  =  { <. x ,  y >.  |  ( x  e.  B  /\  y  =  C ) } )
2 df-mpt 4202 . . 3  |-  ( x  e.  A  |->  C )  =  { <. x ,  y >.  |  ( x  e.  A  /\  y  =  C ) }
32reseq1i 5075 . 2  |-  ( ( x  e.  A  |->  C )  |`  B )  =  ( { <. x ,  y >.  |  ( x  e.  A  /\  y  =  C ) }  |`  B )
4 df-mpt 4202 . 2  |-  ( x  e.  B  |->  C )  =  { <. x ,  y >.  |  ( x  e.  B  /\  y  =  C ) }
51, 3, 43eqtr4g 2437 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 1717    C_ wss 3256   {copab 4199    e. cmpt 4200    |` cres 4813
This theorem is referenced by:  resmpt3  5125  fvresex  5914  f1stres  6300  f2ndres  6301  tposss  6409  dftpos2  6425  dftpos4  6427  oacomf1olem  6736  resixpfo  7029  cantnfres  7559  rlimres2  12275  lo1res2  12276  o1res2  12277  rlimresb  12279  lo1eq  12282  rlimeq  12283  fsumss  12439  isumclim3  12463  bitsf1ocnv  12876  conjsubg  14957  conjsubgen  14958  odf1o2  15127  sylow1lem2  15153  sylow2blem1  15174  gsumzres  15437  gsumzsplit  15449  gsumsplit2  15451  gsum2d  15466  dmdprdsplitlem  15515  dprd2dlem1  15519  dprd2da  15520  dpjidcl  15536  ablfac1b  15548  psrass1lem  16362  psrlidm  16387  psrridm  16388  mplmonmul  16447  mplcoe1  16448  mplcoe2  16450  coe1mul2lem2  16581  tgrest  17138  cmpfi  17386  ptpjopn  17558  xkoptsub  17600  xkopjcn  17602  cnmptid  17607  cnmpt1res  17622  fmss  17892  txflf  17952  tmdgsum  18039  subgntr  18050  opnsubg  18051  clsnsg  18053  tgpconcomp  18056  snclseqg  18059  tsmssplit  18095  tsmsxplem1  18096  imasdsf1olem  18304  subgnm  18538  iscmet3lem3  19107  mbfss  19398  mbfadd  19413  mbfsub  19414  mbflimsup  19418  mbfmullem2  19476  mbfmul  19478  itg2cnlem1  19513  iblss  19556  ellimc2  19624  limcres  19633  dvreslem  19656  dvres2lem  19657  dvidlem  19662  dvcnp2  19666  dvaddbr  19684  dvmulbr  19685  dvcmulf  19691  dvcobr  19692  dvrec  19701  dvmptres3  19702  dvmptres2  19708  dvmptntr  19717  dvcnvlem  19720  lhop1lem  19757  lhop2  19759  lhop  19760  dvfsumle  19765  dvfsumabs  19767  dvfsumlem2  19771  ftc2ditglem  19789  itgparts  19791  itgsubstlem  19792  evlsval2  19801  tdeglem4  19843  mdegfval  19845  plypf1  19991  taylthlem2  20150  psercn2  20199  psercn  20202  pserdvlem2  20204  abelth  20217  abelth2  20218  pige3  20285  efifo  20309  eff1olem  20310  dvlog2  20404  resqrcn  20493  sqrcn  20494  dvatan  20635  rlimcnp2  20665  xrlimcnp  20667  efrlim  20668  cxp2lim  20675  jensenlem2  20686  chpo1ub  21034  dchrisum0lem2a  21071  pntrsumo1  21119  pnt2  21167  pnt  21168  efghgrp  21802  resmptf  23906  ressnm  24016  rmulccn  24111  xrge0mulc1cn  24124  gsumesum  24240  esumsn  24245  esumcvg  24265  lgamcvg2  24611  divcnvshft  24983  divcnvlin  24984  fprodss  25046  fprodefsum  25070  iprodclim3  25078  itggt0cn  25970  areacirclem4  25977  sdclem2  26130  cncfres  26158  pwssplit4  26853  frlmsplit2  26905  pwfi2f1o  26922  hbtlem6  26995  psgnunilem5  27079  lhe4.4ex1a  27208  cncfmptss  27378  dvcosre  27402  itgsinexplem1  27409
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 1661  ax-8 1682  ax-14 1721  ax-6 1736  ax-7 1741  ax-11 1753  ax-12 1939  ax-ext 2361  ax-sep 4264  ax-nul 4272  ax-pr 4337
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 2367  df-cleq 2373  df-clel 2376  df-nfc 2505  df-ne 2545  df-ral 2647  df-rex 2648  df-rab 2651  df-v 2894  df-dif 3259  df-un 3261  df-in 3263  df-ss 3270  df-nul 3565  df-if 3676  df-sn 3756  df-pr 3757  df-op 3759  df-opab 4201  df-mpt 4202  df-xp 4817  df-rel 4818  df-res 4823
  Copyright terms: Public domain W3C validator