Theorem resexg 5996

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

Syntax hints:   → wi 4   ∈ wcel 2114  Vcvv 3442   ⊆ wss 3903   ↾ cres 5636

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 5245

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 3402  df-v 3444  df-in 3910  df-ss 3920  df-res 5646

This theorem is referenced by:  resexd  5997  resex  5998  fvtresfn  6954  offres  7939  ressuppss  8137  ressuppssdif  8139  ecelqsw  8719  uniqsw  8725  eceldmqs  8738  resixp  8885  f1imaen3g  8967  dif1enlem  9098  sbthfilem  9136  fsuppres  9310  climres  15512  setsvalg  17107  setsid  17148  symgfixels  19380  qtopres  23659  vtxdginducedm1  29635  redwlk  29762  hhssva  31351  hhsssm  31352  hhshsslem1  31361  resf1o  32826  eulerpartlemmf  34559  exidres  38158  exidresid  38159  xrnresex  38709  unidmqs  39019  disjqmap2  39106  lmhmlnmsplit  43473  climresdm  46237  setsv  47767