Theorem fnssres 6660

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

Syntax hints:   → wi 4   ∧ wa 395   ⊆ wss 3926   ↾ cres 5656   Fn wfn 6525

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1795  ax-4 1809  ax-5 1910  ax-6 1967  ax-7 2007  ax-8 2110  ax-9 2118  ax-ext 2707  ax-sep 5266  ax-nul 5276  ax-pr 5402

This theorem depends on definitions:  df-bi 207  df-an 396  df-or 848  df-3an 1088  df-tru 1543  df-fal 1553  df-ex 1780  df-sb 2065  df-clab 2714  df-cleq 2727  df-clel 2809  df-ral 3052  df-rex 3061  df-rab 3416  df-v 3461  df-dif 3929  df-un 3931  df-in 3933  df-ss 3943  df-nul 4309  df-if 4501  df-sn 4602  df-pr 4604  df-op 4608  df-br 5120  df-opab 5182  df-xp 5660  df-rel 5661  df-cnv 5662  df-co 5663  df-dm 5664  df-res 5666  df-fun 6532  df-fn 6533

This theorem is referenced by:  fnssresd  6661  fnresin1  6662  fnresin2  6663  fnresi  6666  fssres  6743  fvreseq0  7027  fnreseql  7037  ffvresb  7114  fnressn  7147  soisores  7319  oprres  7573  ofres  7688  fsplitfpar  8115  fnsuppres  8188  tfrlem1  8388  tz7.48lem  8453  tz7.49c  8458  resixp  8945  ixpfi2  9360  ttrclss  9732  dfac12lem1  10156  ackbij2lem3  10252  cfsmolem  10282  alephsing  10288  ttukeylem3  10523  iunfo  10551  fpwwe2lem7  10649  mulnzcnf  11881  seqfeq2  14041  seqf1olem2  14058  bpolylem  16062  reeff1  16136  sscres  17834  fullsubc  17861  fullresc  17862  funcres2c  17914  dmaf  18060  cdaf  18061  frmdplusg  18830  frmdss2  18839  gass  19282  dprdfadd  20001  rngmgpf  20115  mgpf  20206  prdscrngd  20280  rnghmresfn  20577  rnghmsscmap2  20587  rnghmsscmap  20588  rhmresfn  20606  rhmsscmap2  20616  rhmsscmap  20617  subrgascl  22022  upxp  23559  uptx  23561  cnmpt1st  23604  cnmpt2nd  23605  cnextfres1  24004  prdstmdd  24060  ressprdsds  24308  prdsxmslem2  24466  xrsdsre  24748  recosf1o  26494  resinf1o  26495  mpodvdsmulf1o  27154  dvdsmulf1o  27156  ex-fpar  30389  sspg  30655  ssps  30657  sspmlem  30659  sspn  30663  hhssnv  31191  ressupprn  32613  1stpreimas  32629  cnre2csqlem  33887  raddcn  33906  carsggect  34296  subiwrdlen  34364  signsvtn0  34548  signstres  34553  bnj1253  34994  bnj1280  34997  gblacfnacd  35076  subfacp1lem5  35152  cvmlift2lem9a  35271  filnetlem4  36345  finixpnum  37575  poimirlem4  37594  poimirlem8  37598  ftc1anclem3  37665  isdrngo2  37928  diaintclN  41023  dibintclN  41132  dihintcl  41309  imaiinfv  42663  fnwe2lem2  43022  aomclem6  43030  deg1mhm  43171  limsupvaluz2  45715  supcnvlimsup  45717  limsupgtlem  45754  resincncf  45852  icccncfext  45864  fourierdlem42  46126  fourierdlem73  46156  fdivmpt  48468  slotresfo  48821  basresposfo  48900