Theorem fnssres 6703

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

Syntax hints:   → wi 4   ∧ wa 395   ⊆ wss 3976   ↾ cres 5702   Fn wfn 6568

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1793  ax-4 1807  ax-5 1909  ax-6 1967  ax-7 2007  ax-8 2110  ax-9 2118  ax-ext 2711  ax-sep 5317  ax-nul 5324  ax-pr 5447

This theorem depends on definitions:  df-bi 207  df-an 396  df-or 847  df-3an 1089  df-tru 1540  df-fal 1550  df-ex 1778  df-sb 2065  df-clab 2718  df-cleq 2732  df-clel 2819  df-ral 3068  df-rex 3077  df-rab 3444  df-v 3490  df-dif 3979  df-un 3981  df-in 3983  df-ss 3993  df-nul 4353  df-if 4549  df-sn 4649  df-pr 4651  df-op 4655  df-br 5167  df-opab 5229  df-xp 5706  df-rel 5707  df-cnv 5708  df-co 5709  df-dm 5710  df-res 5712  df-fun 6575  df-fn 6576

This theorem is referenced by:  fnssresd  6704  fnresin1  6705  fnresin2  6706  fnresi  6709  fssres  6787  fvreseq0  7071  fnreseql  7081  ffvresb  7159  fnressn  7192  soisores  7363  oprres  7618  ofres  7733  fsplitfpar  8159  fnsuppres  8232  tfrlem1  8432  tz7.48lem  8497  tz7.49c  8502  resixp  8991  ixpfi2  9420  ttrclss  9789  dfac12lem1  10213  ackbij2lem3  10309  cfsmolem  10339  alephsing  10345  ttukeylem3  10580  iunfo  10608  fpwwe2lem7  10706  mulnzcnf  11936  seqfeq2  14076  seqf1olem2  14093  bpolylem  16096  reeff1  16168  sscres  17884  fullsubc  17914  fullresc  17915  funcres2c  17968  dmaf  18116  cdaf  18117  frmdplusg  18889  frmdss2  18898  gass  19341  dprdfadd  20064  rngmgpf  20184  mgpf  20275  prdscrngd  20345  rnghmresfn  20641  rnghmsscmap2  20651  rnghmsscmap  20652  rhmresfn  20670  rhmsscmap2  20680  rhmsscmap  20681  subrgascl  22113  upxp  23652  uptx  23654  cnmpt1st  23697  cnmpt2nd  23698  cnextfres1  24097  prdstmdd  24153  ressprdsds  24402  prdsxmslem2  24563  xrsdsre  24851  itg1addlem4OLD  25754  recosf1o  26595  resinf1o  26596  mpodvdsmulf1o  27255  dvdsmulf1o  27257  ex-fpar  30494  sspg  30760  ssps  30762  sspmlem  30764  sspn  30768  hhssnv  31296  ressupprn  32702  1stpreimas  32717  cnre2csqlem  33856  raddcn  33875  carsggect  34283  subiwrdlen  34351  signsvtn0  34547  signstres  34552  bnj1253  34993  bnj1280  34996  gblacfnacd  35075  subfacp1lem5  35152  cvmlift2lem9a  35271  filnetlem4  36347  finixpnum  37565  poimirlem4  37584  poimirlem8  37588  ftc1anclem3  37655  isdrngo2  37918  diaintclN  41015  dibintclN  41124  dihintcl  41301  imaiinfv  42649  fnwe2lem2  43008  aomclem6  43016  deg1mhm  43161  limsupvaluz2  45659  supcnvlimsup  45661  limsupgtlem  45698  resincncf  45796  icccncfext  45808  dvnprodlem1  45867  fourierdlem42  46070  fourierdlem73  46100  fdivmpt  48274