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 3901   ↾ 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 1796  ax-4 1810  ax-5 1911  ax-6 1968  ax-7 2009  ax-8 2115  ax-9 2123  ax-ext 2708  ax-sep 5241  ax-nul 5251  ax-pr 5377

This theorem depends on definitions:  df-bi 207  df-an 396  df-or 848  df-3an 1088  df-tru 1544  df-fal 1554  df-ex 1781  df-sb 2068  df-clab 2715  df-cleq 2728  df-clel 2811  df-ral 3052  df-rex 3061  df-rab 3400  df-v 3442  df-dif 3904  df-un 3906  df-in 3908  df-ss 3918  df-nul 4286  df-if 4480  df-sn 4581  df-pr 4583  df-op 4587  df-br 5099  df-opab 5161  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  6983  fnreseql  6993  ffvresb  7070  fnressn  7103  soisores  7273  oprres  7526  ofres  7641  fsplitfpar  8060  fnsuppres  8133  tfrlem1  8307  tz7.48lem  8372  tz7.49c  8377  resixp  8871  ixpfi2  9250  ttrclss  9629  dfac12lem1  10054  ackbij2lem3  10150  cfsmolem  10180  alephsing  10186  ttukeylem3  10421  iunfo  10449  fpwwe2lem7  10548  mulnzcnf  11783  seqfeq2  13948  seqf1olem2  13965  bpolylem  15971  reeff1  16045  sscres  17747  fullsubc  17774  fullresc  17775  funcres2c  17827  dmaf  17973  cdaf  17974  frmdplusg  18779  frmdss2  18788  gass  19230  dprdfadd  19951  rngmgpf  20092  mgpf  20183  prdscrngd  20257  rnghmresfn  20552  rnghmsscmap2  20562  rnghmsscmap  20563  rhmresfn  20581  rhmsscmap2  20591  rhmsscmap  20592  subrgascl  22021  upxp  23567  uptx  23569  cnmpt1st  23612  cnmpt2nd  23613  cnextfres1  24012  prdstmdd  24068  ressprdsds  24315  prdsxmslem2  24473  xrsdsre  24755  recosf1o  26500  resinf1o  26501  mpodvdsmulf1o  27160  dvdsmulf1o  27162  ex-fpar  30537  sspg  30803  ssps  30805  sspmlem  30807  sspn  30811  hhssnv  31339  ressupprn  32769  1stpreimas  32785  cnre2csqlem  34067  raddcn  34086  carsggect  34475  subiwrdlen  34543  signsvtn0  34727  signstres  34732  bnj1253  35173  bnj1280  35176  gblacfnacd  35296  subfacp1lem5  35378  cvmlift2lem9a  35497  filnetlem4  36575  finixpnum  37802  poimirlem4  37821  poimirlem8  37825  ftc1anclem3  37892  isdrngo2  38155  diaintclN  41314  dibintclN  41423  dihintcl  41600  imaiinfv  42931  fnwe2lem2  43289  aomclem6  43297  deg1mhm  43438  limsupvaluz2  45978  supcnvlimsup  45980  limsupgtlem  46017  resincncf  46115  icccncfext  46127  fourierdlem42  46389  fourierdlem73  46419  fdivmpt  48782  slotresfo  49140  basresposfo  49219  oppff1  49389