Theorem resexg 5987

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

Syntax hints:   → wi 4   ∈ wcel 2114  Vcvv 3441   ⊆ wss 3902   ↾ cres 5627

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1797  ax-4 1811  ax-5 1912  ax-6 1969  ax-7 2010  ax-8 2116  ax-9 2124  ax-ext 2709  ax-sep 5242

This theorem depends on definitions:  df-bi 207  df-an 396  df-3an 1089  df-tru 1545  df-ex 1782  df-sb 2069  df-clab 2716  df-cleq 2729  df-clel 2812  df-rab 3401  df-v 3443  df-in 3909  df-ss 3919  df-res 5637

This theorem is referenced by:  resexd  5988  resex  5989  fvtresfn  6945  offres  7930  ressuppss  8128  ressuppssdif  8130  ecelqsw  8710  uniqsw  8716  eceldmqs  8729  resixp  8876  f1imaen3g  8958  dif1enlem  9089  sbthfilem  9127  fsuppres  9301  climres  15503  setsvalg  17098  setsid  17139  symgfixels  19368  qtopres  23647  vtxdginducedm1  29622  redwlk  29749  hhssva  31337  hhsssm  31338  hhshsslem1  31347  resf1o  32812  eulerpartlemmf  34545  exidres  38092  exidresid  38093  xrnresex  38643  unidmqs  38953  disjqmap2  39040  lmhmlnmsplit  43407  climresdm  46171  setsv  47701