Theorem resmptd 5452

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

Step	Hyp	Ref	Expression
1		resmptd.b	. 2 |- ( ph -> B C_ A )
2		resmpt 5449	. 2 |- ( B C_ A -> ( ( x e. A |-> C ) |` B ) = ( x e. B |-> C ) )
3	1, 2	syl 17	1 |- ( ph -> ( ( x e. A |-> C ) |` B ) = ( x e. B |-> C ) )

Syntax hints:   -> wi 4   = wceq 1483   C_ wss 3574   |-> cmpt 4729   |` cres 5116

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1722  ax-4 1737  ax-5 1839  ax-6 1888  ax-7 1935  ax-9 1999  ax-10 2019  ax-11 2034  ax-12 2047  ax-13 2246  ax-ext 2602  ax-sep 4781  ax-nul 4789  ax-pr 4906

This theorem depends on definitions:  df-bi 197  df-or 385  df-an 386  df-3an 1039  df-tru 1486  df-ex 1705  df-nf 1710  df-sb 1881  df-clab 2609  df-cleq 2615  df-clel 2618  df-nfc 2753  df-rab 2921  df-v 3202  df-dif 3577  df-un 3579  df-in 3581  df-ss 3588  df-nul 3916  df-if 4087  df-sn 4178  df-pr 4180  df-op 4184  df-opab 4713  df-mpt 4730  df-xp 5120  df-rel 5121  df-res 5126

This theorem is referenced by:  oacomf1olem  7644  cantnfres  8574  rlimres2  14292  lo1res2  14293  o1res2  14294  fsumss  14456  fprodss  14678  conjsubgen  17693  gsumsplit2  18329  gsum2d  18371  dmdprdsplitlem  18436  dprd2dlem1  18440  psrlidm  19403  psrridm  19404  mplmonmul  19464  mplcoe1  19465  mplcoe5  19468  evlsval2  19520  mdetunilem9  20426  cmpfi  21211  ptpjopn  21415  xkoptsub  21457  xkopjcn  21459  cnmpt1res  21479  subgntr  21910  opnsubg  21911  clsnsg  21913  snclseqg  21919  tsmsxplem1  21956  imasdsf1olem  22178  subgnm  22437  mbfss  23413  mbflimsup  23433  mbfmullem2  23491  iblss  23571  limcres  23650  dvaddbr  23701  dvmulbr  23702  dvcmulf  23708  dvmptres3  23719  dvmptres2  23725  dvmptntr  23734  lhop2  23778  lhop  23779  dvfsumle  23784  dvfsumabs  23786  dvfsumlem2  23790  ftc2ditglem  23808  itgsubstlem  23811  mdegfval  23822  psercn2  24177  psercn  24180  abelth  24195  abelth2  24196  efrlim  24696  jensenlem2  24714  lgamcvg2  24781  pntrsumo1  25254  eucrct2eupth  27105  rabfodom  29344  poimirlem16  33425  poimirlem19  33428  poimirlem30  33439  ftc1anclem8  33492  ftc2nc  33494  areacirclem2  33501  hbtlem6  37699  itgpowd  37800  radcnvrat  38513  disjf1o  39378  cncfmptss  39819  limsupvaluzmpt  39949  supcnvlimsupmpt  39973  dvmptresicc  40134  dvnprodlem1  40161  iblsplit  40182  itgcoscmulx  40185  itgiccshift  40196  itgperiod  40197  itgsbtaddcnst  40198  dirkercncflem2  40321  dirkercncflem4  40323  fourierdlem28  40352  fourierdlem40  40364  fourierdlem58  40381  fourierdlem74  40397  fourierdlem75  40398  fourierdlem76  40399  fourierdlem78  40401  fourierdlem80  40403  fourierdlem81  40404  fourierdlem84  40407  fourierdlem85  40408  fourierdlem90  40413  fourierdlem93  40416  fourierdlem101  40424  fourierdlem111  40434  sge0lessmpt  40616  sge0gerpmpt  40619  sge0resrnlem  40620  sge0ssrempt  40622  sge0ltfirpmpt  40625  sge0iunmptlemre  40632  sge0lefimpt  40640  sge0ltfirpmpt2  40643  sge0pnffigtmpt  40657  ismeannd  40684  omeiunltfirp  40733  caratheodorylem2  40741  sssmfmpt  40959  funcrngcsetc  41998  funcrngcsetcALT  41999  funcringcsetc  42035  fdmdifeqresdif  42120  gsumsplit2f  42143