Theorem fnssres 6659

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

This proof depends on syntax axioms:   → wi 4   ∧ wa 401   ⊆ wss 3902   ↾ cres 5661   Fn wfn 6532

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 1943  ax-6 2000  ax-7 2041  ax-8 2147  ax-9 2155  ax-ext 2734  ax-sep 5255  ax-pr 5402

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 2100  df-clab 2741  df-cleq 2754  df-clel 2837  df-ral 3079  df-rex 3089  df-rab 3415  df-v 3455  df-dif 3905  df-un 3907  df-in 3909  df-ss 3919  df-nul 4283  df-if 4486  df-sn 4588  df-pr 4590  df-op 4594  df-br 5108  df-opab 5172  df-xp 5665  df-rel 5666  df-cnv 5667  df-co 5668  df-dm 5669  df-res 5671  df-fun 6539  df-fn 6540

This theorem is used by:  fnssresd  6660  fnresin1  6661  fnresin2  6662  fnresi  6665  fssres  6745  fvreseq0  7034  fnreseql  7044  ffvresb  7123  fnressn  7159  soisores  7332  oprres  7585  ofres  7701  fsplitfpar  8119  fnsuppres  8193  tfrlem1  8368  tz7.48lem  8434  tz7.49c  8439  resixp  8944  ixpfi2  9321  ttrclss  9703  dfac12lem1  10150  ackbij2lem3  10246  cfsmolem  10276  alephsing  10282  ttukeylem3  10517  iunfo  10551  fpwwe2lem7  10650  mulnzcnf  11888  seqfeq2  14093  seqf1olem2  14110  bpolylem  16140  reeff1  16214  sscres  17918  fullsubc  17945  fullresc  17946  funcres2c  17998  dmaf  18144  cdaf  18145  frmdplusg  18969  frmdss2  18978  gass  19434  dprdfadd  20155  rngmgpf  20298  mgpf  20393  prdscrngd  20468  rnghmresfn  20787  rnghmsscmap2  20797  rnghmsscmap  20798  rhmresfn  20816  rhmsscmap2  20826  rhmsscmap  20827  subrgascl  22288  upxp  23855  uptx  23857  cnmpt1st  23900  cnmpt2nd  23901  cnextfres1  24300  prdstmdd  24356  ressprdsds  24603  prdsxmslem2  24761  xrsdsre  25043  recosf1o  26780  resinf1o  26781  mpodvdsmulf1o  27438  dvdsmulf1o  27440  ex-fpar  30950  sspg  31217  ssps  31219  sspmlem  31221  sspn  31225  hhssnv  31753  ressupprn  33170  1stpreimas  33186  cnre2csqlem  34428  raddcn  34447  carsggect  34837  subiwrdlen  34905  signsvtn0  35086  signstres  35091  bnj1253  35534  bnj1280  35537  gblacfnacd  35707  subfacp1lem5  35771  cvmlift2lem9a  35890  filnetlem4  37008  finixpnum  38367  poimirlem4  38381  poimirlem8  38385  ftc1anclem3  38452  isdrngo2  38716  diaintclN  41939  dibintclN  42048  dihintcl  42225  imaiinfv  43546  fnwe2lem2  43900  aomclem6  43908  deg1mhm  44049  limsupvaluz2  46574  supcnvlimsup  46576  limsupgtlem  46613  resincncf  46711  icccncfext  46723  fourierdlem42  46985  fourierdlem73  47015  fdivmpt  49478  slotresfo  49833  basresposfo  49912  oppff1  50082