Theorem resexg 5936

Description: The restriction of a set is a set. (Contributed by NM, 28-Mar-1998.) (Proof shortened by Andrew Salmon, 27-Aug-2011.)

Assertion

Ref	Expression
resexg	⊢ (𝐴 ∈ 𝑉 → (𝐴 ↾ 𝐵) ∈ V)

Proof of Theorem resexg

Step	Hyp	Ref	Expression
1		resss 5915	. 2 ⊢ (𝐴 ↾ 𝐵) ⊆ 𝐴
2		ssexg 5251	. 2 ⊢ (((𝐴 ↾ 𝐵) ⊆ 𝐴 ∧ 𝐴 ∈ 𝑉) → (𝐴 ↾ 𝐵) ∈ V)
3	1, 2	mpan 687	1 ⊢ (𝐴 ∈ 𝑉 → (𝐴 ↾ 𝐵) ∈ V)

Syntax hints:   → wi 4   ∈ wcel 2110  Vcvv 3431   ⊆ wss 3892   ↾ cres 5592

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1802  ax-4 1816  ax-5 1917  ax-6 1975  ax-7 2015  ax-8 2112  ax-9 2120  ax-ext 2711  ax-sep 5227

This theorem depends on definitions:  df-bi 206  df-an 397  df-tru 1545  df-ex 1787  df-sb 2072  df-clab 2718  df-cleq 2732  df-clel 2818  df-rab 3075  df-v 3433  df-in 3899  df-ss 3909  df-res 5602

This theorem is referenced by:  resexd  5937  resex  5938  fvtresfn  6874  offres  7820  ressuppss  7991  ressuppssdif  7993  resixp  8713  dif1enlem  8934  sbthfilem  8975  fsuppres  9141  climres  15295  setsvalg  16878  setsid  16920  symgfixels  19053  qtopres  22860  vtxdginducedm1  27921  redwlk  28050  hhssva  29628  hhsssm  29629  hhshsslem1  29638  resf1o  31074  eulerpartlemmf  32351  exidres  36045  exidresid  36046  xrnresex  36541  unidmqs  36775  lmhmlnmsplit  40921  climresdm  43373  setsv  44809