Theorem fnssres 6691

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

Syntax hints:   → wi 4   ∧ wa 395   ⊆ wss 3962   ↾ cres 5690   Fn wfn 6557

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1791  ax-4 1805  ax-5 1907  ax-6 1964  ax-7 2004  ax-8 2107  ax-9 2115  ax-ext 2705  ax-sep 5301  ax-nul 5311  ax-pr 5437

This theorem depends on definitions:  df-bi 207  df-an 396  df-or 848  df-3an 1088  df-tru 1539  df-fal 1549  df-ex 1776  df-sb 2062  df-clab 2712  df-cleq 2726  df-clel 2813  df-ral 3059  df-rex 3068  df-rab 3433  df-v 3479  df-dif 3965  df-un 3967  df-in 3969  df-ss 3979  df-nul 4339  df-if 4531  df-sn 4631  df-pr 4633  df-op 4637  df-br 5148  df-opab 5210  df-xp 5694  df-rel 5695  df-cnv 5696  df-co 5697  df-dm 5698  df-res 5700  df-fun 6564  df-fn 6565

This theorem is referenced by:  fnssresd  6692  fnresin1  6693  fnresin2  6694  fnresi  6697  fssres  6774  fvreseq0  7057  fnreseql  7067  ffvresb  7144  fnressn  7177  soisores  7346  oprres  7600  ofres  7715  fsplitfpar  8141  fnsuppres  8214  tfrlem1  8414  tz7.48lem  8479  tz7.49c  8484  resixp  8971  ixpfi2  9387  ttrclss  9757  dfac12lem1  10181  ackbij2lem3  10277  cfsmolem  10307  alephsing  10313  ttukeylem3  10548  iunfo  10576  fpwwe2lem7  10674  mulnzcnf  11906  seqfeq2  14062  seqf1olem2  14079  bpolylem  16080  reeff1  16152  sscres  17870  fullsubc  17900  fullresc  17901  funcres2c  17954  dmaf  18102  cdaf  18103  frmdplusg  18879  frmdss2  18888  gass  19331  dprdfadd  20054  rngmgpf  20174  mgpf  20265  prdscrngd  20335  rnghmresfn  20635  rnghmsscmap2  20645  rnghmsscmap  20646  rhmresfn  20664  rhmsscmap2  20674  rhmsscmap  20675  subrgascl  22107  upxp  23646  uptx  23648  cnmpt1st  23691  cnmpt2nd  23692  cnextfres1  24091  prdstmdd  24147  ressprdsds  24396  prdsxmslem2  24557  xrsdsre  24845  itg1addlem4OLD  25748  recosf1o  26591  resinf1o  26592  mpodvdsmulf1o  27251  dvdsmulf1o  27253  ex-fpar  30490  sspg  30756  ssps  30758  sspmlem  30760  sspn  30764  hhssnv  31292  ressupprn  32704  1stpreimas  32720  cnre2csqlem  33870  raddcn  33889  carsggect  34299  subiwrdlen  34367  signsvtn0  34563  signstres  34568  bnj1253  35009  bnj1280  35012  gblacfnacd  35091  subfacp1lem5  35168  cvmlift2lem9a  35287  filnetlem4  36363  finixpnum  37591  poimirlem4  37610  poimirlem8  37614  ftc1anclem3  37681  isdrngo2  37944  diaintclN  41040  dibintclN  41149  dihintcl  41326  imaiinfv  42680  fnwe2lem2  43039  aomclem6  43047  deg1mhm  43188  limsupvaluz2  45693  supcnvlimsup  45695  limsupgtlem  45732  resincncf  45830  icccncfext  45842  fourierdlem42  46104  fourierdlem73  46134  fdivmpt  48389