Theorem resexg 5978

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

Syntax hints:   → wi 4   ∈ wcel 2109  Vcvv 3436   ⊆ wss 3903   ↾ cres 5621

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 5235

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 3395  df-v 3438  df-in 3910  df-ss 3920  df-res 5631

This theorem is referenced by:  resexd  5979  resex  5980  fvtresfn  6932  offres  7918  ressuppss  8116  ressuppssdif  8118  ecelqsw  8696  uniqsw  8702  eceldmqs  8714  resixp  8860  f1imaen3g  8941  dif1enlem  9073  sbthfilem  9112  fsuppres  9283  climres  15482  setsvalg  17077  setsid  17118  symgfixels  19313  qtopres  23583  vtxdginducedm1  29493  redwlk  29620  hhssva  31205  hhsssm  31206  hhshsslem1  31215  resf1o  32682  eulerpartlemmf  34359  exidres  37878  exidresid  37879  xrnresex  38398  unidmqs  38652  lmhmlnmsplit  43080  climresdm  45851  setsv  47382