Theorem fnssres 6648

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

Syntax hints:   → wi 4   ∧ wa 400   ⊆ wss 3907   ↾ cres 5653   Fn wfn 6520

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1818  ax-4 1832  ax-5 1933  ax-6 1990  ax-7 2031  ax-8 2147  ax-9 2155  ax-ext 2737  ax-sep 5250  ax-pr 5394

This theorem depends on definitions:  df-bi 210  df-an 401  df-or 861  df-3an 1103  df-tru 1566  df-fal 1576  df-ex 1803  df-sb 2094  df-clab 2744  df-cleq 2757  df-clel 2840  df-ral 3080  df-rex 3090  df-rab 3418  df-v 3459  df-dif 3910  df-un 3912  df-in 3914  df-ss 3924  df-nul 4289  df-if 4484  df-sn 4586  df-pr 4588  df-op 4592  df-br 5105  df-opab 5167  df-xp 5657  df-rel 5658  df-cnv 5659  df-co 5660  df-dm 5661  df-res 5663  df-fun 6527  df-fn 6528

This theorem is referenced by:  fnssresd  6649  fnresin1  6650  fnresin2  6651  fnresi  6654  fssres  6734  fvreseq0  7023  fnreseql  7033  ffvresb  7111  fnressn  7145  soisores  7315  oprres  7568  ofres  7683  fsplitfpar  8101  fnsuppres  8175  tfrlem1  8350  tz7.48lem  8416  tz7.49c  8421  resixp  8919  ixpfi2  9295  ttrclss  9677  dfac12lem1  10115  ackbij2lem3  10211  cfsmolem  10242  alephsing  10248  ttukeylem3  10483  iunfo  10511  fpwwe2lem7  10610  mulnzcnf  11848  seqfeq2  14049  seqf1olem2  14066  bpolylem  16090  reeff1  16164  sscres  17868  fullsubc  17895  fullresc  17896  funcres2c  17948  dmaf  18094  cdaf  18095  frmdplusg  18901  frmdss2  18910  gass  19359  dprdfadd  20080  rngmgpf  20223  mgpf  20318  prdscrngd  20391  rnghmresfn  20692  rnghmsscmap2  20702  rnghmsscmap  20703  rhmresfn  20721  rhmsscmap2  20731  rhmsscmap  20732  subrgascl  22174  upxp  23737  uptx  23739  cnmpt1st  23782  cnmpt2nd  23783  cnextfres1  24182  prdstmdd  24238  ressprdsds  24485  prdsxmslem2  24643  xrsdsre  24925  recosf1o  26654  resinf1o  26655  mpodvdsmulf1o  27312  dvdsmulf1o  27314  ex-fpar  30718  sspg  30985  ssps  30987  sspmlem  30989  sspn  30993  hhssnv  31521  ressupprn  32943  1stpreimas  32959  cnre2csqlem  34212  raddcn  34231  carsggect  34620  subiwrdlen  34688  signsvtn0  34869  signstres  34874  bnj1253  35317  bnj1280  35320  gblacfnacd  35452  subfacp1lem5  35542  cvmlift2lem9a  35661  filnetlem4  36749  finixpnum  38111  poimirlem4  38130  poimirlem8  38134  ftc1anclem3  38201  isdrngo2  38464  diaintclN  41689  dibintclN  41798  dihintcl  41975  imaiinfv  43281  fnwe2lem2  43635  aomclem6  43643  deg1mhm  43784  limsupvaluz2  46311  supcnvlimsup  46313  limsupgtlem  46350  resincncf  46448  icccncfext  46460  fourierdlem42  46722  fourierdlem73  46752  fdivmpt  49172  slotresfo  49529  basresposfo  49608  oppff1  49778