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

Theorem fnssres 5684
Description: Restriction of a function with a subclass of its domain. (Contributed by NM, 2-Aug-1994.)
Assertion
Ref Expression
fnssres  |-  ( ( F  Fn  A  /\  B  C_  A )  -> 
( F  |`  B )  Fn  B )

Proof of Theorem fnssres
StepHypRef Expression
1 fnssresb 5683 . 2  |-  ( F  Fn  A  ->  (
( F  |`  B )  Fn  B  <->  B  C_  A
) )
21biimpar 485 1  |-  ( ( F  Fn  A  /\  B  C_  A )  -> 
( F  |`  B )  Fn  B )
Colors of variables: wff setvar class
Syntax hints:    -> wi 4    /\ wa 369    C_ wss 3461    |` cres 4991    Fn wfn 5573
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1605  ax-4 1618  ax-5 1691  ax-6 1734  ax-7 1776  ax-9 1808  ax-10 1823  ax-11 1828  ax-12 1840  ax-13 1985  ax-ext 2421  ax-sep 4558  ax-nul 4566  ax-pr 4676
This theorem depends on definitions:  df-bi 185  df-or 370  df-an 371  df-3an 976  df-tru 1386  df-ex 1600  df-nf 1604  df-sb 1727  df-clab 2429  df-cleq 2435  df-clel 2438  df-nfc 2593  df-ne 2640  df-ral 2798  df-rex 2799  df-rab 2802  df-v 3097  df-dif 3464  df-un 3466  df-in 3468  df-ss 3475  df-nul 3771  df-if 3927  df-sn 4015  df-pr 4017  df-op 4021  df-br 4438  df-opab 4496  df-xp 4995  df-rel 4996  df-cnv 4997  df-co 4998  df-dm 4999  df-res 5001  df-fun 5580  df-fn 5581
This theorem is referenced by:  fnresin1  5685  fnresin2  5686  fssres  5741  fvreseq0  5972  fnreseql  5982  ffvresb  6047  fnressn  6068  fnsuppresOLD  6116  soisores  6208  ofres  6540  fnsuppres  6929  tfrlem1  7047  tz7.48lem  7108  tz7.49c  7113  resixp  7506  ixpfi2  7820  dfac12lem1  8526  ackbij2lem3  8624  cfsmolem  8653  alephsing  8659  ttukeylem3  8894  iunfo  8917  fpwwe2lem8  9018  mulnzcnopr  10202  seqfeq2  12111  seqf1olem2  12128  swrd0len  12630  swrdccat1  12663  reeff1  13836  eucalg  14197  sscres  15173  fullsubc  15197  fullresc  15198  funcres2c  15248  dmaf  15354  cdaf  15355  frmdplusg  16000  frmdss2  16009  gass  16317  dprdfadd  17038  dprdfaddOLD  17045  mgpf  17188  prdscrngd  17240  subrgascl  18141  mdetrsca  19082  upxp  20101  uptx  20103  cnmpt1st  20146  cnmpt2nd  20147  cnextfres  20545  prdstmdd  20599  ressprdsds  20851  prdsxmslem2  21009  xrsdsre  21292  itg1addlem4  22083  recosf1o  22898  resinf1o  22899  dvdsmulf1o  23446  eupath2lem3  24955  ghgrpOLD  25346  sspg  25617  ssps  25619  sspmlem  25621  sspn  25625  hhssnv  26156  cnre2csqlem  27869  rmulccn  27887  raddcn  27888  subiwrdlen  28302  signsvtn0  28504  signstres  28509  subfacp1lem3  28603  subfacp1lem5  28605  cvmlift2lem9a  28725  nodenselem6  29421  bpolylem  29785  finixpnum  30013  ftc1anclem3  30067  filnetlem4  30174  isdrngo2  30336  imaiinfv  30600  fnwe2lem2  30972  aomclem6  30980  deg1mhm  31143  resincncf  31584  icccncfext  31597  fourierdlem42  31820  fourierdlem73  31851  rnghmresfn  32511  rnghmsscmap2  32521  rnghmsscmap  32522  rhmresfn  32554  rhmsscmap2  32564  rhmsscmap  32565  bnj1253  33806  bnj1280  33809  diaintclN  36525  dibintclN  36634  dihintcl  36811
  Copyright terms: Public domain W3C validator