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

Theorem resmptd 5175
Description: Restriction of the mapping operation, deduction form. (Contributed by Glauco Siliprandi, 11-Dec-2019.)
Hypothesis
Ref Expression
resmptd.b  |-  ( ph  ->  B  C_  A )
Assertion
Ref Expression
resmptd  |-  ( ph  ->  ( ( x  e.  A  |->  C )  |`  B )  =  ( x  e.  B  |->  C ) )
Distinct variable groups:    x, A    x, B
Allowed substitution hints:    ph( x)    C( x)

Proof of Theorem resmptd
StepHypRef Expression
1 resmptd.b . 2  |-  ( ph  ->  B  C_  A )
2 resmpt 5173 . 2  |-  ( B 
C_  A  ->  (
( x  e.  A  |->  C )  |`  B )  =  ( x  e.  B  |->  C ) )
31, 2syl 17 1  |-  ( ph  ->  ( ( x  e.  A  |->  C )  |`  B )  =  ( x  e.  B  |->  C ) )
Colors of variables: wff setvar class
Syntax hints:    -> wi 4    = wceq 1455    C_ wss 3416    |-> cmpt 4475    |` cres 4855
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1680  ax-4 1693  ax-5 1769  ax-6 1816  ax-7 1862  ax-9 1907  ax-10 1926  ax-11 1931  ax-12 1944  ax-13 2102  ax-ext 2442  ax-sep 4539  ax-nul 4548  ax-pr 4653
This theorem depends on definitions:  df-bi 190  df-or 376  df-an 377  df-3an 993  df-tru 1458  df-ex 1675  df-nf 1679  df-sb 1809  df-clab 2449  df-cleq 2455  df-clel 2458  df-nfc 2592  df-ne 2635  df-ral 2754  df-rex 2755  df-rab 2758  df-v 3059  df-dif 3419  df-un 3421  df-in 3423  df-ss 3430  df-nul 3744  df-if 3894  df-sn 3981  df-pr 3983  df-op 3987  df-opab 4476  df-mpt 4477  df-xp 4859  df-rel 4860  df-res 4865
This theorem is referenced by:  oacomf1olem  7291  cantnfres  8208  rlimres2  13674  lo1res2  13675  o1res2  13676  fsumss  13840  fprodss  14051  conjsubgen  16964  gsumsplit2  17611  gsum2d  17653  dmdprdsplitlem  17719  dprd2dlem1  17723  psrlidm  18676  psrridm  18677  mplmonmul  18737  mplcoe1  18738  mplcoe5  18741  evlsval2  18792  mdetunilem9  19694  cmpfi  20472  ptpjopn  20676  xkoptsub  20718  xkopjcn  20720  cnmpt1res  20740  subgntr  21170  opnsubg  21171  clsnsg  21173  snclseqg  21179  tsmsxplem1  21216  imasdsf1olem  21437  subgnm  21690  mbfss  22651  mbflimsup  22672  mbflimsupOLD  22673  mbfmullem2  22731  iblss  22811  limcres  22890  dvaddbr  22941  dvmulbr  22942  dvcmulf  22948  dvmptres3  22959  dvmptres2  22965  dvmptntr  22974  lhop2  23016  lhop  23017  dvfsumle  23022  dvfsumabs  23024  dvfsumlem2  23028  ftc2ditglem  23046  itgsubstlem  23049  mdegfval  23060  psercn2  23427  psercn  23430  abelth  23445  abelth2  23446  efrlim  23944  jensenlem2  23962  lgamcvg2  24029  pntrsumo1  24452  efghgrpOLD  26150  rabfodom  28189  poimirlem16  32001  poimirlem19  32004  poimirlem30  32015  ftc1anclem8  32069  ftc2nc  32071  areacirclem2  32078  hbtlem6  36033  itgpowd  36144  radcnvrat  36707  disjf1o  37504  cncfmptss  37703  dvmptresicc  37829  dvnprodlem1  37859  iblsplit  37881  itgcoscmulx  37884  itgiccshift  37895  itgperiod  37896  itgsbtaddcnst  37897  dirkercncflem2  38004  dirkercncflem4  38006  fourierdlem28  38035  fourierdlem40  38048  fourierdlem58  38066  fourierdlem74  38082  fourierdlem75  38083  fourierdlem76  38084  fourierdlem78  38086  fourierdlem80  38088  fourierdlem81  38089  fourierdlem84  38092  fourierdlem85  38093  fourierdlem90  38098  fourierdlem93  38101  fourierdlem101  38109  fourierdlem111  38119  sge0lessmpt  38279  sge0gerpmpt  38282  sge0resrnlem  38283  sge0ssrempt  38285  sge0ltfirpmpt  38288  sge0iunmptlemre  38295  sge0lefimpt  38303  sge0ltfirpmpt2  38306  sge0pnffigtmpt  38320  ismeannd  38343  omeiunltfirp  38378  caratheodorylem2  38386  funcrngcsetc  40273  funcrngcsetcALT  40274  funcringcsetc  40310  fdmdifeqresdif  40396  gsumsplit2f  40419
  Copyright terms: Public domain W3C validator