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 478	1 ⊢ ((𝐹 Fn 𝐴 ∧ 𝐵 ⊆ 𝐴) → (𝐹 ↾ 𝐵) Fn 𝐵)

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

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1802  ax-4 1816  ax-5 1917  ax-6 1974  ax-7 2015  ax-8 2121  ax-9 2129  ax-ext 2712  ax-sep 5225  ax-pr 5369

This theorem depends on definitions:  df-bi 208  df-an 397  df-or 854  df-3an 1094  df-tru 1550  df-fal 1560  df-ex 1787  df-sb 2074  df-clab 2719  df-cleq 2732  df-clel 2815  df-ral 3055  df-rex 3065  df-rab 3393  df-v 3434  df-dif 3893  df-un 3895  df-in 3897  df-ss 3907  df-nul 4269  df-if 4462  df-sn 4563  df-pr 4565  df-op 4569  df-br 5080  df-opab 5142  df-xp 5631  df-rel 5632  df-cnv 5633  df-co 5634  df-dm 5635  df-res 5637  df-fun 6494  df-fn 6495

This theorem is referenced by:  fnssresd  6616  fnresin1  6617  fnresin2  6618  fnresi  6621  fssres  6700  fvreseq0  6986  fnreseql  6996  ffvresb  7074  fnressn  7108  soisores  7278  oprres  7531  ofres  7646  fsplitfpar  8064  fnsuppres  8138  tfrlem1  8312  tz7.48lem  8377  tz7.49c  8382  resixp  8878  ixpfi2  9257  ttrclss  9639  dfac12lem1  10064  ackbij2lem3  10160  cfsmolem  10190  alephsing  10196  ttukeylem3  10431  iunfo  10459  fpwwe2lem7  10558  mulnzcnf  11794  seqfeq2  13985  seqf1olem2  14002  bpolylem  16011  reeff1  16085  sscres  17788  fullsubc  17815  fullresc  17816  funcres2c  17868  dmaf  18014  cdaf  18015  frmdplusg  18820  frmdss2  18829  gass  19274  dprdfadd  19995  rngmgpf  20136  mgpf  20227  prdscrngd  20299  rnghmresfn  20598  rnghmsscmap2  20608  rnghmsscmap  20609  rhmresfn  20627  rhmsscmap2  20637  rhmsscmap  20638  subrgascl  22049  upxp  23613  uptx  23615  cnmpt1st  23658  cnmpt2nd  23659  cnextfres1  24058  prdstmdd  24114  ressprdsds  24361  prdsxmslem2  24519  xrsdsre  24801  recosf1o  26524  resinf1o  26525  mpodvdsmulf1o  27182  dvdsmulf1o  27184  ex-fpar  30557  sspg  30824  ssps  30826  sspmlem  30828  sspn  30832  hhssnv  31360  ressupprn  32789  1stpreimas  32805  cnre2csqlem  34101  raddcn  34120  carsggect  34509  subiwrdlen  34577  signsvtn0  34761  signstres  34766  bnj1253  35206  bnj1280  35209  gblacfnacd  35337  subfacp1lem5  35419  cvmlift2lem9a  35538  filnetlem4  36616  finixpnum  37979  poimirlem4  37998  poimirlem8  38002  ftc1anclem3  38069  isdrngo2  38332  diaintclN  41557  dibintclN  41666  dihintcl  41843  imaiinfv  43149  fnwe2lem2  43503  aomclem6  43511  deg1mhm  43652  limsupvaluz2  46188  supcnvlimsup  46190  limsupgtlem  46227  resincncf  46325  icccncfext  46337  fourierdlem42  46599  fourierdlem73  46629  fdivmpt  49038  slotresfo  49396  basresposfo  49475  oppff1  49645