Theorem fnssres 6648

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

Syntax hints:   → wi 4   ∧ wa 400   ⊆ wss 3907   ↾ cres 5654   Fn wfn 6520

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1818  ax-4 1832  ax-5 1933  ax-6 1990  ax-7 2031  ax-8 2147  ax-9 2155  ax-ext 2737  ax-sep 5251  ax-pr 5395

This theorem depends on definitions:  df-bi 210  df-an 401  df-or 861  df-3an 1103  df-tru 1566  df-fal 1576  df-ex 1803  df-sb 2094  df-clab 2744  df-cleq 2757  df-clel 2840  df-ral 3080  df-rex 3090  df-rab 3418  df-v 3459  df-dif 3910  df-un 3912  df-in 3914  df-ss 3924  df-nul 4289  df-if 4484  df-sn 4586  df-pr 4588  df-op 4592  df-br 5106  df-opab 5168  df-xp 5658  df-rel 5659  df-cnv 5660  df-co 5661  df-dm 5662  df-res 5664  df-fun 6527  df-fn 6528

This theorem is referenced by:  fnssresd  6649  fnresin1  6650  fnresin2  6651  fnresi  6654  fssres  6734  fvreseq0  7023  fnreseql  7033  ffvresb  7111  fnressn  7145  soisores  7315  oprres  7568  ofres  7683  fsplitfpar  8101  fnsuppres  8175  tfrlem1  8350  tz7.48lem  8416  tz7.49c  8421  resixp  8919  ixpfi2  9295  ttrclss  9677  dfac12lem1  10115  ackbij2lem3  10211  cfsmolem  10242  alephsing  10248  ttukeylem3  10483  iunfo  10511  fpwwe2lem7  10610  mulnzcnf  11848  seqfeq2  14052  seqf1olem2  14069  bpolylem  16092  reeff1  16166  sscres  17870  fullsubc  17897  fullresc  17898  funcres2c  17950  dmaf  18096  cdaf  18097  frmdplusg  18903  frmdss2  18912  gass  19362  dprdfadd  20083  rngmgpf  20226  mgpf  20321  prdscrngd  20394  rnghmresfn  20695  rnghmsscmap2  20705  rnghmsscmap  20706  rhmresfn  20724  rhmsscmap2  20734  rhmsscmap  20735  subrgascl  22177  upxp  23741  uptx  23743  cnmpt1st  23786  cnmpt2nd  23787  cnextfres1  24186  prdstmdd  24242  ressprdsds  24489  prdsxmslem2  24647  xrsdsre  24929  recosf1o  26658  resinf1o  26659  mpodvdsmulf1o  27316  dvdsmulf1o  27318  ex-fpar  30722  sspg  30989  ssps  30991  sspmlem  30993  sspn  30997  hhssnv  31525  ressupprn  32947  1stpreimas  32963  cnre2csqlem  34217  raddcn  34236  carsggect  34625  subiwrdlen  34693  signsvtn0  34874  signstres  34879  bnj1253  35322  bnj1280  35325  gblacfnacd  35457  subfacp1lem5  35547  cvmlift2lem9a  35666  filnetlem4  36754  finixpnum  38116  poimirlem4  38135  poimirlem8  38139  ftc1anclem3  38206  isdrngo2  38469  diaintclN  41694  dibintclN  41803  dihintcl  41980  imaiinfv  43286  fnwe2lem2  43640  aomclem6  43648  deg1mhm  43789  limsupvaluz2  46310  supcnvlimsup  46312  limsupgtlem  46349  resincncf  46447  icccncfext  46459  fourierdlem42  46721  fourierdlem73  46751  fdivmpt  49171  slotresfo  49528  basresposfo  49607  oppff1  49777