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

Theorem resmptd 5118
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 5116 . 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 1437    C_ wss 3379    |-> cmpt 4425    |` cres 4798
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1663  ax-4 1676  ax-5 1752  ax-6 1798  ax-7 1843  ax-9 1876  ax-10 1891  ax-11 1896  ax-12 1909  ax-13 2063  ax-ext 2408  ax-sep 4489  ax-nul 4498  ax-pr 4603
This theorem depends on definitions:  df-bi 188  df-or 371  df-an 372  df-3an 984  df-tru 1440  df-ex 1658  df-nf 1662  df-sb 1791  df-clab 2415  df-cleq 2421  df-clel 2424  df-nfc 2558  df-ne 2601  df-ral 2719  df-rex 2720  df-rab 2723  df-v 3024  df-dif 3382  df-un 3384  df-in 3386  df-ss 3393  df-nul 3705  df-if 3855  df-sn 3942  df-pr 3944  df-op 3948  df-opab 4426  df-mpt 4427  df-xp 4802  df-rel 4803  df-res 4808
This theorem is referenced by:  oacomf1olem  7220  cantnfres  8134  rlimres2  13568  lo1res2  13569  o1res2  13570  fsumss  13734  fprodss  13945  conjsubgen  16858  gsumsplit2  17505  gsum2d  17547  dmdprdsplitlem  17613  dprd2dlem1  17617  psrlidm  18570  psrridm  18571  mplmonmul  18631  mplcoe1  18632  mplcoe5  18635  evlsval2  18686  mdetunilem9  19587  cmpfi  20365  ptpjopn  20569  xkoptsub  20611  xkopjcn  20613  cnmpt1res  20633  subgntr  21063  opnsubg  21064  clsnsg  21066  snclseqg  21072  tsmsxplem1  21109  imasdsf1olem  21330  subgnm  21583  mbfss  22544  mbflimsup  22565  mbflimsupOLD  22566  mbfmullem2  22624  iblss  22704  limcres  22783  dvaddbr  22834  dvmulbr  22835  dvcmulf  22841  dvmptres3  22852  dvmptres2  22858  dvmptntr  22867  lhop2  22909  lhop  22910  dvfsumle  22915  dvfsumabs  22917  dvfsumlem2  22921  ftc2ditglem  22939  itgsubstlem  22942  mdegfval  22953  psercn2  23320  psercn  23323  abelth  23338  abelth2  23339  efrlim  23837  jensenlem2  23855  lgamcvg2  23922  pntrsumo1  24345  efghgrpOLD  26043  rabfodom  28083  poimirlem16  31863  poimirlem19  31866  poimirlem30  31877  ftc1anclem8  31931  ftc2nc  31933  areacirclem2  31940  hbtlem6  35901  itgpowd  36012  radcnvrat  36576  disjf1o  37370  cncfmptss  37548  dvmptresicc  37674  dvnprodlem1  37704  iblsplit  37726  itgcoscmulx  37729  itgiccshift  37740  itgperiod  37741  itgsbtaddcnst  37742  dirkercncflem2  37849  dirkercncflem4  37851  fourierdlem28  37880  fourierdlem40  37893  fourierdlem58  37911  fourierdlem74  37927  fourierdlem75  37928  fourierdlem76  37929  fourierdlem78  37931  fourierdlem80  37933  fourierdlem81  37934  fourierdlem84  37937  fourierdlem85  37938  fourierdlem90  37943  fourierdlem93  37946  fourierdlem101  37954  fourierdlem111  37964  sge0lessmpt  38092  sge0gerpmpt  38095  sge0resrnlem  38096  sge0ssrempt  38098  sge0ltfirpmpt  38101  sge0iunmptlemre  38108  sge0lefimpt  38116  sge0ltfirpmpt2  38119  sge0pnffigtmpt  38133  ismeannd  38156  omeiunltfirp  38191  caratheodorylem2  38199  funcrngcsetc  39601  funcrngcsetcALT  39602  funcringcsetc  39638  fdmdifeqresdif  39726  gsumsplit2f  39749
  Copyright terms: Public domain W3C validator