Theorem fnssres 6673

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

Syntax hints:   → wi 4   ∧ wa 396   ⊆ wss 3948   ↾ cres 5678   Fn wfn 6538

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 1913  ax-6 1971  ax-7 2011  ax-8 2108  ax-9 2116  ax-ext 2703  ax-sep 5299  ax-nul 5306  ax-pr 5427

This theorem depends on definitions:  df-bi 206  df-an 397  df-or 846  df-3an 1089  df-tru 1544  df-fal 1554  df-ex 1782  df-sb 2068  df-clab 2710  df-cleq 2724  df-clel 2810  df-ral 3062  df-rex 3071  df-rab 3433  df-v 3476  df-dif 3951  df-un 3953  df-in 3955  df-ss 3965  df-nul 4323  df-if 4529  df-sn 4629  df-pr 4631  df-op 4635  df-br 5149  df-opab 5211  df-xp 5682  df-rel 5683  df-cnv 5684  df-co 5685  df-dm 5686  df-res 5688  df-fun 6545  df-fn 6546

This theorem is referenced by:  fnssresd  6674  fnresin1  6675  fnresin2  6676  fnresi  6679  fssres  6757  fvreseq0  7039  fnreseql  7049  ffvresb  7126  fnressn  7158  soisores  7326  oprres  7577  ofres  7691  fsplitfpar  8106  fnsuppres  8178  tfrlem1  8378  tz7.48lem  8443  tz7.49c  8448  resixp  8929  ixpfi2  9352  ttrclss  9717  dfac12lem1  10140  ackbij2lem3  10238  cfsmolem  10267  alephsing  10273  ttukeylem3  10508  iunfo  10536  fpwwe2lem7  10634  mulnzcnopr  11862  seqfeq2  13993  seqf1olem2  14010  bpolylem  15994  reeff1  16065  sscres  17772  fullsubc  17802  fullresc  17803  funcres2c  17854  dmaf  18001  cdaf  18002  frmdplusg  18737  frmdss2  18746  gass  19167  dprdfadd  19892  mgpf  20073  prdscrngd  20139  subrgascl  21633  upxp  23134  uptx  23136  cnmpt1st  23179  cnmpt2nd  23180  cnextfres1  23579  prdstmdd  23635  ressprdsds  23884  prdsxmslem2  24045  xrsdsre  24333  itg1addlem4OLD  25224  recosf1o  26051  resinf1o  26052  dvdsmulf1o  26705  ex-fpar  29753  sspg  30019  ssps  30021  sspmlem  30023  sspn  30027  hhssnv  30555  ressupprn  31950  1stpreimas  31965  dimkerim  32771  cnre2csqlem  32959  rmulccn  32977  raddcn  32978  carsggect  33386  subiwrdlen  33454  signsvtn0  33650  signstres  33655  bnj1253  34097  bnj1280  34100  subfacp1lem5  34244  cvmlift2lem9a  34363  filnetlem4  35352  finixpnum  36559  poimirlem4  36578  poimirlem8  36582  ftc1anclem3  36649  isdrngo2  36912  diaintclN  40015  dibintclN  40124  dihintcl  40301  imaiinfv  41513  fnwe2lem2  41875  aomclem6  41883  deg1mhm  42031  limsupvaluz2  44533  supcnvlimsup  44535  limsupgtlem  44572  resincncf  44670  icccncfext  44682  dvnprodlem1  44741  fourierdlem42  44944  fourierdlem73  44974  rngmgpf  46732  rnghmresfn  46940  rnghmsscmap2  46950  rnghmsscmap  46951  rhmresfn  46986  rhmsscmap2  46996  rhmsscmap  46997  fdivmpt  47304