Theorem fnssres 6691

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

Syntax hints:   → wi 4   ∧ wa 395   ⊆ wss 3951   ↾ cres 5687   Fn wfn 6556

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1795  ax-4 1809  ax-5 1910  ax-6 1967  ax-7 2007  ax-8 2110  ax-9 2118  ax-ext 2708  ax-sep 5296  ax-nul 5306  ax-pr 5432

This theorem depends on definitions:  df-bi 207  df-an 396  df-or 849  df-3an 1089  df-tru 1543  df-fal 1553  df-ex 1780  df-sb 2065  df-clab 2715  df-cleq 2729  df-clel 2816  df-ral 3062  df-rex 3071  df-rab 3437  df-v 3482  df-dif 3954  df-un 3956  df-in 3958  df-ss 3968  df-nul 4334  df-if 4526  df-sn 4627  df-pr 4629  df-op 4633  df-br 5144  df-opab 5206  df-xp 5691  df-rel 5692  df-cnv 5693  df-co 5694  df-dm 5695  df-res 5697  df-fun 6563  df-fn 6564

This theorem is referenced by:  fnssresd  6692  fnresin1  6693  fnresin2  6694  fnresi  6697  fssres  6774  fvreseq0  7058  fnreseql  7068  ffvresb  7145  fnressn  7178  soisores  7347  oprres  7601  ofres  7716  fsplitfpar  8143  fnsuppres  8216  tfrlem1  8416  tz7.48lem  8481  tz7.49c  8486  resixp  8973  ixpfi2  9390  ttrclss  9760  dfac12lem1  10184  ackbij2lem3  10280  cfsmolem  10310  alephsing  10316  ttukeylem3  10551  iunfo  10579  fpwwe2lem7  10677  mulnzcnf  11909  seqfeq2  14066  seqf1olem2  14083  bpolylem  16084  reeff1  16156  sscres  17867  fullsubc  17895  fullresc  17896  funcres2c  17948  dmaf  18094  cdaf  18095  frmdplusg  18867  frmdss2  18876  gass  19319  dprdfadd  20040  rngmgpf  20154  mgpf  20245  prdscrngd  20319  rnghmresfn  20619  rnghmsscmap2  20629  rnghmsscmap  20630  rhmresfn  20648  rhmsscmap2  20658  rhmsscmap  20659  subrgascl  22090  upxp  23631  uptx  23633  cnmpt1st  23676  cnmpt2nd  23677  cnextfres1  24076  prdstmdd  24132  ressprdsds  24381  prdsxmslem2  24542  xrsdsre  24832  recosf1o  26577  resinf1o  26578  mpodvdsmulf1o  27237  dvdsmulf1o  27239  ex-fpar  30481  sspg  30747  ssps  30749  sspmlem  30751  sspn  30755  hhssnv  31283  ressupprn  32699  1stpreimas  32715  cnre2csqlem  33909  raddcn  33928  carsggect  34320  subiwrdlen  34388  signsvtn0  34585  signstres  34590  bnj1253  35031  bnj1280  35034  gblacfnacd  35113  subfacp1lem5  35189  cvmlift2lem9a  35308  filnetlem4  36382  finixpnum  37612  poimirlem4  37631  poimirlem8  37635  ftc1anclem3  37702  isdrngo2  37965  diaintclN  41060  dibintclN  41169  dihintcl  41346  imaiinfv  42704  fnwe2lem2  43063  aomclem6  43071  deg1mhm  43212  limsupvaluz2  45753  supcnvlimsup  45755  limsupgtlem  45792  resincncf  45890  icccncfext  45902  fourierdlem42  46164  fourierdlem73  46194  fdivmpt  48461