Theorem fnssres 6004

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

Syntax hints:   → wi 4   ∧ wa 384   ⊆ wss 3574   ↾ cres 5116   Fn wfn 5883

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1722  ax-4 1737  ax-5 1839  ax-6 1888  ax-7 1935  ax-9 1999  ax-10 2019  ax-11 2034  ax-12 2047  ax-13 2246  ax-ext 2602  ax-sep 4781  ax-nul 4789  ax-pr 4906

This theorem depends on definitions:  df-bi 197  df-or 385  df-an 386  df-3an 1039  df-tru 1486  df-ex 1705  df-nf 1710  df-sb 1881  df-clab 2609  df-cleq 2615  df-clel 2618  df-nfc 2753  df-ral 2917  df-rex 2918  df-rab 2921  df-v 3202  df-dif 3577  df-un 3579  df-in 3581  df-ss 3588  df-nul 3916  df-if 4087  df-sn 4178  df-pr 4180  df-op 4184  df-br 4654  df-opab 4713  df-xp 5120  df-rel 5121  df-cnv 5122  df-co 5123  df-dm 5124  df-res 5126  df-fun 5890  df-fn 5891

This theorem is referenced by:  fnresin1  6005  fnresin2  6006  fssres  6070  fvreseq0  6317  fnreseql  6327  ffvresb  6394  fnressn  6425  soisores  6577  oprres  6802  ofres  6913  fnsuppres  7322  tfrlem1  7472  tz7.48lem  7536  tz7.49c  7541  resixp  7943  ixpfi2  8264  dfac12lem1  8965  ackbij2lem3  9063  cfsmolem  9092  alephsing  9098  ttukeylem3  9333  iunfo  9361  fpwwe2lem8  9459  mulnzcnopr  10673  seqfeq2  12824  seqf1olem2  12841  swrd0len  13422  swrdccat1  13457  bpolylem  14779  reeff1  14850  eucalg  15300  sscres  16483  fullsubc  16510  fullresc  16511  funcres2c  16561  dmaf  16699  cdaf  16700  frmdplusg  17391  frmdss2  17400  gass  17734  dprdfadd  18419  mgpf  18559  prdscrngd  18613  subrgascl  19498  mdetrsca  20409  upxp  21426  uptx  21428  cnmpt1st  21471  cnmpt2nd  21472  cnextfres1  21872  prdstmdd  21927  ressprdsds  22176  prdsxmslem2  22334  xrsdsre  22613  itg1addlem4  23466  recosf1o  24281  resinf1o  24282  dvdsmulf1o  24920  wlkres  26567  sspg  27583  ssps  27585  sspmlem  27587  sspn  27591  hhssnv  28121  1stpreimas  29483  cnre2csqlem  29956  rmulccn  29974  raddcn  29975  carsggect  30380  subiwrdlen  30448  signsvtn0  30647  signstres  30652  bnj1253  31085  bnj1280  31088  subfacp1lem3  31164  subfacp1lem5  31166  cvmlift2lem9a  31285  filnetlem4  32376  finixpnum  33394  poimirlem4  33413  poimirlem8  33417  ftc1anclem3  33487  isdrngo2  33757  diaintclN  36347  dibintclN  36456  dihintcl  36633  imaiinfv  37256  fnwe2lem2  37621  aomclem6  37629  deg1mhm  37785  fnssresd  39482  limsupvaluz2  39970  supcnvlimsup  39972  limsupgtlem  40009  resincncf  40088  icccncfext  40100  dvnprodlem1  40161  fourierdlem42  40366  fourierdlem73  40396  pfxccat1  41410  rnghmresfn  41963  rnghmsscmap2  41973  rnghmsscmap  41974  rhmresfn  42009  rhmsscmap2  42019  rhmsscmap  42020  fdivmpt  42334