Theorem fnssres 6609

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

Syntax hints:   → wi 4   ∧ wa 395   ⊆ wss 3905   ↾ cres 5625   Fn wfn 6481

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 2008  ax-8 2111  ax-9 2119  ax-ext 2701  ax-sep 5238  ax-nul 5248  ax-pr 5374

This theorem depends on definitions:  df-bi 207  df-an 396  df-or 848  df-3an 1088  df-tru 1543  df-fal 1553  df-ex 1780  df-sb 2066  df-clab 2708  df-cleq 2721  df-clel 2803  df-ral 3045  df-rex 3054  df-rab 3397  df-v 3440  df-dif 3908  df-un 3910  df-in 3912  df-ss 3922  df-nul 4287  df-if 4479  df-sn 4580  df-pr 4582  df-op 4586  df-br 5096  df-opab 5158  df-xp 5629  df-rel 5630  df-cnv 5631  df-co 5632  df-dm 5633  df-res 5635  df-fun 6488  df-fn 6489

This theorem is referenced by:  fnssresd  6610  fnresin1  6611  fnresin2  6612  fnresi  6615  fssres  6694  fvreseq0  6976  fnreseql  6986  ffvresb  7063  fnressn  7096  soisores  7268  oprres  7521  ofres  7636  fsplitfpar  8058  fnsuppres  8131  tfrlem1  8305  tz7.48lem  8370  tz7.49c  8375  resixp  8867  ixpfi2  9259  ttrclss  9635  dfac12lem1  10057  ackbij2lem3  10153  cfsmolem  10183  alephsing  10189  ttukeylem3  10424  iunfo  10452  fpwwe2lem7  10550  mulnzcnf  11784  seqfeq2  13950  seqf1olem2  13967  bpolylem  15973  reeff1  16047  sscres  17748  fullsubc  17775  fullresc  17776  funcres2c  17828  dmaf  17974  cdaf  17975  frmdplusg  18746  frmdss2  18755  gass  19198  dprdfadd  19919  rngmgpf  20060  mgpf  20151  prdscrngd  20225  rnghmresfn  20522  rnghmsscmap2  20532  rnghmsscmap  20533  rhmresfn  20551  rhmsscmap2  20561  rhmsscmap  20562  subrgascl  21989  upxp  23526  uptx  23528  cnmpt1st  23571  cnmpt2nd  23572  cnextfres1  23971  prdstmdd  24027  ressprdsds  24275  prdsxmslem2  24433  xrsdsre  24715  recosf1o  26460  resinf1o  26461  mpodvdsmulf1o  27120  dvdsmulf1o  27122  ex-fpar  30424  sspg  30690  ssps  30692  sspmlem  30694  sspn  30698  hhssnv  31226  ressupprn  32646  1stpreimas  32662  cnre2csqlem  33879  raddcn  33898  carsggect  34288  subiwrdlen  34356  signsvtn0  34540  signstres  34545  bnj1253  34986  bnj1280  34989  gblacfnacd  35077  subfacp1lem5  35159  cvmlift2lem9a  35278  filnetlem4  36357  finixpnum  37587  poimirlem4  37606  poimirlem8  37610  ftc1anclem3  37677  isdrngo2  37940  diaintclN  41040  dibintclN  41149  dihintcl  41326  imaiinfv  42669  fnwe2lem2  43027  aomclem6  43035  deg1mhm  43176  limsupvaluz2  45723  supcnvlimsup  45725  limsupgtlem  45762  resincncf  45860  icccncfext  45872  fourierdlem42  46134  fourierdlem73  46164  fdivmpt  48529  slotresfo  48887  basresposfo  48966  oppff1  49137