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 477	1 ⊢ ((𝐹 Fn 𝐴 ∧ 𝐵 ⊆ 𝐴) → (𝐹 ↾ 𝐵) Fn 𝐵)

Syntax hints:   → wi 4   ∧ wa 395   ⊆ 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 1796  ax-4 1810  ax-5 1912  ax-6 1970  ax-7 2010  ax-8 2107  ax-9 2115  ax-ext 2702  ax-sep 5299  ax-nul 5306  ax-pr 5427

This theorem depends on definitions:  df-bi 206  df-an 396  df-or 845  df-3an 1088  df-tru 1543  df-fal 1553  df-ex 1781  df-sb 2067  df-clab 2709  df-cleq 2723  df-clel 2809  df-ral 3061  df-rex 3070  df-rab 3432  df-v 3475  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  7327  oprres  7579  ofres  7693  fsplitfpar  8109  fnsuppres  8181  tfrlem1  8382  tz7.48lem  8447  tz7.49c  8452  resixp  8933  ixpfi2  9356  ttrclss  9721  dfac12lem1  10144  ackbij2lem3  10242  cfsmolem  10271  alephsing  10277  ttukeylem3  10512  iunfo  10540  fpwwe2lem7  10638  mulnzcnf  11867  seqfeq2  13998  seqf1olem2  14015  bpolylem  15999  reeff1  16070  sscres  17777  fullsubc  17807  fullresc  17808  funcres2c  17861  dmaf  18009  cdaf  18010  frmdplusg  18777  frmdss2  18786  gass  19213  dprdfadd  19938  rngmgpf  20058  mgpf  20149  prdscrngd  20217  rnghmresfn  20511  rnghmsscmap2  20521  rnghmsscmap  20522  rhmresfn  20540  rhmsscmap2  20550  rhmsscmap  20551  subrgascl  21938  upxp  23447  uptx  23449  cnmpt1st  23492  cnmpt2nd  23493  cnextfres1  23892  prdstmdd  23948  ressprdsds  24197  prdsxmslem2  24358  xrsdsre  24646  itg1addlem4OLD  25549  recosf1o  26384  resinf1o  26385  mpodvdsmulf1o  27040  dvdsmulf1o  27042  ex-fpar  30149  sspg  30415  ssps  30417  sspmlem  30419  sspn  30423  hhssnv  30951  ressupprn  32346  1stpreimas  32361  cnre2csqlem  33355  raddcn  33374  carsggect  33782  subiwrdlen  33850  signsvtn0  34046  signstres  34051  bnj1253  34493  bnj1280  34496  subfacp1lem5  34640  cvmlift2lem9a  34759  filnetlem4  35732  finixpnum  36939  poimirlem4  36958  poimirlem8  36962  ftc1anclem3  37029  isdrngo2  37292  diaintclN  40395  dibintclN  40504  dihintcl  40681  imaiinfv  41896  fnwe2lem2  42258  aomclem6  42266  deg1mhm  42414  limsupvaluz2  44915  supcnvlimsup  44917  limsupgtlem  44954  resincncf  45052  icccncfext  45064  dvnprodlem1  45123  fourierdlem42  45326  fourierdlem73  45356  fdivmpt  47390