Theorem fnssres 6654

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

This proof depends on syntax axioms:   → wi 4   ∧ wa 401   ⊆ wss 3899   ↾ cres 5653   Fn wfn 6526

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 2733  ax-sep 5249  ax-pr 5391

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 2740  df-cleq 2753  df-clel 2836  df-ral 3078  df-rex 3088  df-rab 3414  df-v 3453  df-dif 3902  df-un 3904  df-in 3906  df-ss 3916  df-nul 4280  df-if 4483  df-sn 4585  df-pr 4587  df-op 4591  df-br 5104  df-opab 5168  df-xp 5657  df-rel 5658  df-cnv 5659  df-co 5660  df-dm 5661  df-res 5663  df-fun 6533  df-fn 6534

This theorem is used by:  fnssresd  6655  fnresin1  6656  fnresin2  6657  fnresi  6660  fssres  6740  fvreseq0  7029  fnreseql  7039  ffvresb  7118  fnressn  7154  soisores  7327  oprres  7580  ofres  7701  fsplitfpar  8118  fnsuppres  8192  tfrlem1  8367  tz7.48lemOLD  8435  tz7.49c  8440  resixp  8945  ixpfi2  9323  ttrclss  9705  dfac12lem1  10203  ackbij2lem3  10299  cfsmolem  10329  alephsing  10335  ttukeylem3  10570  iunfo  10604  fpwwe2lem7  10703  mulnzcnf  11943  seqfeq2  14148  seqf1olem2  14165  bpolylem  16194  reeff1  16268  sscres  17978  fullsubc  18005  fullresc  18006  funcres2c  18058  dmaf  18204  cdaf  18205  frmdplusg  19030  frmdss2  19039  gass  19495  dprdfadd  20216  rngmgpf  20359  mgpf  20455  prdscrngd  20531  rnghmresfn  20851  rnghmsscmap2  20861  rnghmsscmap  20862  rhmresfn  20880  rhmsscmap2  20890  rhmsscmap  20891  subrgascl  22355  upxp  23922  uptx  23924  cnmpt1st  23967  cnmpt2nd  23968  cnextfres1  24367  prdstmdd  24423  ressprdsds  24670  prdsxmslem2  24828  xrsdsre  25110  recosf1o  26845  resinf1o  26846  mpodvdsmulf1o  27503  dvdsmulf1o  27505  ex-fpar  31045  sspg  31312  ssps  31314  sspmlem  31316  sspn  31320  hhssnv  31848  ressupprn  33265  1stpreimas  33281  cnre2csqlem  34524  raddcn  34543  carsggect  34933  subiwrdlen  35001  signsvtn0  35182  signstres  35187  bnj1253  35630  bnj1280  35633  gblacfnacd  35854  subfacp1lem5  35918  cvmlift2lem9a  36037  filnetlem4  37139  finixpnum  38496  poimirlem4  38510  poimirlem8  38514  ftc1anclem3  38581  isdrngo2  38860  diaintclN  42083  dibintclN  42192  dihintcl  42369  imaiinfv  43657  fnwe2lem2  44011  aomclem6  44019  deg1mhm  44160  limsupvaluz2  46692  supcnvlimsup  46694  limsupgtlem  46731  resincncf  46829  icccncfext  46841  fourierdlem42  47103  fourierdlem73  47133  fdivmpt  49596  slotresfo  49951  basresposfo  50030  oppff1  50200