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  28831  redwlk  28960  hhssva  30541  hhsssm  30542  hhshsslem1  30551  resf1o  31986  eulerpartlemmf  33405  exidres  36794  exidresid  36795  xrnresex  37324  unidmqs  37572  lmhmlnmsplit  41877  climresdm  44614  setsv  46094