Theorem fnssres 6238

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

Syntax hints:   → wi 4   ∧ wa 386   ⊆ wss 3799   ↾ cres 5345   Fn wfn 6119

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1896  ax-4 1910  ax-5 2011  ax-6 2077  ax-7 2114  ax-9 2175  ax-10 2194  ax-11 2209  ax-12 2222  ax-13 2391  ax-ext 2804  ax-sep 5006  ax-nul 5014  ax-pr 5128

This theorem depends on definitions:  df-bi 199  df-an 387  df-or 881  df-3an 1115  df-tru 1662  df-ex 1881  df-nf 1885  df-sb 2070  df-clab 2813  df-cleq 2819  df-clel 2822  df-nfc 2959  df-ral 3123  df-rex 3124  df-rab 3127  df-v 3417  df-dif 3802  df-un 3804  df-in 3806  df-ss 3813  df-nul 4146  df-if 4308  df-sn 4399  df-pr 4401  df-op 4405  df-br 4875  df-opab 4937  df-xp 5349  df-rel 5350  df-cnv 5351  df-co 5352  df-dm 5353  df-res 5355  df-fun 6126  df-fn 6127

This theorem is referenced by:  fnresin1  6239  fnresin2  6240  fssres  6308  fvreseq0  6567  fnreseql  6577  ffvresb  6644  fnressn  6677  soisores  6833  oprres  7063  ofres  7174  fnsuppres  7588  tfrlem1  7739  tz7.48lem  7803  tz7.49c  7808  resixp  8211  ixpfi2  8534  dfac12lem1  9281  ackbij2lem3  9379  cfsmolem  9408  alephsing  9414  ttukeylem3  9649  iunfo  9677  fpwwe2lem8  9775  mulnzcnopr  10999  seqfeq2  13119  seqf1olem2  13136  swrd0lenOLD  13709  swrdccat1OLD  13748  pfxccat1  13782  bpolylem  15152  reeff1  15223  sscres  16836  fullsubc  16863  fullresc  16864  funcres2c  16914  dmaf  17052  cdaf  17053  frmdplusg  17746  frmdss2  17755  gass  18085  dprdfadd  18774  mgpf  18914  prdscrngd  18968  subrgascl  19859  mdetrsca  20778  upxp  21798  uptx  21800  cnmpt1st  21843  cnmpt2nd  21844  cnextfres1  22243  prdstmdd  22298  ressprdsds  22547  prdsxmslem2  22705  xrsdsre  22984  itg1addlem4  23866  recosf1o  24682  resinf1o  24683  dvdsmulf1o  25334  wlkresOLD  26972  sspg  28139  ssps  28141  sspmlem  28143  sspn  28147  hhssnv  28677  1stpreimas  30032  cnre2csqlem  30502  rmulccn  30520  raddcn  30521  carsggect  30926  subiwrdlen  30994  signsvtn0  31195  signsvtn0OLD  31196  signstres  31201  bnj1253  31632  bnj1280  31635  subfacp1lem3  31711  subfacp1lem5  31713  cvmlift2lem9a  31832  filnetlem4  32915  finixpnum  33938  poimirlem4  33958  poimirlem8  33962  ftc1anclem3  34031  isdrngo2  34300  diaintclN  37134  dibintclN  37243  dihintcl  37420  imaiinfv  38101  fnwe2lem2  38465  aomclem6  38473  deg1mhm  38629  fnssresd  40283  limsupvaluz2  40766  supcnvlimsup  40768  limsupgtlem  40805  resincncf  40884  icccncfext  40896  dvnprodlem1  40957  fourierdlem42  41161  fourierdlem73  41191  rnghmresfn  42811  rnghmsscmap2  42821  rnghmsscmap  42822  rhmresfn  42857  rhmsscmap2  42867  rhmsscmap  42868  fdivmpt  43182