Theorem fnssres 6463

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

Syntax hints:   → wi 4   ∧ wa 398   ⊆ wss 3934   ↾ cres 5550   Fn wfn 6343

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1790  ax-4 1804  ax-5 1905  ax-6 1964  ax-7 2009  ax-8 2110  ax-9 2118  ax-10 2139  ax-11 2154  ax-12 2170  ax-ext 2791  ax-sep 5194  ax-nul 5201  ax-pr 5320

This theorem depends on definitions:  df-bi 209  df-an 399  df-or 844  df-3an 1084  df-tru 1534  df-ex 1775  df-nf 1779  df-sb 2064  df-clab 2798  df-cleq 2812  df-clel 2891  df-nfc 2961  df-ral 3141  df-rex 3142  df-rab 3145  df-v 3495  df-dif 3937  df-un 3939  df-in 3941  df-ss 3950  df-nul 4290  df-if 4466  df-sn 4560  df-pr 4562  df-op 4566  df-br 5058  df-opab 5120  df-xp 5554  df-rel 5555  df-cnv 5556  df-co 5557  df-dm 5558  df-res 5560  df-fun 6350  df-fn 6351

This theorem is referenced by:  fnssresd  6464  fnresin1  6465  fnresin2  6466  fnresi  6469  fssres  6537  fvreseq0  6801  fnreseql  6811  ffvresb  6881  fnressn  6913  soisores  7072  oprres  7308  ofres  7417  fsplitfpar  7806  fnsuppres  7849  tfrlem1  8004  tz7.48lem  8069  tz7.49c  8074  resixp  8489  ixpfi2  8814  dfac12lem1  9561  ackbij2lem3  9655  cfsmolem  9684  alephsing  9690  ttukeylem3  9925  iunfo  9953  fpwwe2lem8  10051  mulnzcnopr  11278  seqfeq2  13385  seqf1olem2  13402  bpolylem  15394  reeff1  15465  sscres  17085  fullsubc  17112  fullresc  17113  funcres2c  17163  dmaf  17301  cdaf  17302  frmdplusg  18011  frmdss2  18020  gass  18423  dprdfadd  19134  mgpf  19301  prdscrngd  19355  subrgascl  20270  mdetrsca  21204  upxp  22223  uptx  22225  cnmpt1st  22268  cnmpt2nd  22269  cnextfres1  22668  prdstmdd  22724  ressprdsds  22973  prdsxmslem2  23131  xrsdsre  23410  itg1addlem4  24292  recosf1o  25111  resinf1o  25112  dvdsmulf1o  25763  ex-fpar  28233  sspg  28497  ssps  28499  sspmlem  28501  sspn  28505  hhssnv  29033  1stpreimas  30433  dimkerim  31016  cnre2csqlem  31146  rmulccn  31164  raddcn  31165  carsggect  31569  subiwrdlen  31637  signsvtn0  31833  signstres  31838  bnj1253  32282  bnj1280  32285  subfacp1lem3  32422  subfacp1lem5  32424  cvmlift2lem9a  32543  filnetlem4  33722  finixpnum  34869  poimirlem4  34888  poimirlem8  34892  ftc1anclem3  34961  isdrngo2  35228  diaintclN  38186  dibintclN  38295  dihintcl  38472  imaiinfv  39281  fnwe2lem2  39642  aomclem6  39650  deg1mhm  39798  limsupvaluz2  42009  supcnvlimsup  42011  limsupgtlem  42048  resincncf  42148  icccncfext  42160  dvnprodlem1  42221  fourierdlem42  42425  fourierdlem73  42455  rnghmresfn  44225  rnghmsscmap2  44235  rnghmsscmap  44236  rhmresfn  44271  rhmsscmap2  44281  rhmsscmap  44282  fdivmpt  44591