Theorem resexd 5986

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

Syntax hints:   → wi 4   ∈ wcel 2121  Vcvv 3433   ↾ cres 5622

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1803  ax-4 1817  ax-5 1918  ax-6 1975  ax-7 2016  ax-8 2123  ax-9 2131  ax-ext 2713  ax-sep 5220

This theorem depends on definitions:  df-bi 209  df-an 398  df-3an 1095  df-tru 1551  df-ex 1788  df-sb 2075  df-clab 2720  df-cleq 2733  df-clel 2816  df-rab 3394  df-v 3435  df-in 3891  df-ss 3901  df-res 5632

This theorem is referenced by:  gsum2dlem2  19940  psrbagres  21908  tsmspropd  24118  ulmss  26383  elrgspnlem4  33328  extvfvcl  33730  esplyind  33769  lmimdim  33798  aks6d1c6lem3  42670  pwssplit4  43547  limsupresre  46151  limsupresico  46155  limsupresuz  46158  limsupres  46160  limsupresxr  46221  liminfresxr  46222  liminfresico  46226  liminfresre  46234  liminfresuz  46239  isubgriedg  48366  isubgrvtx  48370