Theorem fnssres 6623

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

Syntax hints:   → wi 4   ∧ wa 395   ⊆ wss 3903   ↾ cres 5634   Fn wfn 6495

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1797  ax-4 1811  ax-5 1912  ax-6 1969  ax-7 2010  ax-8 2116  ax-9 2124  ax-ext 2709  ax-sep 5243  ax-pr 5379

This theorem depends on definitions:  df-bi 207  df-an 396  df-or 849  df-3an 1089  df-tru 1545  df-fal 1555  df-ex 1782  df-sb 2069  df-clab 2716  df-cleq 2729  df-clel 2812  df-ral 3053  df-rex 3063  df-rab 3402  df-v 3444  df-dif 3906  df-un 3908  df-in 3910  df-ss 3920  df-nul 4288  df-if 4482  df-sn 4583  df-pr 4585  df-op 4589  df-br 5101  df-opab 5163  df-xp 5638  df-rel 5639  df-cnv 5640  df-co 5641  df-dm 5642  df-res 5644  df-fun 6502  df-fn 6503

This theorem is referenced by:  fnssresd  6624  fnresin1  6625  fnresin2  6626  fnresi  6629  fssres  6708  fvreseq0  6992  fnreseql  7002  ffvresb  7080  fnressn  7113  soisores  7283  oprres  7536  ofres  7651  fsplitfpar  8070  fnsuppres  8143  tfrlem1  8317  tz7.48lem  8382  tz7.49c  8387  resixp  8883  ixpfi2  9262  ttrclss  9641  dfac12lem1  10066  ackbij2lem3  10162  cfsmolem  10192  alephsing  10198  ttukeylem3  10433  iunfo  10461  fpwwe2lem7  10560  mulnzcnf  11795  seqfeq2  13960  seqf1olem2  13977  bpolylem  15983  reeff1  16057  sscres  17759  fullsubc  17786  fullresc  17787  funcres2c  17839  dmaf  17985  cdaf  17986  frmdplusg  18791  frmdss2  18800  gass  19242  dprdfadd  19963  rngmgpf  20104  mgpf  20195  prdscrngd  20269  rnghmresfn  20564  rnghmsscmap2  20574  rnghmsscmap  20575  rhmresfn  20593  rhmsscmap2  20603  rhmsscmap  20604  subrgascl  22033  upxp  23579  uptx  23581  cnmpt1st  23624  cnmpt2nd  23625  cnextfres1  24024  prdstmdd  24080  ressprdsds  24327  prdsxmslem2  24485  xrsdsre  24767  recosf1o  26512  resinf1o  26513  mpodvdsmulf1o  27172  dvdsmulf1o  27174  ex-fpar  30549  sspg  30815  ssps  30817  sspmlem  30819  sspn  30823  hhssnv  31351  ressupprn  32779  1stpreimas  32795  cnre2csqlem  34087  raddcn  34106  carsggect  34495  subiwrdlen  34563  signsvtn0  34747  signstres  34752  bnj1253  35192  bnj1280  35195  gblacfnacd  35315  subfacp1lem5  35397  cvmlift2lem9a  35516  filnetlem4  36594  finixpnum  37853  poimirlem4  37872  poimirlem8  37876  ftc1anclem3  37943  isdrngo2  38206  diaintclN  41431  dibintclN  41540  dihintcl  41717  imaiinfv  43047  fnwe2lem2  43405  aomclem6  43413  deg1mhm  43554  limsupvaluz2  46093  supcnvlimsup  46095  limsupgtlem  46132  resincncf  46230  icccncfext  46242  fourierdlem42  46504  fourierdlem73  46534  fdivmpt  48897  slotresfo  49255  basresposfo  49334  oppff1  49504