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

Syntax hints:   → wi 4   ∧ wa 400   ⊆ wss 3906   ↾ cres 5665   Fn wfn 6533

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1825  ax-4 1839  ax-5 1940  ax-6 1997  ax-7 2038  ax-8 2145  ax-9 2153  ax-ext 2735  ax-sep 5258  ax-pr 5406

This theorem depends on definitions:  df-bi 210  df-an 401  df-or 861  df-3an 1105  df-tru 1573  df-fal 1583  df-ex 1810  df-sb 2097  df-clab 2742  df-cleq 2755  df-clel 2838  df-ral 3080  df-rex 3090  df-rab 3417  df-v 3457  df-dif 3909  df-un 3911  df-in 3913  df-ss 3923  df-nul 4288  df-if 4489  df-sn 4591  df-pr 4593  df-op 4597  df-br 5111  df-opab 5175  df-xp 5669  df-rel 5670  df-cnv 5671  df-co 5672  df-dm 5673  df-res 5675  df-fun 6540  df-fn 6541

This theorem is referenced by:  fnssresd  6661  fnresin1  6662  fnresin2  6663  fnresi  6666  fssres  6746  fvreseq0  7035  fnreseql  7045  ffvresb  7123  fnressn  7157  soisores  7327  oprres  7580  ofres  7695  fsplitfpar  8114  fnsuppres  8188  tfrlem1  8363  tz7.48lem  8429  tz7.49c  8434  resixp  8932  ixpfi2  9308  ttrclss  9690  dfac12lem1  10128  ackbij2lem3  10224  cfsmolem  10255  alephsing  10261  ttukeylem3  10496  iunfo  10524  fpwwe2lem7  10623  mulnzcnf  11861  seqfeq2  14063  seqf1olem2  14080  bpolylem  16103  reeff1  16177  sscres  17881  fullsubc  17908  fullresc  17909  funcres2c  17961  dmaf  18107  cdaf  18108  frmdplusg  18914  frmdss2  18923  gass  19372  dprdfadd  20093  rngmgpf  20236  mgpf  20331  prdscrngd  20404  rnghmresfn  20705  rnghmsscmap2  20715  rnghmsscmap  20716  rhmresfn  20734  rhmsscmap2  20744  rhmsscmap  20745  subrgascl  22198  upxp  23761  uptx  23763  cnmpt1st  23806  cnmpt2nd  23807  cnextfres1  24206  prdstmdd  24262  ressprdsds  24509  prdsxmslem2  24667  xrsdsre  24949  recosf1o  26681  resinf1o  26682  mpodvdsmulf1o  27339  dvdsmulf1o  27341  ex-fpar  30794  sspg  31061  ssps  31063  sspmlem  31065  sspn  31069  hhssnv  31597  ressupprn  33016  1stpreimas  33032  cnre2csqlem  34281  raddcn  34300  carsggect  34689  subiwrdlen  34757  signsvtn0  34938  signstres  34943  bnj1253  35386  bnj1280  35389  gblacfnacd  35567  subfacp1lem5  35657  cvmlift2lem9a  35776  filnetlem4  36873  finixpnum  38237  poimirlem4  38256  poimirlem8  38260  ftc1anclem3  38327  isdrngo2  38590  diaintclN  41813  dibintclN  41922  dihintcl  42099  imaiinfv  43407  fnwe2lem2  43761  aomclem6  43769  deg1mhm  43910  limsupvaluz2  46435  supcnvlimsup  46437  limsupgtlem  46474  resincncf  46572  icccncfext  46584  fourierdlem42  46846  fourierdlem73  46876  fdivmpt  49303  slotresfo  49660  basresposfo  49739  oppff1  49909