Theorem fnssres 6640

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

Syntax hints:   → wi 4   ∧ wa 399   ⊆ wss 3904   ↾ cres 5647   Fn wfn 6512

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1814  ax-4 1828  ax-5 1929  ax-6 1986  ax-7 2027  ax-8 2143  ax-9 2151  ax-ext 2733  ax-sep 5245  ax-pr 5389

This theorem depends on definitions:  df-bi 209  df-an 400  df-or 859  df-3an 1099  df-tru 1562  df-fal 1572  df-ex 1799  df-sb 2090  df-clab 2740  df-cleq 2753  df-clel 2836  df-ral 3076  df-rex 3086  df-rab 3414  df-v 3455  df-dif 3907  df-un 3909  df-in 3911  df-ss 3921  df-nul 4286  df-if 4480  df-sn 4582  df-pr 4584  df-op 4588  df-br 5100  df-opab 5162  df-xp 5651  df-rel 5652  df-cnv 5653  df-co 5654  df-dm 5655  df-res 5657  df-fun 6519  df-fn 6520

This theorem is referenced by:  fnssresd  6641  fnresin1  6642  fnresin2  6643  fnresi  6646  fssres  6726  fvreseq0  7015  fnreseql  7025  ffvresb  7103  fnressn  7137  soisores  7307  oprres  7560  ofres  7675  fsplitfpar  8092  fnsuppres  8166  tfrlem1  8341  tz7.48lem  8407  tz7.49c  8412  resixp  8911  ixpfi2  9290  ttrclss  9672  dfac12lem1  10097  ackbij2lem3  10193  cfsmolem  10224  alephsing  10230  ttukeylem3  10465  iunfo  10493  fpwwe2lem7  10592  mulnzcnf  11830  seqfeq2  14035  seqf1olem2  14052  bpolylem  16061  reeff1  16135  sscres  17839  fullsubc  17866  fullresc  17867  funcres2c  17919  dmaf  18065  cdaf  18066  frmdplusg  18871  frmdss2  18880  gass  19324  dprdfadd  20045  rngmgpf  20186  mgpf  20277  prdscrngd  20349  rnghmresfn  20648  rnghmsscmap2  20658  rnghmsscmap  20659  rhmresfn  20677  rhmsscmap2  20687  rhmsscmap  20688  subrgascl  22099  upxp  23663  uptx  23665  cnmpt1st  23708  cnmpt2nd  23709  cnextfres1  24108  prdstmdd  24164  ressprdsds  24411  prdsxmslem2  24569  xrsdsre  24851  recosf1o  26577  resinf1o  26578  mpodvdsmulf1o  27235  dvdsmulf1o  27237  ex-fpar  30610  sspg  30877  ssps  30879  sspmlem  30881  sspn  30885  hhssnv  31413  ressupprn  32842  1stpreimas  32858  cnre2csqlem  34168  raddcn  34187  carsggect  34576  subiwrdlen  34644  signsvtn0  34828  signstres  34833  bnj1253  35276  bnj1280  35279  gblacfnacd  35409  subfacp1lem5  35498  cvmlift2lem9a  35617  filnetlem4  36705  finixpnum  38068  poimirlem4  38087  poimirlem8  38091  ftc1anclem3  38158  isdrngo2  38421  diaintclN  41646  dibintclN  41755  dihintcl  41932  imaiinfv  43238  fnwe2lem2  43592  aomclem6  43600  deg1mhm  43741  limsupvaluz2  46276  supcnvlimsup  46278  limsupgtlem  46315  resincncf  46413  icccncfext  46425  fourierdlem42  46687  fourierdlem73  46717  fdivmpt  49126  slotresfo  49484  basresposfo  49563  oppff1  49733