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

Theorem fnssres 5498
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 5497 . 2  |-  ( F  Fn  A  ->  (
( F  |`  B )  Fn  B  <->  B  C_  A
) )
21biimpar 472 1  |-  ( ( F  Fn  A  /\  B  C_  A )  -> 
( F  |`  B )  Fn  B )
Colors of variables: wff set class
Syntax hints:    -> wi 4    /\ wa 359    C_ wss 3263    |` cres 4820    Fn wfn 5389
This theorem is referenced by:  fnresin1  5499  fnresin2  5500  fssres  5550  fvreseq  5772  fnreseql  5779  ffvresb  5839  fnressn  5857  fnsuppres  5891  soisores  5986  ofres  6260  tz7.48lem  6634  tz7.49c  6639  resixp  7033  ixpfi2  7340  dfac12lem1  7956  ackbij2lem3  8054  cfsmolem  8083  alephsing  8089  ttukeylem3  8324  iunfo  8347  fpwwe2lem8  8445  mulnzcnopr  9600  seqfeq2  11273  seqf1olem2  11290  hashgval2  11579  swrd0len  11696  swrdccat1  11701  reeff1  12648  eucalg  13005  sscres  13950  fullsubc  13974  fullresc  13975  funcres2c  14025  dmaf  14131  cdaf  14132  frmdplusg  14726  frmdss2  14735  gass  15005  dprdfadd  15505  mgpf  15602  prdscrngd  15646  subrgascl  16485  upxp  17576  uptx  17578  cnmpt1st  17621  cnmpt2nd  17622  cnextfres  18020  prdstmdd  18074  ressprdsds  18309  prdsxmslem2  18449  xrsdsre  18712  itg1addlem4  19458  recosf1o  20304  resinf1o  20305  dvdsmulf1o  20846  eupath2lem3  21549  ghgrp  21804  sspg  22075  ssps  22077  sspmlem  22079  sspn  22083  hhssnv  22612  cnre2csqlem  24112  rmulccn  24118  raddcn  24119  subfacp1lem3  24647  subfacp1lem5  24649  cvmlift2lem9a  24769  nodenselem6  25364  bpolylem  25808  filnetlem4  26101  isdrngo2  26265  imaiinfv  26431  fnwe2lem2  26817  aomclem6  26825  deg1mhm  27195  bnj1253  28724  bnj1280  28727  diaintclN  31173  dibintclN  31282  dihintcl  31459
This theorem was proved from axioms:  ax-1 5  ax-2 6  ax-3 7  ax-mp 8  ax-gen 1552  ax-5 1563  ax-17 1623  ax-9 1661  ax-8 1682  ax-14 1721  ax-6 1736  ax-7 1741  ax-11 1753  ax-12 1939  ax-ext 2368  ax-sep 4271  ax-nul 4279  ax-pr 4344
This theorem depends on definitions:  df-bi 178  df-or 360  df-an 361  df-3an 938  df-tru 1325  df-ex 1548  df-nf 1551  df-sb 1656  df-clab 2374  df-cleq 2380  df-clel 2383  df-nfc 2512  df-ne 2552  df-ral 2654  df-rex 2655  df-rab 2658  df-v 2901  df-dif 3266  df-un 3268  df-in 3270  df-ss 3277  df-nul 3572  df-if 3683  df-sn 3763  df-pr 3764  df-op 3766  df-br 4154  df-opab 4208  df-xp 4824  df-rel 4825  df-cnv 4826  df-co 4827  df-dm 4828  df-res 4830  df-fun 5396  df-fn 5397
  Copyright terms: Public domain W3C validator