Theorem fnssres 6042

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

Syntax hints:   → wi 4   ∧ wa 383   ⊆ wss 3607   ↾ cres 5145   Fn wfn 5921

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1762  ax-4 1777  ax-5 1879  ax-6 1945  ax-7 1981  ax-9 2039  ax-10 2059  ax-11 2074  ax-12 2087  ax-13 2282  ax-ext 2631  ax-sep 4814  ax-nul 4822  ax-pr 4936

This theorem depends on definitions:  df-bi 197  df-or 384  df-an 385  df-3an 1056  df-tru 1526  df-ex 1745  df-nf 1750  df-sb 1938  df-clab 2638  df-cleq 2644  df-clel 2647  df-nfc 2782  df-ral 2946  df-rex 2947  df-rab 2950  df-v 3233  df-dif 3610  df-un 3612  df-in 3614  df-ss 3621  df-nul 3949  df-if 4120  df-sn 4211  df-pr 4213  df-op 4217  df-br 4686  df-opab 4746  df-xp 5149  df-rel 5150  df-cnv 5151  df-co 5152  df-dm 5153  df-res 5155  df-fun 5928  df-fn 5929

This theorem is referenced by:  fnresin1  6043  fnresin2  6044  fssres  6108  fvreseq0  6357  fnreseql  6367  ffvresb  6434  fnressn  6465  soisores  6617  oprres  6844  ofres  6955  fnsuppres  7367  tfrlem1  7517  tz7.48lem  7581  tz7.49c  7586  resixp  7985  ixpfi2  8305  dfac12lem1  9003  ackbij2lem3  9101  cfsmolem  9130  alephsing  9136  ttukeylem3  9371  iunfo  9399  fpwwe2lem8  9497  mulnzcnopr  10711  seqfeq2  12864  seqf1olem2  12881  swrd0len  13467  swrdccat1  13503  bpolylem  14823  reeff1  14894  eucalg  15347  sscres  16530  fullsubc  16557  fullresc  16558  funcres2c  16608  dmaf  16746  cdaf  16747  frmdplusg  17438  frmdss2  17447  gass  17780  dprdfadd  18465  mgpf  18605  prdscrngd  18659  subrgascl  19546  mdetrsca  20457  upxp  21474  uptx  21476  cnmpt1st  21519  cnmpt2nd  21520  cnextfres1  21919  prdstmdd  21974  ressprdsds  22223  prdsxmslem2  22381  xrsdsre  22660  itg1addlem4  23511  recosf1o  24326  resinf1o  24327  dvdsmulf1o  24965  wlkres  26623  sspg  27711  ssps  27713  sspmlem  27715  sspn  27719  hhssnv  28249  1stpreimas  29611  cnre2csqlem  30084  rmulccn  30102  raddcn  30103  carsggect  30508  subiwrdlen  30576  signsvtn0  30775  signstres  30780  bnj1253  31211  bnj1280  31214  subfacp1lem3  31290  subfacp1lem5  31292  cvmlift2lem9a  31411  filnetlem4  32501  finixpnum  33524  poimirlem4  33543  poimirlem8  33547  ftc1anclem3  33617  isdrngo2  33887  diaintclN  36664  dibintclN  36773  dihintcl  36950  imaiinfv  37573  fnwe2lem2  37938  aomclem6  37946  deg1mhm  38102  fnssresd  39796  limsupvaluz2  40288  supcnvlimsup  40290  limsupgtlem  40327  resincncf  40406  icccncfext  40418  dvnprodlem1  40479  fourierdlem42  40684  fourierdlem73  40714  pfxccat1  41735  rnghmresfn  42288  rnghmsscmap2  42298  rnghmsscmap  42299  rhmresfn  42334  rhmsscmap2  42344  rhmsscmap  42345  fdivmpt  42659