Theorem resexd 6027

Description: The restriction of a set is a set. (Contributed by Glauco Siliprandi, 23-Oct-2021.)

Hypothesis

Ref	Expression
resexd.1	⊢ (𝜑 → 𝐴 ∈ 𝑉)

Assertion

Ref	Expression
resexd	⊢ (𝜑 → (𝐴 ↾ 𝐵) ∈ V)

Proof of Theorem resexd

Step	Hyp	Ref	Expression
1		resexd.1	. 2 ⊢ (𝜑 → 𝐴 ∈ 𝑉)
2		resexg 6026	. 2 ⊢ (𝐴 ∈ 𝑉 → (𝐴 ↾ 𝐵) ∈ V)
3	1, 2	syl 18	1 ⊢ (𝜑 → (𝐴 ↾ 𝐵) ∈ V)

Syntax hints:   → wi 4   ∈ wcel 2141  Vcvv 3453   ↾ cres 5663

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1823  ax-4 1837  ax-5 1938  ax-6 1995  ax-7 2036  ax-8 2143  ax-9 2151  ax-ext 2733  ax-sep 5256

This theorem depends on definitions:  df-bi 210  df-an 401  df-3an 1103  df-tru 1571  df-ex 1808  df-sb 2095  df-clab 2740  df-cleq 2753  df-clel 2836  df-rab 3415  df-v 3455  df-in 3911  df-ss 3921  df-res 5673

This theorem is referenced by:  gsum2dlem2  20040  psrbagres  22059  tsmspropd  24268  ulmss  26536  elrgspnlem4  33531  extvfvcl  33892  esplyind  33931  lmimdim  33960  aks6d1c6lem3  42885  pwssplit4  43764  limsupresre  46358  limsupresico  46362  limsupresuz  46365  limsupres  46367  limsupresxr  46428  liminfresxr  46429  liminfresico  46433  liminfresre  46441  liminfresuz  46446  isubgriedg  48573  isubgrvtx  48577