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

Theorem fnssres 5357
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 5356 . 2  |-  ( F  Fn  A  ->  (
( F  |`  B )  Fn  B  <->  B  C_  A
) )
21biimpar 471 1  |-  ( ( F  Fn  A  /\  B  C_  A )  -> 
( F  |`  B )  Fn  B )
Colors of variables: wff set class
Syntax hints:    -> wi 4    /\ wa 358    C_ wss 3152    |` cres 4691    Fn wfn 5250
This theorem is referenced by:  fnresin1  5358  fnresin2  5359  fssres  5408  fvreseq  5628  fnreseql  5635  ffvresb  5690  fnressn  5705  fnsuppres  5732  soisores  5824  ofres  6094  tz7.48lem  6453  tz7.49c  6458  resixp  6851  ixpfi2  7154  dfac12lem1  7769  ackbij2lem3  7867  cfsmolem  7896  alephsing  7902  ttukeylem3  8138  iunfo  8161  fpwwe2lem8  8259  mulnzcnopr  9414  seqfeq2  11069  seqf1olem2  11086  hashgval2  11360  swrd0len  11455  swrdccat1  11460  reeff1  12400  eucalg  12757  sscres  13700  fullsubc  13724  fullresc  13725  funcres2c  13775  dmaf  13881  cdaf  13882  frmdplusg  14476  frmdss2  14485  gass  14755  dprdfadd  15255  mgpf  15352  prdscrngd  15396  subrgascl  16239  upxp  17317  uptx  17319  cnmpt1st  17362  cnmpt2nd  17363  prdstmdd  17806  ressprdsds  17935  prdsxmslem2  18075  xrsdsre  18316  itg1addlem4  19054  recosf1o  19897  resinf1o  19898  dvdsmulf1o  20434  ghgrp  21035  sspg  21304  ssps  21306  sspmlem  21308  sspn  21312  hhssnv  21841  cnre2csqlem  23294  rmulccn  23301  raddcn  23302  subfacp1lem3  23713  subfacp1lem5  23715  cvmlift2lem9a  23834  eupath2lem3  23903  nodenselem6  24340  bpolylem  24783  valdom  25884  filnetlem4  26330  isdrngo2  26589  imaiinfv  26759  fnwe2lem2  27148  aomclem6  27156  deg1mhm  27526  bnj1253  29047  bnj1280  29050  diaintclN  31248  dibintclN  31357  dihintcl  31534
This theorem was proved from axioms:  ax-1 5  ax-2 6  ax-3 7  ax-mp 8  ax-gen 1533  ax-5 1544  ax-17 1603  ax-9 1635  ax-8 1643  ax-14 1688  ax-6 1703  ax-7 1708  ax-11 1715  ax-12 1866  ax-ext 2264  ax-sep 4141  ax-nul 4149  ax-pr 4214
This theorem depends on definitions:  df-bi 177  df-or 359  df-an 360  df-3an 936  df-tru 1310  df-ex 1529  df-nf 1532  df-sb 1630  df-clab 2270  df-cleq 2276  df-clel 2279  df-nfc 2408  df-ne 2448  df-ral 2548  df-rex 2549  df-rab 2552  df-v 2790  df-dif 3155  df-un 3157  df-in 3159  df-ss 3166  df-nul 3456  df-if 3566  df-sn 3646  df-pr 3647  df-op 3649  df-br 4024  df-opab 4078  df-xp 4695  df-rel 4696  df-cnv 4697  df-co 4698  df-dm 4699  df-res 4701  df-fun 5257  df-fn 5258
  Copyright terms: Public domain W3C validator