Theorem resexg 6028

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 6007	. 2 ⊢ (𝐴 ↾ 𝐵) ⊆ 𝐴
2		ssexg 5324	. 2 ⊢ (((𝐴 ↾ 𝐵) ⊆ 𝐴 ∧ 𝐴 ∈ 𝑉) → (𝐴 ↾ 𝐵) ∈ V)
3	1, 2	mpan 689	1 ⊢ (𝐴 ∈ 𝑉 → (𝐴 ↾ 𝐵) ∈ V)

Syntax hints:   → wi 4   ∈ wcel 2107  Vcvv 3475   ⊆ wss 3949   ↾ cres 5679

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1798  ax-4 1812  ax-5 1914  ax-6 1972  ax-7 2012  ax-8 2109  ax-9 2117  ax-ext 2704  ax-sep 5300

This theorem depends on definitions:  df-bi 206  df-an 398  df-tru 1545  df-ex 1783  df-sb 2069  df-clab 2711  df-cleq 2725  df-clel 2811  df-rab 3434  df-v 3477  df-in 3956  df-ss 3966  df-res 5689

This theorem is referenced by:  resexd  6029  resex  6030  fvtresfn  7001  offres  7970  ressuppss  8168  ressuppssdif  8170  resixp  8927  dif1enlem  9156  dif1enlemOLD  9157  sbthfilem  9201  fsuppres  9388  climres  15519  setsvalg  17099  setsid  17141  symgfixels  19302  qtopres  23202  vtxdginducedm1  28800  redwlk  28929  hhssva  30510  hhsssm  30511  hhshsslem1  30520  resf1o  31955  eulerpartlemmf  33374  exidres  36746  exidresid  36747  xrnresex  37276  unidmqs  37524  lmhmlnmsplit  41829  climresdm  44566  setsv  46046