Theorem resexd 6025

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 6024	. 2 ⊢ (𝐴 ∈ 𝑉 → (𝐴 ↾ 𝐵) ∈ V)
3	1, 2	syl 18	1 ⊢ (𝜑 → (𝐴 ↾ 𝐵) ∈ V)

This proof depends on syntax axioms:   → wi 4   ∈ wcel 2145  Vcvv 3453   ↾ cres 5661

This proof depends on axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1828  ax-4 1842  ax-5 1943  ax-6 2000  ax-7 2041  ax-8 2147  ax-9 2155  ax-ext 2734  ax-sep 5255

This proof depends on definitions:  df-bi 210  df-an 402  df-3an 1105  df-tru 1573  df-ex 1813  df-sb 2100  df-clab 2741  df-cleq 2754  df-clel 2837  df-rab 3415  df-v 3455  df-in 3909  df-ss 3919  df-res 5671

This theorem is used by:  gsum2dlem2  20099  psrbagres  22146  tsmspropd  24359  ulmss  26630  elrgspnlem4  33672  extvfvcl  34033  esplyind  34072  lmimdim  34101  aks6d1c6lem3  43025  pwssplit4  43917  limsupresre  46511  limsupresico  46515  limsupresuz  46518  limsupres  46520  limsupresxr  46581  liminfresxr  46582  liminfresico  46586  liminfresre  46594  liminfresuz  46599  isubgriedg  48766  isubgrvtx  48770