Theorem fnssres 6539

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 6538	. 2 ⊢ (𝐹 Fn 𝐴 → ((𝐹 ↾ 𝐵) Fn 𝐵 ↔ 𝐵 ⊆ 𝐴))
2	1	biimpar 477	1 ⊢ ((𝐹 Fn 𝐴 ∧ 𝐵 ⊆ 𝐴) → (𝐹 ↾ 𝐵) Fn 𝐵)

Syntax hints:   → wi 4   ∧ wa 395   ⊆ wss 3883   ↾ cres 5582   Fn wfn 6413

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1799  ax-4 1813  ax-5 1914  ax-6 1972  ax-7 2012  ax-8 2110  ax-9 2118  ax-ext 2709  ax-sep 5218  ax-nul 5225  ax-pr 5347

This theorem depends on definitions:  df-bi 206  df-an 396  df-or 844  df-3an 1087  df-tru 1542  df-fal 1552  df-ex 1784  df-sb 2069  df-clab 2716  df-cleq 2730  df-clel 2817  df-ral 3068  df-rex 3069  df-rab 3072  df-v 3424  df-dif 3886  df-un 3888  df-in 3890  df-ss 3900  df-nul 4254  df-if 4457  df-sn 4559  df-pr 4561  df-op 4565  df-br 5071  df-opab 5133  df-xp 5586  df-rel 5587  df-cnv 5588  df-co 5589  df-dm 5590  df-res 5592  df-fun 6420  df-fn 6421

This theorem is referenced by:  fnssresd  6540  fnresin1  6541  fnresin2  6542  fnresi  6545  fssres  6624  fvreseq0  6897  fnreseql  6907  ffvresb  6980  fnressn  7012  soisores  7178  oprres  7418  ofres  7530  fsplitfpar  7930  fnsuppres  7978  tfrlem1  8178  tz7.48lem  8242  tz7.49c  8247  resixp  8679  ixpfi2  9047  dfac12lem1  9830  ackbij2lem3  9928  cfsmolem  9957  alephsing  9963  ttukeylem3  10198  iunfo  10226  fpwwe2lem7  10324  mulnzcnopr  11551  seqfeq2  13674  seqf1olem2  13691  bpolylem  15686  reeff1  15757  sscres  17452  fullsubc  17481  fullresc  17482  funcres2c  17533  dmaf  17680  cdaf  17681  frmdplusg  18408  frmdss2  18417  gass  18822  dprdfadd  19538  mgpf  19713  prdscrngd  19767  subrgascl  21184  mdetrsca  21660  upxp  22682  uptx  22684  cnmpt1st  22727  cnmpt2nd  22728  cnextfres1  23127  prdstmdd  23183  ressprdsds  23432  prdsxmslem2  23591  xrsdsre  23879  itg1addlem4OLD  24769  recosf1o  25596  resinf1o  25597  dvdsmulf1o  26248  ex-fpar  28727  sspg  28991  ssps  28993  sspmlem  28995  sspn  28999  hhssnv  29527  ressupprn  30926  1stpreimas  30940  dimkerim  31610  cnre2csqlem  31762  rmulccn  31780  raddcn  31781  carsggect  32185  subiwrdlen  32253  signsvtn0  32449  signstres  32454  bnj1253  32897  bnj1280  32900  subfacp1lem5  33046  cvmlift2lem9a  33165  ttrclss  33706  filnetlem4  34497  finixpnum  35689  poimirlem4  35708  poimirlem8  35712  ftc1anclem3  35779  isdrngo2  36043  diaintclN  38999  dibintclN  39108  dihintcl  39285  imaiinfv  40431  fnwe2lem2  40792  aomclem6  40800  deg1mhm  40948  limsupvaluz2  43169  supcnvlimsup  43171  limsupgtlem  43208  resincncf  43306  icccncfext  43318  dvnprodlem1  43377  fourierdlem42  43580  fourierdlem73  43610  rnghmresfn  45409  rnghmsscmap2  45419  rnghmsscmap  45420  rhmresfn  45455  rhmsscmap2  45465  rhmsscmap  45466  fdivmpt  45774