Theorem fnssres 6609

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

Syntax hints:   → wi 4   ∧ wa 395   ⊆ wss 3898   ↾ cres 5621   Fn wfn 6481

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 2705  ax-sep 5236  ax-nul 5246  ax-pr 5372

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 2712  df-cleq 2725  df-clel 2808  df-ral 3049  df-rex 3058  df-rab 3397  df-v 3439  df-dif 3901  df-un 3903  df-in 3905  df-ss 3915  df-nul 4283  df-if 4475  df-sn 4576  df-pr 4578  df-op 4582  df-br 5094  df-opab 5156  df-xp 5625  df-rel 5626  df-cnv 5627  df-co 5628  df-dm 5629  df-res 5631  df-fun 6488  df-fn 6489

This theorem is referenced by:  fnssresd  6610  fnresin1  6611  fnresin2  6612  fnresi  6615  fssres  6694  fvreseq0  6977  fnreseql  6987  ffvresb  7064  fnressn  7097  soisores  7267  oprres  7520  ofres  7635  fsplitfpar  8054  fnsuppres  8127  tfrlem1  8301  tz7.48lem  8366  tz7.49c  8371  resixp  8863  ixpfi2  9241  ttrclss  9617  dfac12lem1  10042  ackbij2lem3  10138  cfsmolem  10168  alephsing  10174  ttukeylem3  10409  iunfo  10437  fpwwe2lem7  10535  mulnzcnf  11770  seqfeq2  13934  seqf1olem2  13951  bpolylem  15957  reeff1  16031  sscres  17732  fullsubc  17759  fullresc  17760  funcres2c  17812  dmaf  17958  cdaf  17959  frmdplusg  18764  frmdss2  18773  gass  19215  dprdfadd  19936  rngmgpf  20077  mgpf  20168  prdscrngd  20242  rnghmresfn  20536  rnghmsscmap2  20546  rnghmsscmap  20547  rhmresfn  20565  rhmsscmap2  20575  rhmsscmap  20576  subrgascl  22002  upxp  23539  uptx  23541  cnmpt1st  23584  cnmpt2nd  23585  cnextfres1  23984  prdstmdd  24040  ressprdsds  24287  prdsxmslem2  24445  xrsdsre  24727  recosf1o  26472  resinf1o  26473  mpodvdsmulf1o  27132  dvdsmulf1o  27134  ex-fpar  30444  sspg  30710  ssps  30712  sspmlem  30714  sspn  30718  hhssnv  31246  ressupprn  32675  1stpreimas  32691  cnre2csqlem  33944  raddcn  33963  carsggect  34352  subiwrdlen  34420  signsvtn0  34604  signstres  34609  bnj1253  35050  bnj1280  35053  gblacfnacd  35167  subfacp1lem5  35249  cvmlift2lem9a  35368  filnetlem4  36446  finixpnum  37666  poimirlem4  37685  poimirlem8  37689  ftc1anclem3  37756  isdrngo2  38019  diaintclN  41178  dibintclN  41287  dihintcl  41464  imaiinfv  42811  fnwe2lem2  43169  aomclem6  43177  deg1mhm  43318  limsupvaluz2  45861  supcnvlimsup  45863  limsupgtlem  45900  resincncf  45998  icccncfext  46010  fourierdlem42  46272  fourierdlem73  46302  fdivmpt  48666  slotresfo  49024  basresposfo  49103  oppff1  49274