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

Theorem resmptd 5313
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 5311 . 2  |-  ( B 
C_  A  ->  (
( x  e.  A  |->  C )  |`  B )  =  ( x  e.  B  |->  C ) )
31, 2syl 16 1  |-  ( ph  ->  ( ( x  e.  A  |->  C )  |`  B )  =  ( x  e.  B  |->  C ) )
Colors of variables: wff setvar class
Syntax hints:    -> wi 4    = wceq 1398    C_ wss 3461    |-> cmpt 4497    |` cres 4990
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1623  ax-4 1636  ax-5 1709  ax-6 1752  ax-7 1795  ax-9 1827  ax-10 1842  ax-11 1847  ax-12 1859  ax-13 2004  ax-ext 2432  ax-sep 4560  ax-nul 4568  ax-pr 4676
This theorem depends on definitions:  df-bi 185  df-or 368  df-an 369  df-3an 973  df-tru 1401  df-ex 1618  df-nf 1622  df-sb 1745  df-clab 2440  df-cleq 2446  df-clel 2449  df-nfc 2604  df-ne 2651  df-ral 2809  df-rex 2810  df-rab 2813  df-v 3108  df-dif 3464  df-un 3466  df-in 3468  df-ss 3475  df-nul 3784  df-if 3930  df-sn 4017  df-pr 4019  df-op 4023  df-opab 4498  df-mpt 4499  df-xp 4994  df-rel 4995  df-res 5000
This theorem is referenced by:  oacomf1olem  7205  cantnfres  8087  rlimres2  13466  lo1res2  13467  o1res2  13468  fsumss  13629  fprodss  13837  conjsubgen  16498  gsumsplit2  17147  gsum2d  17195  dmdprdsplitlem  17279  dprd2dlem1  17285  psrlidm  18251  psrridm  18253  mplmonmul  18321  mplcoe1  18322  mplcoe5  18326  evlsval2  18384  mdetunilem9  19289  cmpfi  20075  ptpjopn  20279  xkoptsub  20321  xkopjcn  20323  cnmpt1res  20343  subgntr  20771  opnsubg  20772  clsnsg  20774  snclseqg  20780  tsmsxplem1  20821  imasdsf1olem  21042  subgnm  21313  mbfss  22219  mbflimsup  22239  mbfmullem2  22297  iblss  22377  limcres  22456  dvaddbr  22507  dvmulbr  22508  dvcmulf  22514  dvmptres3  22525  dvmptres2  22531  dvmptntr  22540  lhop2  22582  lhop  22583  dvfsumle  22588  dvfsumabs  22590  dvfsumlem2  22594  ftc2ditglem  22612  itgsubstlem  22615  mdegfval  22626  psercn2  22984  psercn  22987  abelth  23002  abelth2  23003  efrlim  23497  jensenlem2  23515  pntrsumo1  23948  efghgrpOLD  25573  rabfodom  27603  lgamcvg2  28861  ftc1anclem8  30337  ftc2nc  30339  areacirclem2  30348  hbtlem6  31319  itgpowd  31423  radcnvrat  31436  cncfmptss  31820  dvmptresicc  31955  dvnprodlem1  31982  iblsplit  32004  itgcoscmulx  32007  itgiccshift  32018  itgperiod  32019  itgsbtaddcnst  32020  dirkercncflem2  32125  dirkercncflem4  32127  fourierdlem28  32156  fourierdlem40  32168  fourierdlem58  32186  fourierdlem74  32202  fourierdlem75  32203  fourierdlem76  32204  fourierdlem78  32206  fourierdlem80  32208  fourierdlem81  32209  fourierdlem84  32212  fourierdlem85  32213  fourierdlem90  32218  fourierdlem93  32221  fourierdlem101  32229  fourierdlem111  32239  funcrngcsetc  33060  funcrngcsetcALT  33061  funcringcsetc  33097  fdmdifeqresdif  33185  gsumsplit2f  33208
  Copyright terms: Public domain W3C validator