Theorem fnssres 6621

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

Syntax hints:   → wi 4   ∧ wa 395   ⊆ wss 3889   ↾ cres 5633   Fn wfn 6493

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1797  ax-4 1811  ax-5 1912  ax-6 1969  ax-7 2010  ax-8 2116  ax-9 2124  ax-ext 2708  ax-sep 5231  ax-pr 5375

This theorem depends on definitions:  df-bi 207  df-an 396  df-or 849  df-3an 1089  df-tru 1545  df-fal 1555  df-ex 1782  df-sb 2069  df-clab 2715  df-cleq 2728  df-clel 2811  df-ral 3052  df-rex 3062  df-rab 3390  df-v 3431  df-dif 3892  df-un 3894  df-in 3896  df-ss 3906  df-nul 4274  df-if 4467  df-sn 4568  df-pr 4570  df-op 4574  df-br 5086  df-opab 5148  df-xp 5637  df-rel 5638  df-cnv 5639  df-co 5640  df-dm 5641  df-res 5643  df-fun 6500  df-fn 6501

This theorem is referenced by:  fnssresd  6622  fnresin1  6623  fnresin2  6624  fnresi  6627  fssres  6706  fvreseq0  6990  fnreseql  7000  ffvresb  7078  fnressn  7112  soisores  7282  oprres  7535  ofres  7650  fsplitfpar  8068  fnsuppres  8141  tfrlem1  8315  tz7.48lem  8380  tz7.49c  8385  resixp  8881  ixpfi2  9260  ttrclss  9641  dfac12lem1  10066  ackbij2lem3  10162  cfsmolem  10192  alephsing  10198  ttukeylem3  10433  iunfo  10461  fpwwe2lem7  10560  mulnzcnf  11796  seqfeq2  13987  seqf1olem2  14004  bpolylem  16013  reeff1  16087  sscres  17790  fullsubc  17817  fullresc  17818  funcres2c  17870  dmaf  18016  cdaf  18017  frmdplusg  18822  frmdss2  18831  gass  19276  dprdfadd  19997  rngmgpf  20138  mgpf  20229  prdscrngd  20301  rnghmresfn  20596  rnghmsscmap2  20606  rnghmsscmap  20607  rhmresfn  20625  rhmsscmap2  20635  rhmsscmap  20636  subrgascl  22044  upxp  23588  uptx  23590  cnmpt1st  23633  cnmpt2nd  23634  cnextfres1  24033  prdstmdd  24089  ressprdsds  24336  prdsxmslem2  24494  xrsdsre  24776  recosf1o  26499  resinf1o  26500  mpodvdsmulf1o  27157  dvdsmulf1o  27159  ex-fpar  30532  sspg  30799  ssps  30801  sspmlem  30803  sspn  30807  hhssnv  31335  ressupprn  32763  1stpreimas  32779  cnre2csqlem  34054  raddcn  34073  carsggect  34462  subiwrdlen  34530  signsvtn0  34714  signstres  34719  bnj1253  35159  bnj1280  35162  gblacfnacd  35284  subfacp1lem5  35366  cvmlift2lem9a  35485  filnetlem4  36563  finixpnum  37926  poimirlem4  37945  poimirlem8  37949  ftc1anclem3  38016  isdrngo2  38279  diaintclN  41504  dibintclN  41613  dihintcl  41790  imaiinfv  43125  fnwe2lem2  43479  aomclem6  43487  deg1mhm  43628  limsupvaluz2  46166  supcnvlimsup  46168  limsupgtlem  46205  resincncf  46303  icccncfext  46315  fourierdlem42  46577  fourierdlem73  46607  fdivmpt  49016  slotresfo  49374  basresposfo  49453  oppff1  49623