Theorem fnssres 6629

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

Syntax hints:   → wi 4   ∧ wa 396   ⊆ wss 3913   ↾ cres 5640   Fn wfn 6496

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 2702  ax-sep 5261  ax-nul 5268  ax-pr 5389

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 2709  df-cleq 2723  df-clel 2809  df-ral 3061  df-rex 3070  df-rab 3406  df-v 3448  df-dif 3916  df-un 3918  df-in 3920  df-ss 3930  df-nul 4288  df-if 4492  df-sn 4592  df-pr 4594  df-op 4598  df-br 5111  df-opab 5173  df-xp 5644  df-rel 5645  df-cnv 5646  df-co 5647  df-dm 5648  df-res 5650  df-fun 6503  df-fn 6504

This theorem is referenced by:  fnssresd  6630  fnresin1  6631  fnresin2  6632  fnresi  6635  fssres  6713  fvreseq0  6993  fnreseql  7003  ffvresb  7077  fnressn  7109  soisores  7277  oprres  7527  ofres  7641  fsplitfpar  8055  fnsuppres  8127  tfrlem1  8327  tz7.48lem  8392  tz7.49c  8397  resixp  8878  ixpfi2  9301  ttrclss  9665  dfac12lem1  10088  ackbij2lem3  10186  cfsmolem  10215  alephsing  10221  ttukeylem3  10456  iunfo  10484  fpwwe2lem7  10582  mulnzcnopr  11810  seqfeq2  13941  seqf1olem2  13958  bpolylem  15942  reeff1  16013  sscres  17720  fullsubc  17750  fullresc  17751  funcres2c  17802  dmaf  17949  cdaf  17950  frmdplusg  18678  frmdss2  18687  gass  19095  dprdfadd  19813  mgpf  19993  prdscrngd  20051  subrgascl  21511  mdetrsca  21989  upxp  23011  uptx  23013  cnmpt1st  23056  cnmpt2nd  23057  cnextfres1  23456  prdstmdd  23512  ressprdsds  23761  prdsxmslem2  23922  xrsdsre  24210  itg1addlem4OLD  25101  recosf1o  25928  resinf1o  25929  dvdsmulf1o  26580  ex-fpar  29469  sspg  29733  ssps  29735  sspmlem  29737  sspn  29741  hhssnv  30269  ressupprn  31672  1stpreimas  31687  dimkerim  32409  cnre2csqlem  32580  rmulccn  32598  raddcn  32599  carsggect  33007  subiwrdlen  33075  signsvtn0  33271  signstres  33276  bnj1253  33718  bnj1280  33721  subfacp1lem5  33865  cvmlift2lem9a  33984  filnetlem4  34929  finixpnum  36136  poimirlem4  36155  poimirlem8  36159  ftc1anclem3  36226  isdrngo2  36490  diaintclN  39594  dibintclN  39703  dihintcl  39880  imaiinfv  41074  fnwe2lem2  41436  aomclem6  41444  deg1mhm  41592  limsupvaluz2  44099  supcnvlimsup  44101  limsupgtlem  44138  resincncf  44236  icccncfext  44248  dvnprodlem1  44307  fourierdlem42  44510  fourierdlem73  44540  rnghmresfn  46381  rnghmsscmap2  46391  rnghmsscmap  46392  rhmresfn  46427  rhmsscmap2  46437  rhmsscmap  46438  fdivmpt  46746