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

Theorem fnssres 5685
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 5684 . 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 3469    |` cres 4994    Fn wfn 5574
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1596  ax-4 1607  ax-5 1675  ax-6 1714  ax-7 1734  ax-9 1766  ax-10 1781  ax-11 1786  ax-12 1798  ax-13 1961  ax-ext 2438  ax-sep 4561  ax-nul 4569  ax-pr 4679
This theorem depends on definitions:  df-bi 185  df-or 370  df-an 371  df-3an 970  df-tru 1377  df-ex 1592  df-nf 1595  df-sb 1707  df-clab 2446  df-cleq 2452  df-clel 2455  df-nfc 2610  df-ne 2657  df-ral 2812  df-rex 2813  df-rab 2816  df-v 3108  df-dif 3472  df-un 3474  df-in 3476  df-ss 3483  df-nul 3779  df-if 3933  df-sn 4021  df-pr 4023  df-op 4027  df-br 4441  df-opab 4499  df-xp 4998  df-rel 4999  df-cnv 5000  df-co 5001  df-dm 5002  df-res 5004  df-fun 5581  df-fn 5582
This theorem is referenced by:  fnresin1  5686  fnresin2  5687  fssres  5742  fvreseq0  5972  fnreseql  5982  ffvresb  6043  fnressn  6064  fnsuppresOLD  6112  soisores  6202  ofres  6530  fnsuppres  6917  tfrlem1  7035  tz7.48lem  7096  tz7.49c  7101  resixp  7494  ixpfi2  7807  dfac12lem1  8512  ackbij2lem3  8610  cfsmolem  8639  alephsing  8645  ttukeylem3  8880  iunfo  8903  fpwwe2lem8  9004  mulnzcnopr  10184  seqfeq2  12086  seqf1olem2  12103  hashgval2  12401  swrd0len  12599  swrdccat1  12632  reeff1  13705  eucalg  14064  sscres  15042  fullsubc  15066  fullresc  15067  funcres2c  15117  dmaf  15223  cdaf  15224  frmdplusg  15838  frmdss2  15847  gass  16127  dprdfadd  16843  dprdfaddOLD  16850  mgpf  16990  prdscrngd  17039  subrgascl  17927  mdetrsca  18865  upxp  19852  uptx  19854  cnmpt1st  19897  cnmpt2nd  19898  cnextfres  20296  prdstmdd  20350  ressprdsds  20602  prdsxmslem2  20760  xrsdsre  21043  itg1addlem4  21834  recosf1o  22648  resinf1o  22649  dvdsmulf1o  23191  eupath2lem3  24641  ghgrp  25032  sspg  25303  ssps  25305  sspmlem  25307  sspn  25311  hhssnv  25842  cnre2csqlem  27514  rmulccn  27532  raddcn  27533  subiwrdlen  27951  signsvtn0  28153  signstres  28158  subfacp1lem3  28252  subfacp1lem5  28254  cvmlift2lem9a  28374  nodenselem6  29009  bpolylem  29373  finixpnum  29601  ftc1anclem3  29656  filnetlem4  29789  isdrngo2  29951  imaiinfv  30216  fnwe2lem2  30590  aomclem6  30598  deg1mhm  30761  resincncf  31168  icccncfext  31181  fourierdlem42  31404  fourierdlem73  31435  bnj1253  33027  bnj1280  33030  diaintclN  35730  dibintclN  35839  dihintcl  36016
  Copyright terms: Public domain W3C validator