Theorem fnssres 6662

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

This proof depends on syntax axioms:   → wi 4   ∧ wa 401   ⊆ wss 3895   ↾ cres 5652   Fn wfn 6533

This proof depends on axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1827  ax-4 1841  ax-5 1942  ax-6 1999  ax-7 2040  ax-8 2146  ax-9 2154  ax-ext 2732  ax-sep 5248  ax-pr 5390

This proof depends on definitions:  df-bi 210  df-an 402  df-or 862  df-3an 1105  df-tru 1572  df-fal 1582  df-ex 1812  df-sb 2099  df-clab 2739  df-cleq 2752  df-clel 2835  df-ral 3077  df-rex 3087  df-rab 3413  df-v 3452  df-ss 3896  df-dif 4047  df-in 4091  df-un 4151  df-nul 4279  df-if 4482  df-sn 4585  df-pr 4587  df-op 4835  df-br 5103  df-opab 5167  df-xp 5656  df-rel 5657  df-cnv 5658  df-co 5659  df-dm 5660  df-res 5662  df-fun 6540  df-fn 6541

This theorem is used by:  fnssresd  6663  fnresin1  6664  fnresin2  6665  fnresi  6668  fssres  6748  fvreseq0  7037  fnreseql  7047  ffvresb  7126  fnressn  7162  soisores  7335  oprres  7588  ofres  7712  fsplitfpar  8131  fnsuppres  8211  tfrlem1  8386  tz7.48lemOLD  8454  tz7.49c  8459  resixp  8964  ixpfi2  9342  ttrclss  9724  dfac12lem1  10225  ackbij2lem3  10321  cfsmolem  10351  alephsing  10357  ttukeylem3  10592  iunfo  10626  fpwwe2lem7  10725  mulnzcnf  11965  seqfeq2  14171  seqf1olem2  14188  bpolylem  16219  reeff1  16293  sscres  18003  fullsubc  18030  fullresc  18031  funcres2c  18083  dmaf  18229  cdaf  18230  frmdplusg  19055  frmdss2  19064  gass  19520  dprdfadd  20241  rngmgpf  20384  mgpf  20480  prdscrngd  20556  rnghmresfn  20876  rnghmsscmap2  20886  rnghmsscmap  20887  rhmresfn  20905  rhmsscmap2  20915  rhmsscmap  20916  subrgascl  22380  upxp  23947  uptx  23949  cnmpt1st  23992  cnmpt2nd  23993  cnextfres1  24392  prdstmdd  24448  ressprdsds  24695  prdsxmslem2  24853  xrsdsre  25135  recosf1o  26868  resinf1o  26869  mpodvdsmulf1o  27526  dvdsmulf1o  27528  ex-fpar  31068  sspg  31335  ssps  31337  sspmlem  31339  sspn  31343  hhssnv  31871  ressupprn  33330  1stpreimas  33346  cnre2csqlem  34588  raddcn  34607  carsggect  34996  subiwrdlen  35064  signsvtn0  35245  signstres  35250  bnj1253  35693  bnj1280  35696  gblacfnacd  35948  subfacp1lem5  36035  cvmlift2lem9a  36154  filnetlem4  37261  finixpnum  38621  poimirlem4  38635  poimirlem8  38639  ftc1anclem3  38706  isdrngo2  38985  diaintclN  42208  dibintclN  42317  dihintcl  42494  imaiinfv  43797  aomclem6  44154  deg1mhm  44295  limsupvaluz2  46841  supcnvlimsup  46843  limsupgtlem  46880  resincncf  46978  icccncfext  46990  fourierdlem42  47252  fourierdlem73  47282  fdivmpt  49745  slotresfo  50106  basresposfo  50185  oppff1  50357