Theorem resexd 6016

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

This proof depends on syntax axioms:   → wi 4   ∈ wcel 2144  Vcvv 3450   ↾ cres 5652

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

This proof depends on definitions:  df-bi 210  df-an 402  df-3an 1105  df-tru 1572  df-ex 1812  df-sb 2099  df-clab 2739  df-cleq 2752  df-clel 2835  df-rab 3413  df-v 3452  df-ss 3896  df-in 4091  df-res 5662

This theorem is used by:  gsum2dlem2  20185  psrbagres  22238  tsmspropd  24451  ulmss  26724  elrgspnlem4  33806  extvfvcl  34168  esplyind  34207  lmimdim  34236  aks6d1c6lem3  43223  pwssplit4  44091  limsupresre  46706  limsupresico  46710  limsupresuz  46713  limsupres  46715  limsupresxr  46776  liminfresxr  46777  liminfresico  46781  liminfresre  46789  liminfresuz  46794  isubgriedg  48961  isubgrvtx  48965