Theorem fnssres 6622

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

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

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 2709  ax-sep 5232  ax-pr 5376

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 2716  df-cleq 2729  df-clel 2812  df-ral 3053  df-rex 3063  df-rab 3391  df-v 3432  df-dif 3893  df-un 3895  df-in 3897  df-ss 3907  df-nul 4275  df-if 4468  df-sn 4569  df-pr 4571  df-op 4575  df-br 5087  df-opab 5149  df-xp 5637  df-rel 5638  df-cnv 5639  df-co 5640  df-dm 5641  df-res 5643  df-fun 6501  df-fn 6502

This theorem is referenced by:  fnssresd  6623  fnresin1  6624  fnresin2  6625  fnresi  6628  fssres  6707  fvreseq0  6991  fnreseql  7001  ffvresb  7079  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  49010  slotresfo  49368  basresposfo  49447  oppff1  49617