Theorem fnssres 6442

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

Syntax hints:   → wi 4   ∧ wa 399   ⊆ wss 3881   ↾ cres 5521   Fn wfn 6319

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 1911  ax-6 1970  ax-7 2015  ax-8 2113  ax-9 2121  ax-10 2142  ax-11 2158  ax-12 2175  ax-ext 2770  ax-sep 5167  ax-nul 5174  ax-pr 5295

This theorem depends on definitions:  df-bi 210  df-an 400  df-or 845  df-3an 1086  df-tru 1541  df-ex 1782  df-nf 1786  df-sb 2070  df-clab 2777  df-cleq 2791  df-clel 2870  df-nfc 2938  df-ral 3111  df-rex 3112  df-v 3443  df-dif 3884  df-un 3886  df-in 3888  df-ss 3898  df-nul 4244  df-if 4426  df-sn 4526  df-pr 4528  df-op 4532  df-br 5031  df-opab 5093  df-xp 5525  df-rel 5526  df-cnv 5527  df-co 5528  df-dm 5529  df-res 5531  df-fun 6326  df-fn 6327

This theorem is referenced by:  fnssresd  6443  fnresin1  6444  fnresin2  6445  fnresi  6448  fssres  6518  fvreseq0  6785  fnreseql  6795  ffvresb  6865  fnressn  6897  soisores  7059  oprres  7296  ofres  7405  fsplitfpar  7797  fnsuppres  7840  tfrlem1  7995  tz7.48lem  8060  tz7.49c  8065  resixp  8480  ixpfi2  8806  dfac12lem1  9554  ackbij2lem3  9652  cfsmolem  9681  alephsing  9687  ttukeylem3  9922  iunfo  9950  fpwwe2lem8  10048  mulnzcnopr  11275  seqfeq2  13389  seqf1olem2  13406  bpolylem  15394  reeff1  15465  sscres  17085  fullsubc  17112  fullresc  17113  funcres2c  17163  dmaf  17301  cdaf  17302  frmdplusg  18011  frmdss2  18020  gass  18423  dprdfadd  19135  mgpf  19305  prdscrngd  19359  subrgascl  20737  mdetrsca  21208  upxp  22228  uptx  22230  cnmpt1st  22273  cnmpt2nd  22274  cnextfres1  22673  prdstmdd  22729  ressprdsds  22978  prdsxmslem2  23136  xrsdsre  23415  itg1addlem4  24303  recosf1o  25127  resinf1o  25128  dvdsmulf1o  25779  ex-fpar  28247  sspg  28511  ssps  28513  sspmlem  28515  sspn  28519  hhssnv  29047  ressupprn  30450  1stpreimas  30465  dimkerim  31111  cnre2csqlem  31263  rmulccn  31281  raddcn  31282  carsggect  31686  subiwrdlen  31754  signsvtn0  31950  signstres  31955  bnj1253  32399  bnj1280  32402  subfacp1lem3  32542  subfacp1lem5  32544  cvmlift2lem9a  32663  filnetlem4  33842  finixpnum  35042  poimirlem4  35061  poimirlem8  35065  ftc1anclem3  35132  isdrngo2  35396  diaintclN  38354  dibintclN  38463  dihintcl  38640  imaiinfv  39634  fnwe2lem2  39995  aomclem6  40003  deg1mhm  40151  limsupvaluz2  42380  supcnvlimsup  42382  limsupgtlem  42419  resincncf  42517  icccncfext  42529  dvnprodlem1  42588  fourierdlem42  42791  fourierdlem73  42821  rnghmresfn  44587  rnghmsscmap2  44597  rnghmsscmap  44598  rhmresfn  44633  rhmsscmap2  44643  rhmsscmap  44644  fdivmpt  44954