Theorem fnssres 6644

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

Syntax hints:   → wi 4   ∧ wa 395   ⊆ wss 3917   ↾ cres 5643   Fn wfn 6509

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1795  ax-4 1809  ax-5 1910  ax-6 1967  ax-7 2008  ax-8 2111  ax-9 2119  ax-ext 2702  ax-sep 5254  ax-nul 5264  ax-pr 5390

This theorem depends on definitions:  df-bi 207  df-an 396  df-or 848  df-3an 1088  df-tru 1543  df-fal 1553  df-ex 1780  df-sb 2066  df-clab 2709  df-cleq 2722  df-clel 2804  df-ral 3046  df-rex 3055  df-rab 3409  df-v 3452  df-dif 3920  df-un 3922  df-in 3924  df-ss 3934  df-nul 4300  df-if 4492  df-sn 4593  df-pr 4595  df-op 4599  df-br 5111  df-opab 5173  df-xp 5647  df-rel 5648  df-cnv 5649  df-co 5650  df-dm 5651  df-res 5653  df-fun 6516  df-fn 6517

This theorem is referenced by:  fnssresd  6645  fnresin1  6646  fnresin2  6647  fnresi  6650  fssres  6729  fvreseq0  7013  fnreseql  7023  ffvresb  7100  fnressn  7133  soisores  7305  oprres  7560  ofres  7675  fsplitfpar  8100  fnsuppres  8173  tfrlem1  8347  tz7.48lem  8412  tz7.49c  8417  resixp  8909  ixpfi2  9308  ttrclss  9680  dfac12lem1  10104  ackbij2lem3  10200  cfsmolem  10230  alephsing  10236  ttukeylem3  10471  iunfo  10499  fpwwe2lem7  10597  mulnzcnf  11831  seqfeq2  13997  seqf1olem2  14014  bpolylem  16021  reeff1  16095  sscres  17792  fullsubc  17819  fullresc  17820  funcres2c  17872  dmaf  18018  cdaf  18019  frmdplusg  18788  frmdss2  18797  gass  19240  dprdfadd  19959  rngmgpf  20073  mgpf  20164  prdscrngd  20238  rnghmresfn  20535  rnghmsscmap2  20545  rnghmsscmap  20546  rhmresfn  20564  rhmsscmap2  20574  rhmsscmap  20575  subrgascl  21980  upxp  23517  uptx  23519  cnmpt1st  23562  cnmpt2nd  23563  cnextfres1  23962  prdstmdd  24018  ressprdsds  24266  prdsxmslem2  24424  xrsdsre  24706  recosf1o  26451  resinf1o  26452  mpodvdsmulf1o  27111  dvdsmulf1o  27113  ex-fpar  30398  sspg  30664  ssps  30666  sspmlem  30668  sspn  30672  hhssnv  31200  ressupprn  32620  1stpreimas  32636  cnre2csqlem  33907  raddcn  33926  carsggect  34316  subiwrdlen  34384  signsvtn0  34568  signstres  34573  bnj1253  35014  bnj1280  35017  gblacfnacd  35096  subfacp1lem5  35178  cvmlift2lem9a  35297  filnetlem4  36376  finixpnum  37606  poimirlem4  37625  poimirlem8  37629  ftc1anclem3  37696  isdrngo2  37959  diaintclN  41059  dibintclN  41168  dihintcl  41345  imaiinfv  42688  fnwe2lem2  43047  aomclem6  43055  deg1mhm  43196  limsupvaluz2  45743  supcnvlimsup  45745  limsupgtlem  45782  resincncf  45880  icccncfext  45892  fourierdlem42  46154  fourierdlem73  46184  fdivmpt  48533  slotresfo  48891  basresposfo  48970  oppff1  49141