Theorem fnssres 6687

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

This proof depends on syntax axioms:   → wi 4   ∧ wa 401   ⊆ wss 3900   ↾ cres 5658   Fn wfn 6556

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 1945  ax-6 2002  ax-7 2043  ax-8 2149  ax-9 2157  ax-ext 2735  ax-sep 5253  ax-pr 5396

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 2102  df-clab 2742  df-cleq 2755  df-clel 2839  df-ral 3081  df-rex 3091  df-rab 3417  df-v 3456  df-ss 3901  df-dif 4050  df-in 4094  df-un 4154  df-nul 4282  df-if 4486  df-sn 4589  df-pr 4591  df-op 4839  df-br 5107  df-opab 5172  df-xp 5662  df-rel 5663  df-cnv 5664  df-co 5665  df-dm 5666  df-res 5668  df-fun 6563  df-fn 6564

This theorem is used by:  fnssresd  6688  fnresin1  6689  fnresin2  6690  fnresi  6693  fssres  6773  fvreseq0  7063  fnreseql  7073  ffvresb  7153  fnressn  7189  soisores  7361  oprres  7615  ofres  7739  fsplitfpar  8159  fnsuppres  8239  tfrlem1  8414  tz7.48lemOLD  8482  tz7.49c  8487  resixp  8992  ixpfi2  9370  ttrclss  9751  dfac12lem1  10252  ackbij2lem3  10348  cfsmolem  10378  alephsing  10384  ttukeylem3  10619  iunfo  10653  fpwwe2lem7  10752  mulnzcnf  11992  seqfeq2  14198  seqf1olem2  14215  bpolylem  16246  reeff1  16320  sscres  18030  fullsubc  18057  fullresc  18058  funcres2c  18110  dmaf  18256  cdaf  18257  frmdplusg  19082  frmdss2  19091  gass  19548  dprdfadd  20269  rngmgpf  20412  mgpf  20508  prdscrngd  20584  rnghmresfn  20904  rnghmsscmap2  20914  rnghmsscmap  20915  rhmresfn  20933  rhmsscmap2  20943  rhmsscmap  20944  subrgascl  22408  upxp  23975  uptx  23977  cnmpt1st  24020  cnmpt2nd  24021  cnextfres1  24420  prdstmdd  24476  ressprdsds  24723  prdsxmslem2  24881  xrsdsre  25163  recosf1o  26896  resinf1o  26897  mpodvdsmulf1o  27554  dvdsmulf1o  27556  ex-fpar  31096  sspg  31363  ssps  31365  sspmlem  31367  sspn  31371  hhssnv  31899  ressupprn  33357  1stpreimas  33373  cnre2csqlem  34625  raddcn  34644  carsggect  35033  subiwrdlen  35101  signsvtn0  35282  signstres  35287  bnj1253  35730  bnj1280  35733  gblacfnacd  36042  subfacp1lem5  36129  cvmlift2lem9a  36248  filnetlem4  37360  finixpnum  38733  poimirlem4  38747  poimirlem8  38751  ftc1anclem3  38818  isdrngo2  39095  diaintclN  42318  dibintclN  42427  dihintcl  42604  imaiinfv  43908  aomclem6  44265  deg1mhm  44405  limsupvaluz2  46963  supcnvlimsup  46965  limsupgtlem  47002  resincncf  47100  icccncfext  47112  fourierdlem42  47374  fourierdlem73  47404  fdivmpt  49867  slotresfo  50228  basresposfo  50307  oppff1  50479