Theorem fnssresd 6640

Description: Restriction of a function to a subclass of its domain. (Contributed by Glauco Siliprandi, 5-Feb-2022.)

Hypotheses

Ref	Expression
fnssresd.1	⊢ (𝜑 → 𝐹 Fn 𝐴)
fnssresd.2	⊢ (𝜑 → 𝐵 ⊆ 𝐴)

Assertion

Ref	Expression
fnssresd	⊢ (𝜑 → (𝐹 ↾ 𝐵) Fn 𝐵)

Proof of Theorem fnssresd

Step	Hyp	Ref	Expression
1		fnssresd.1	. 2 ⊢ (𝜑 → 𝐹 Fn 𝐴)
2		fnssresd.2	. 2 ⊢ (𝜑 → 𝐵 ⊆ 𝐴)
3		fnssres 6639	. 2 ⊢ ((𝐹 Fn 𝐴 ∧ 𝐵 ⊆ 𝐴) → (𝐹 ↾ 𝐵) Fn 𝐵)
4	1, 2, 3	syl2anc 593	1 ⊢ (𝜑 → (𝐹 ↾ 𝐵) Fn 𝐵)

Syntax hints:   → wi 4   ⊆ wss 3902   ↾ cres 5645   Fn wfn 6511

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1814  ax-4 1828  ax-5 1929  ax-6 1986  ax-7 2027  ax-8 2143  ax-9 2151  ax-ext 2733  ax-sep 5243  ax-pr 5387

This theorem depends on definitions:  df-bi 209  df-an 400  df-or 859  df-3an 1099  df-tru 1562  df-fal 1572  df-ex 1799  df-sb 2090  df-clab 2740  df-cleq 2753  df-clel 2836  df-ral 3076  df-rex 3086  df-rab 3414  df-v 3455  df-dif 3905  df-un 3907  df-in 3909  df-ss 3919  df-nul 4284  df-if 4478  df-sn 4580  df-pr 4582  df-op 4586  df-br 5098  df-opab 5160  df-xp 5649  df-rel 5650  df-cnv 5651  df-co 5652  df-dm 5653  df-res 5655  df-fun 6518  df-fn 6519

This theorem is referenced by:  rescnvimafod  7049  fssrescdmd  7103  fpwwe2lem7  10589  pfxccat1  14709  mdetrsca  22651  2ndresdju  32812  fdifsupp  32848  fdifsuppconst  32852  ply1gsumz  33756  esplyind  33833  dimkerim  33885  rmulccn  34186  subfacp1lem3  35493  satfn  35666  eqresfnbd  42812  tfsconcatrev  43886  ofoafg  43892  xlimconst2  46370  dvnprodlem1  46481  fcoreslem4  47621  isubgredg  48449