Theorem fnssres 6674

Description: Restriction of a function with a subclass of its domain. (Contributed by NM, 2-Aug-1994.)

Assertion

Ref	Expression
fnssres	⊢ ((𝐹 Fn 𝐴 ∧ 𝐵 ⊆ 𝐴) → (𝐹 ↾ 𝐵) Fn 𝐵)

Proof of Theorem fnssres

Step	Hyp	Ref	Expression
1		fnssresb 6673	. 2 ⊢ (𝐹 Fn 𝐴 → ((𝐹 ↾ 𝐵) Fn 𝐵 ↔ 𝐵 ⊆ 𝐴))
2	1	biimpar 479	1 ⊢ ((𝐹 Fn 𝐴 ∧ 𝐵 ⊆ 𝐴) → (𝐹 ↾ 𝐵) Fn 𝐵)

Syntax hints:   → wi 4   ∧ wa 397   ⊆ wss 3949   ↾ cres 5679   Fn wfn 6539

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1798  ax-4 1812  ax-5 1914  ax-6 1972  ax-7 2012  ax-8 2109  ax-9 2117  ax-ext 2704  ax-sep 5300  ax-nul 5307  ax-pr 5428

This theorem depends on definitions:  df-bi 206  df-an 398  df-or 847  df-3an 1090  df-tru 1545  df-fal 1555  df-ex 1783  df-sb 2069  df-clab 2711  df-cleq 2725  df-clel 2811  df-ral 3063  df-rex 3072  df-rab 3434  df-v 3477  df-dif 3952  df-un 3954  df-in 3956  df-ss 3966  df-nul 4324  df-if 4530  df-sn 4630  df-pr 4632  df-op 4636  df-br 5150  df-opab 5212  df-xp 5683  df-rel 5684  df-cnv 5685  df-co 5686  df-dm 5687  df-res 5689  df-fun 6546  df-fn 6547

This theorem is referenced by:  fnssresd  6675  fnresin1  6676  fnresin2  6677  fnresi  6680  fssres  6758  fvreseq0  7040  fnreseql  7050  ffvresb  7124  fnressn  7156  soisores  7324  oprres  7575  ofres  7689  fsplitfpar  8104  fnsuppres  8176  tfrlem1  8376  tz7.48lem  8441  tz7.49c  8446  resixp  8927  ixpfi2  9350  ttrclss  9715  dfac12lem1  10138  ackbij2lem3  10236  cfsmolem  10265  alephsing  10271  ttukeylem3  10506  iunfo  10534  fpwwe2lem7  10632  mulnzcnopr  11860  seqfeq2  13991  seqf1olem2  14008  bpolylem  15992  reeff1  16063  sscres  17770  fullsubc  17800  fullresc  17801  funcres2c  17852  dmaf  17999  cdaf  18000  frmdplusg  18735  frmdss2  18744  gass  19165  dprdfadd  19890  mgpf  20071  prdscrngd  20135  subrgascl  21627  upxp  23127  uptx  23129  cnmpt1st  23172  cnmpt2nd  23173  cnextfres1  23572  prdstmdd  23628  ressprdsds  23877  prdsxmslem2  24038  xrsdsre  24326  itg1addlem4OLD  25217  recosf1o  26044  resinf1o  26045  dvdsmulf1o  26698  ex-fpar  29715  sspg  29981  ssps  29983  sspmlem  29985  sspn  29989  hhssnv  30517  ressupprn  31912  1stpreimas  31927  dimkerim  32712  cnre2csqlem  32890  rmulccn  32908  raddcn  32909  carsggect  33317  subiwrdlen  33385  signsvtn0  33581  signstres  33586  bnj1253  34028  bnj1280  34031  subfacp1lem5  34175  cvmlift2lem9a  34294  gg-rmulccn  35179  filnetlem4  35266  finixpnum  36473  poimirlem4  36492  poimirlem8  36496  ftc1anclem3  36563  isdrngo2  36826  diaintclN  39929  dibintclN  40038  dihintcl  40215  imaiinfv  41431  fnwe2lem2  41793  aomclem6  41801  deg1mhm  41949  limsupvaluz2  44454  supcnvlimsup  44456  limsupgtlem  44493  resincncf  44591  icccncfext  44603  dvnprodlem1  44662  fourierdlem42  44865  fourierdlem73  44895  rngmgpf  46653  rnghmresfn  46861  rnghmsscmap2  46871  rnghmsscmap  46872  rhmresfn  46907  rhmsscmap2  46917  rhmsscmap  46918  fdivmpt  47226