Theorem fnssresd 6666

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 6665	. 2 ⊢ ((𝐹 Fn 𝐴 ∧ 𝐵 ⊆ 𝐴) → (𝐹 ↾ 𝐵) Fn 𝐵)
4	1, 2, 3	syl2anc 596	1 ⊢ (𝜑 → (𝐹 ↾ 𝐵) Fn 𝐵)

This proof depends on syntax axioms:   → wi 4   ⊆ wss 3896   ↾ cres 5652   Fn wfn 6536

This proof depends on axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1827  ax-4 1841  ax-5 1942  ax-6 1999  ax-7 2040  ax-8 2146  ax-9 2154  ax-ext 2732  ax-sep 5248  ax-pr 5390

This proof depends on definitions:  df-bi 210  df-an 402  df-or 862  df-3an 1105  df-tru 1572  df-fal 1582  df-ex 1812  df-sb 2099  df-clab 2739  df-cleq 2752  df-clel 2835  df-ral 3077  df-rex 3087  df-rab 3413  df-v 3452  df-ss 3897  df-dif 4046  df-in 4090  df-un 4150  df-nul 4278  df-if 4482  df-sn 4585  df-pr 4587  df-op 4835  df-br 5103  df-opab 5167  df-xp 5656  df-rel 5657  df-cnv 5658  df-co 5659  df-dm 5660  df-res 5662  df-fun 6543  df-fn 6544

This theorem is used by:  rescnvimafod  7076  fssrescdmd  7130  fnwe2lem3  8151  fpwwe2lem7  10727  pfxccat1  14857  mdetrsca  22925  2ndresdju  33292  fdifsupp  33327  fdifsuppconst  33331  ply1gsumz  34179  esplyind  34255  dimkerim  34307  rmulccn  34608  subfacp1lem3  36035  satfn  36208  eqresfnbd  43393  tfsconcatrev  44457  ofoafg  44463  xlimconst2  46952  dvnprodlem1  47063  fcoreslem4  48243  isubgredg  49071