Theorem resexg 5988

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

Syntax hints:   → wi 4   ∈ wcel 2109  Vcvv 3444   ⊆ wss 3911   ↾ cres 5633

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1795  ax-4 1809  ax-5 1910  ax-6 1967  ax-7 2008  ax-8 2111  ax-9 2119  ax-ext 2701  ax-sep 5246

This theorem depends on definitions:  df-bi 207  df-an 396  df-3an 1088  df-tru 1543  df-ex 1780  df-sb 2066  df-clab 2708  df-cleq 2721  df-clel 2803  df-rab 3403  df-v 3446  df-in 3918  df-ss 3928  df-res 5643

This theorem is referenced by:  resexd  5989  resex  5990  fvtresfn  6953  offres  7942  ressuppss  8140  ressuppssdif  8142  ecelqsw  8720  uniqsw  8726  eceldmqs  8738  resixp  8884  f1imaen3g  8965  dif1enlem  9098  dif1enlemOLD  9099  sbthfilem  9140  fsuppres  9321  climres  15519  setsvalg  17114  setsid  17155  symgfixels  19350  qtopres  23620  vtxdginducedm1  29526  redwlk  29653  hhssva  31238  hhsssm  31239  hhshsslem1  31248  resf1o  32705  eulerpartlemmf  34361  exidres  37867  exidresid  37868  xrnresex  38387  unidmqs  38641  lmhmlnmsplit  43071  climresdm  45843  setsv  47374