Theorem fnssres 6564

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

Syntax hints:   → wi 4   ∧ wa 396   ⊆ wss 3888   ↾ cres 5592   Fn wfn 6432

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 2710  ax-sep 5224  ax-nul 5231  ax-pr 5353

This theorem depends on definitions:  df-bi 206  df-an 397  df-or 845  df-3an 1088  df-tru 1542  df-fal 1552  df-ex 1783  df-sb 2069  df-clab 2717  df-cleq 2731  df-clel 2817  df-ral 3070  df-rex 3071  df-rab 3074  df-v 3435  df-dif 3891  df-un 3893  df-in 3895  df-ss 3905  df-nul 4258  df-if 4461  df-sn 4563  df-pr 4565  df-op 4569  df-br 5076  df-opab 5138  df-xp 5596  df-rel 5597  df-cnv 5598  df-co 5599  df-dm 5600  df-res 5602  df-fun 6439  df-fn 6440

This theorem is referenced by:  fnssresd  6565  fnresin1  6566  fnresin2  6567  fnresi  6570  fssres  6649  fvreseq0  6924  fnreseql  6934  ffvresb  7007  fnressn  7039  soisores  7207  oprres  7449  ofres  7561  fsplitfpar  7968  fnsuppres  8016  tfrlem1  8216  tz7.48lem  8281  tz7.49c  8286  resixp  8730  ixpfi2  9126  ttrclss  9487  dfac12lem1  9908  ackbij2lem3  10006  cfsmolem  10035  alephsing  10041  ttukeylem3  10276  iunfo  10304  fpwwe2lem7  10402  mulnzcnopr  11630  seqfeq2  13755  seqf1olem2  13772  bpolylem  15767  reeff1  15838  sscres  17544  fullsubc  17574  fullresc  17575  funcres2c  17626  dmaf  17773  cdaf  17774  frmdplusg  18502  frmdss2  18511  gass  18916  dprdfadd  19632  mgpf  19807  prdscrngd  19861  subrgascl  21283  mdetrsca  21761  upxp  22783  uptx  22785  cnmpt1st  22828  cnmpt2nd  22829  cnextfres1  23228  prdstmdd  23284  ressprdsds  23533  prdsxmslem2  23694  xrsdsre  23982  itg1addlem4OLD  24873  recosf1o  25700  resinf1o  25701  dvdsmulf1o  26352  ex-fpar  28835  sspg  29099  ssps  29101  sspmlem  29103  sspn  29107  hhssnv  29635  ressupprn  31033  1stpreimas  31047  dimkerim  31717  cnre2csqlem  31869  rmulccn  31887  raddcn  31888  carsggect  32294  subiwrdlen  32362  signsvtn0  32558  signstres  32563  bnj1253  33006  bnj1280  33009  subfacp1lem5  33155  cvmlift2lem9a  33274  filnetlem4  34579  finixpnum  35771  poimirlem4  35790  poimirlem8  35794  ftc1anclem3  35861  isdrngo2  36125  diaintclN  39079  dibintclN  39188  dihintcl  39365  imaiinfv  40522  fnwe2lem2  40883  aomclem6  40891  deg1mhm  41039  limsupvaluz2  43286  supcnvlimsup  43288  limsupgtlem  43325  resincncf  43423  icccncfext  43435  dvnprodlem1  43494  fourierdlem42  43697  fourierdlem73  43727  rnghmresfn  45532  rnghmsscmap2  45542  rnghmsscmap  45543  rhmresfn  45578  rhmsscmap2  45588  rhmsscmap  45589  fdivmpt  45897