Theorem fnssres 6665

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

This proof depends on syntax axioms:   → wi 4   ∧ wa 401   ⊆ wss 3908   ↾ cres 5668   Fn wfn 6538

This proof depends on axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1828  ax-4 1842  ax-5 1943  ax-6 2000  ax-7 2041  ax-8 2148  ax-9 2156  ax-ext 2738  ax-sep 5262  ax-pr 5409

This proof depends on definitions:  df-bi 210  df-an 402  df-or 862  df-3an 1105  df-tru 1573  df-fal 1583  df-ex 1813  df-sb 2100  df-clab 2745  df-cleq 2758  df-clel 2841  df-ral 3083  df-rex 3093  df-rab 3420  df-v 3460  df-dif 3911  df-un 3913  df-in 3915  df-ss 3925  df-nul 4290  df-if 4493  df-sn 4595  df-pr 4597  df-op 4601  df-br 5115  df-opab 5179  df-xp 5672  df-rel 5673  df-cnv 5674  df-co 5675  df-dm 5676  df-res 5678  df-fun 6545  df-fn 6546

This theorem is used by:  fnssresd  6666  fnresin1  6667  fnresin2  6668  fnresi  6671  fssres  6751  fvreseq0  7040  fnreseql  7050  ffvresb  7128  fnressn  7162  soisores  7336  oprres  7591  ofres  7706  fsplitfpar  8122  fnsuppres  8196  tfrlem1  8371  tz7.48lem  8437  tz7.49c  8442  resixp  8940  ixpfi2  9317  ttrclss  9699  dfac12lem1  10146  ackbij2lem3  10242  cfsmolem  10272  alephsing  10278  ttukeylem3  10513  iunfo  10541  fpwwe2lem7  10640  mulnzcnf  11878  seqfeq2  14081  seqf1olem2  14098  bpolylem  16127  reeff1  16201  sscres  17905  fullsubc  17932  fullresc  17933  funcres2c  17985  dmaf  18131  cdaf  18132  frmdplusg  18944  frmdss2  18953  gass  19402  dprdfadd  20123  rngmgpf  20266  mgpf  20361  prdscrngd  20436  rnghmresfn  20755  rnghmsscmap2  20765  rnghmsscmap  20766  rhmresfn  20784  rhmsscmap2  20794  rhmsscmap  20795  subrgascl  22254  upxp  23817  uptx  23819  cnmpt1st  23862  cnmpt2nd  23863  cnextfres1  24262  prdstmdd  24318  ressprdsds  24565  prdsxmslem2  24723  xrsdsre  25005  recosf1o  26737  resinf1o  26738  mpodvdsmulf1o  27395  dvdsmulf1o  27397  ex-fpar  30850  sspg  31117  ssps  31119  sspmlem  31121  sspn  31125  hhssnv  31653  ressupprn  33072  1stpreimas  33088  cnre2csqlem  34331  raddcn  34350  carsggect  34740  subiwrdlen  34808  signsvtn0  34989  signstres  34994  bnj1253  35437  bnj1280  35440  gblacfnacd  35610  subfacp1lem5  35697  cvmlift2lem9a  35816  filnetlem4  36933  finixpnum  38297  poimirlem4  38316  poimirlem8  38320  ftc1anclem3  38387  isdrngo2  38650  diaintclN  41873  dibintclN  41982  dihintcl  42159  imaiinfv  43465  fnwe2lem2  43819  aomclem6  43827  deg1mhm  43968  limsupvaluz2  46493  supcnvlimsup  46495  limsupgtlem  46532  resincncf  46630  icccncfext  46642  fourierdlem42  46904  fourierdlem73  46934  fdivmpt  49361  slotresfo  49718  basresposfo  49797  oppff1  49967