Theorem fnssres 6615

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

Syntax hints:   → wi 4   ∧ wa 395   ⊆ wss 3890   ↾ cres 5626   Fn wfn 6487

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 5231  ax-pr 5370

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 3391  df-v 3432  df-dif 3893  df-un 3895  df-in 3897  df-ss 3907  df-nul 4275  df-if 4468  df-sn 4569  df-pr 4571  df-op 4575  df-br 5087  df-opab 5149  df-xp 5630  df-rel 5631  df-cnv 5632  df-co 5633  df-dm 5634  df-res 5636  df-fun 6494  df-fn 6495

This theorem is referenced by:  fnssresd  6616  fnresin1  6617  fnresin2  6618  fnresi  6621  fssres  6700  fvreseq0  6984  fnreseql  6994  ffvresb  7072  fnressn  7105  soisores  7275  oprres  7528  ofres  7643  fsplitfpar  8061  fnsuppres  8134  tfrlem1  8308  tz7.48lem  8373  tz7.49c  8378  resixp  8874  ixpfi2  9253  ttrclss  9632  dfac12lem1  10057  ackbij2lem3  10153  cfsmolem  10183  alephsing  10189  ttukeylem3  10424  iunfo  10452  fpwwe2lem7  10551  mulnzcnf  11787  seqfeq2  13978  seqf1olem2  13995  bpolylem  16004  reeff1  16078  sscres  17781  fullsubc  17808  fullresc  17809  funcres2c  17861  dmaf  18007  cdaf  18008  frmdplusg  18813  frmdss2  18822  gass  19267  dprdfadd  19988  rngmgpf  20129  mgpf  20220  prdscrngd  20292  rnghmresfn  20587  rnghmsscmap2  20597  rnghmsscmap  20598  rhmresfn  20616  rhmsscmap2  20626  rhmsscmap  20627  subrgascl  22054  upxp  23598  uptx  23600  cnmpt1st  23643  cnmpt2nd  23644  cnextfres1  24043  prdstmdd  24099  ressprdsds  24346  prdsxmslem2  24504  xrsdsre  24786  recosf1o  26512  resinf1o  26513  mpodvdsmulf1o  27171  dvdsmulf1o  27173  ex-fpar  30547  sspg  30814  ssps  30816  sspmlem  30818  sspn  30822  hhssnv  31350  ressupprn  32778  1stpreimas  32794  cnre2csqlem  34070  raddcn  34089  carsggect  34478  subiwrdlen  34546  signsvtn0  34730  signstres  34735  bnj1253  35175  bnj1280  35178  gblacfnacd  35300  subfacp1lem5  35382  cvmlift2lem9a  35501  filnetlem4  36579  finixpnum  37940  poimirlem4  37959  poimirlem8  37963  ftc1anclem3  38030  isdrngo2  38293  diaintclN  41518  dibintclN  41627  dihintcl  41804  imaiinfv  43139  fnwe2lem2  43497  aomclem6  43505  deg1mhm  43646  limsupvaluz2  46184  supcnvlimsup  46186  limsupgtlem  46223  resincncf  46321  icccncfext  46333  fourierdlem42  46595  fourierdlem73  46625  fdivmpt  49028  slotresfo  49386  basresposfo  49465  oppff1  49635